5
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.
P basak
Posted 2014-06-20T18:41:17.517
Reputation: 171
2
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.
P basak
Posted 2014-06-20T18:41:17.517
Reputation: 171
1Hi, I get the same error message, although I installed coq with homebrew on a mac. Could you possibly explain in more detail how to add the path to the emacs path? – Michael Bächtold – 2014-06-29T16:15:57.610
2Solved it by adding this to .emacs: (custom-set-variables '(coq-prog-name "PATH/TO/coqtop") '(proof-three-window-enable t)) – Michael Bächtold – 2014-06-29T16:48:44.637
actually I only invoked emacs from shell, and in that case it inherits the PATH variable of the bash. – P basak – 2014-07-03T19:21:21.850
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
dinosaur
Posted 2014-06-20T18:41:17.517
Reputation: 131
The question specifically states "I installed Coq", so this isn't the problem. – Toby Speight – 2016-10-06T13:37:13.800
1As I said, this is different from the OP's case. But this question comes up in search results for Searching for program no such file or directory coqtop. In many of thoses cases, this answer is useful. – dinosaur – 2016-10-06T16:07:49.383
What you describe sounds like a basic situation where the first things to check would be whether the library is in your load path, and whether that library has a provide statement at the bottom, and whether there is a require statement in your user configuration file. Typically, the proper procedure is to assign a directory to the load path and place the library there. In the user configuration, file put a statement
(require '....). So long as the library is in your load path, and so long as it has a statement like(provide '...), then that is usually sufficient to resolve load issues. – lawlist – 2014-06-23T05:44:35.033