Configuring Proof general for Coq in emacs

Question

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.

Answer 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.

Answer 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

Answer 3

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.

Answer 4

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.