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.

Solution 1:

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.

Solution 2:

Different from the OP's case but a similar issue: The error message Searching for program: no such file or directory, coqtop may also occur if you haven't installed coq. Then the coqtop command will be missing from your system.

To diagnose, run which coqtop. If the result is empty, it's not installed or not on your path.

On mac, I solved this problem by installing coq with homebrew using brew install coq