Coqtop not found

I’m trying to use Coq with Proof General, but I’m new to this and don’t know what I’m doing.

I installed Coq on my Mac and was able to use CoqIDE.

Then I installed Emacs and Proof General, but Proof General cannot find coqtop. When I ran

which coqtop

on Terminal, it said “coqtop not found”. How can I fix this? I tried adding

(setq coq-prog-name “/usr/bin/coqtop -emacs”)

to my .emacs but it didn’t help.

(setq coq-prog-name “/usr/bin/coqtop”) maybe? That variable should contain the path of the binary, not the command line. Also, are you on macOS? If so, look into exec-path-from-shell.

But if you can’t find coqtop in the terminal, I think the problem isn’t with Emacs — how did you install coq? Did you install it as a macOS app? If so, the path is a bit different — something like /Applications/…/Contents/MacOS/… maybe?

I’m on mac too, actually, and had the same problem. You have to right click on coqide and click open application content, you’ll then find coqtop and all the executable stuff in resources/bin or something like that if my memory is good (at least there should be a bin folder containing all executable files somewhere in there).
You can add those to your path for next uses. Actually, I advise you to download everything with OPAM to get latest releases and be able to use mac shortcuts for some symbols.

I was able to find coqtop in


so I added

(setq coq-prog-name “/Applications/”)

to my .emacs but Proof General gives the error

usr/bin/coqtop -emacs -emacs … failed.

I installed CoqIDE for Mac OS X as an app. Should I delete it and reinstall with OPAM? If so, how?

Thanks for the help.

Can you show your .emacs?

+1 your emacs config is probably not working correctly.
Please show you .emacs and also the content of the *Messages* buffer after starting emacs.

I was able to fix it. I uninstalled the CoqIDE app and redid everything with opam as suggested. Thanks again for the help.