Configuring Proof general for Coq in emacs

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.

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