[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

bug#27761: Crash while using proof-general/company-coq on OS X

From: Charles A. Roelli
Subject: bug#27761: Crash while using proof-general/company-coq on OS X
Date: Wed, 19 Jul 2017 21:12:18 +0200
User-agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:45.0) Gecko/20100101 Thunderbird/45.8.0

And by the way, I did more or less the following to install everything:
(I'm not familiar with these packages)

install coq from: https://coq.inria.fr/distrib/V8.4/files/coq-8.4.dmg
(latest version that works on macOS 10.6, it installs in /usr/local)

launch emacs -q 25.2

M-x load-library package
(setq package-user-dir "/tmp/elpa-bug-27761")

   '("melpa" . "http://melpa.milkbox.net/packages/";))

M-x package-refresh-contents

M-x package-install company
M-x package-install company-coq

# Follow instructions for compiling PG at https://github.com/ProofGeneral/PG
git clone https://github.com/ProofGeneral/PG /tmp/elpa-bug-27761/proof-general/
cd /tmp/elpa-bug-27761/proof-general/
make EMACS=/path/to/emacs-25.2

(load "/tmp/elpa-bug-27761/proof-general/generic/proof-site")

# As recommended here: https://github.com/cpitclaudel/company-coq
(add-hook 'coq-mode-hook #'company-coq-mode)

# Also recommended in the company-coq Readme
M-x company-coq-tutorial

reply via email to

[Prev in Thread] Current Thread [Next in Thread]