6

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.

3
  • 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
    Jun 23, 2014 at 5:44
  • 1
    did you try which cotop (assuming you have it installed) and then adding this (setq coq-prog-name “/usr/bin/coqtop -emacs”) to your .emacs file? Of course use your path. Btw, this link is useful: coq.discourse.group/t/coqtop-not-found/856/9 Jun 23, 2021 at 22:02
  • @CharlieParker Don't put -emacs in coq-prog-name
    – Clément
    Sep 21, 2021 at 16:07

4 Answers 4

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.

5
  • 1
    Hi, 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? Jun 29, 2014 at 16:15
  • 2
    Solved it by adding this to .emacs: (custom-set-variables '(coq-prog-name "PATH/TO/coqtop") '(proof-three-window-enable t)) Jun 29, 2014 at 16:48
  • actually I only invoked emacs from shell, and in that case it inherits the PATH variable of the bash.
    – P basak
    Jul 3, 2014 at 19:21
  • @MichaelBächtold how to do you find the path to coqtop? i.e. how do you do PATH/TO/coqtop Jun 23, 2021 at 21:49
  • @CharlieParker maybe this helps superuser.com/questions/570112/… Jun 24, 2021 at 6:06
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

2
  • The question specifically states "I installed Coq", so this isn't the problem. Oct 6, 2016 at 13:37
  • 1
    As 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
    Oct 6, 2016 at 16:07
0

This Worked for me. I have shown the entire process from nothing to getting Coq and configuring Proof General.

If you want to use Proof-General for Coq, first install Coq or anything that you want to use proof-general for.

I wanted to use it for Coq, so I installed Coq first.

1) Install Coq -> brew install coq (for macOS)

Get Emacs.app from https://emacsformacosx.com and install the application by dragging the icon into the Applications folder.

Follow the instructions for installing the Emacs Proof General extension via the MELPA package manager for Emacs or via Git.

2) Install Proof General ->

  • Using MELPA (recommended procedure) MELPA is a repository of Emacs packages. Skip this step if you already use MELPA. Otherwise, add the following to your .emacs and restart Emacs:

    (require 'package) (let* ((no-ssl (and (memq system-type '(windows-nt ms-dos)) (not (gnutls-available-p)))) (proto (if no-ssl "http" "https"))) (add-to-list 'package-archives (cons "melpa" (concat proto "://melpa.org/packages/")) t)) (package-initialize)

Note: If you switch to MELPA from a previously manually-installed Proof General, make sure you removed the old versions of Proof General from your Emacs context (by removing from your .emacs the line loading PG/generic/proof-site, or by uninstalling the proofgeneral package provided by your OS package manager).

Then, run M-x package-refresh-contents RET followed by M-x package-install RET proof-general RET to install and byte-compile proof-general.

You can now open a Coq file (.v), an EasyCrypt file (.ec), or a PhoX file (.phx) to automatically load the corresponding major mode.

  • Using Git (manual compilation procedure) Remove old versions of Proof General, clone the PG repo from GitHub and byte-compile the sources:

    git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG cd ~/.emacs.d/lisp/PG make

Then add the following to your .emacs:

;; Open .v files with Proof General's Coq mode
(load "~/.emacs.d/lisp/PG/generic/proof-site")

If Proof General complains about a version mismatch, make sure that the shell's emacs is indeed your usual Emacs. If not, run the Makefile again with an explicit path to Emacs. On macOS in particular you'll probably need something like

make clean; make EMACS=/Applications/Emacs.app/Contents/MacOS/Emacs

3) Add the following lines to your ~/.emacs file:

;; Make sure we can find coqtop
(setq exec-path (append exec-path '("/usr/local/bin")))

4) Add this to your .emacs

(custom-set-variables '(coq-prog-name "PATH/TO/coqtop") '(proof-three-window-enable t))

in case you can't find out your .emacs file, check this out. In my case I had to create a new .emacs file in my home directory.

0

First make sure you have installed Coq (these two worked for me: https://coq.inria.fr/opam-using.html or https://coq.discourse.group/t/coqtop-not-found/856/7).

Then ask your computer for the path to the current bin for coqtop:

which coqtop

e.g.

(base) miranda9@Brandos-MBP bin % which coqtop
/Users/miranda9/.opam/qcert-env/bin/coqtop

then put that path in your .emacs file as follow e.g.:

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

Actually, I just noticed I didn't use the one displayed by which but it seems to work for me regardless - which is still useful though.


Additional comments

Let me share the .emacs file that works for me:

(require 'package)
;; (setq gnutls-algorithm-priority "NORMAL:-VERS-TLS1.3") ; see remark below
(add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/") t)
(package-initialize)
(require 'evil)
  (evil-mode 1)
(custom-set-variables
 ;; custom-set-variables was added by Custom.
 ;; If you edit it by hand, you could mess it up, so be careful.
 ;; Your init file should contain only one such instance.
 ;; If there is more than one, they won't work right.
 '(package-selected-packages '(proof-general)))
(custom-set-faces
 ;; custom-set-faces was added by Custom.
 ;; If you edit it by hand, you could mess it up, so be careful.
 ;; Your init file should contain only one such instance.
 ;; If there is more than one, they won't work right.
 )

I learned that copy pasting different tutorial commands does not work well...e.g.

  • if you copy (require 'package) multiple times it causes errors becuase it is not an indepodent op
  • it seems that you do not need to set the coqtop path explicitly if you use PG - PG finds it on its own
    • I think it's because I installed it with opam but I am not 100%

hope that helps.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.