GNU bug report logs - #27761
Crash while using proof-general/company-coq on OS X

Previous Next

Full log

View this message in rfc822 format

From: "Charles A. Roelli" <charles <at> aurox.ch>
To: 27761 <at> debbugs.gnu.org
Subject: bug#27761: Crash while using proof-general/company-coq on OS X
Date: Wed, 19 Jul 2017 21:12:18 +0200

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")

(add-to-list
   'package-archives
   '("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

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.