The Coq mailing list

[Kwanghoon Choi <lazyswamp AT gmail.com>]

Dear Jelle,

You gave me a wonderful solution. It works! 

My problem seems to be caused by incorrect coq-prot-* settings. After applying .dir-locals.el as you suggested, I now see Coq/Emacs/ProofGeneral working well as I expect. 

Thanks!!!

Kwanghoon

On Wed, Feb 8, 2012 at 7:37 AM, Jelle Herold <jelle AT defekt.nl> wrote:

On 02/07/2012 12:57 AM, lazyswamp AT gmail.com wrote:

Hi,

I have an installation problem. When I load a Coq script (.v) and start
navigating by pressing C-c C-n (Next), the Emacs editor seems to hang for ever
by giving a message:

     Starting coqtop -emacs-U

I am not entirely sure, but I think this is due to incorrect coq-prog-* settings. Currently my preferred way of running coq is by placing a file named ".dir-locals.el" in the parent folder of my coq project. The file contains:

((coq-mode . (
(coq-prog-args . ("-emacs-U"))
(coq-prog-name . "/home/wires/opt/coq/coq-8.4beta/bin/coqtop")
)))

(Note the full path to the coq binary)
My .emacs file has no further settings.

Should you need to include libraries, then the format is

((coq-mode . (
(coq-prog-args . ("-emacs-U" "-R" "lib/something" "Something" "-R" "lib/else" "Else"))
(coq-prog-name . "/home/wires/opt/coq/coq-8.4beta/bin/coqtop")
)))


I realize this is not an answer to your question but it might help...

Bye,
Jelle.