Mac – Configuring Proof general for Coq in emacs


I installed Coq in my system from the default installer. Then I added proof general to my existing emacs. But the problem is when I try to run a command in emacs I find the following from emacs,

Searching for program no such file or directory coqtop

I believe there are some configuration errors.

Looking forward to your thoughts.

Best Answer

  • I just figured out that i have to include the path to coqtop to the emacs path. or you can have that in your system path. in that case you have to invoke emacs from shell.