Coqtop not found

Using Coq
1

I’m trying to use Coq with Proof General, but I’m new to this and don’t know what I’m doing.

I installed Coq on my Mac and was able to use CoqIDE.

Then I installed Emacs and Proof General, but Proof General cannot find coqtop. When I ran

which coqtop

on Terminal, it said “coqtop not found”. How can I fix this? I tried adding

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

to my .emacs but it didn’t help.

1 Like
2

(setq coq-prog-name “/usr/bin/coqtop”) maybe? That variable should contain the path of the binary, not the command line. Also, are you on macOS? If so, look into exec-path-from-shell.

But if you can’t find coqtop in the terminal, I think the problem isn’t with Emacs — how did you install coq? Did you install it as a macOS app? If so, the path is a bit different — something like /Applications/…/Contents/MacOS/… maybe?

1 Like
3

I’m on mac too, actually, and had the same problem. You have to right click on coqide and click open application content, you’ll then find coqtop and all the executable stuff in resources/bin or something like that if my memory is good (at least there should be a bin folder containing all executable files somewhere in there).
You can add those to your path for next uses. Actually, I advise you to download everything with OPAM to get latest releases and be able to use mac shortcuts for some symbols.

4

I was able to find coqtop in

/Applications/CoqIDE_8.11.1.app/Contents/Resources/bin

so I added

(setq coq-prog-name “/Applications/CoqIDE_8.11.1.app/Contents/Resources/bin/coqtop”)

to my .emacs but Proof General gives the error

usr/bin/coqtop -emacs -emacs … failed.

I installed CoqIDE for Mac OS X as an app. Should I delete it and reinstall with OPAM? If so, how?

Thanks for the help.

5

Can you show your .emacs?

6

+1 your emacs config is probably not working correctly.
Please show you .emacs and also the content of the *Messages* buffer after starting emacs.

7

I was able to fix it. I uninstalled the CoqIDE app and redid everything with opam as suggested. Thanks again for the help.

8

Did you ever find a solution to this?

What brought me here was that I was using vs-code (How to set the coq path for vscode (how to find coqtop)? · Issue #243 · coq-community/vscoq · GitHub) and it couldn’t find the path since I didn’t have it installed. The dmg didn’t work so I installed it with opam and now vs-code was able to find coqtop by itself once I installed it with opam. Perhaps that is your issue. This is how I installed it with opam:

Installing Coq

  1. install brew: https://brew.sh/

  2. install opam (opam - Install):

# Homebrew
brew install gpatch
brew install opam

check opam was installed:

opam --version
  1. follow inria’s instructions: https://coq.inria.fr/opam-using.html but I think this works:
opam init
eval $(opam env)

opam install opam-depext
opam-depext coq

opam pin add coq 8.13.1

note: Pinning prevents opam from upgrading Coq automatically, which may cause inadvertent breakage in your Coq projects

then check coq installed correctly with:

coqc -v

To ensure that installation was successful, check that
coqc -v
prints the expected version of Coq.

hope it helps though I know this doesn’t answer the question of “where is coqtop” which I think would be nice to get an answer.

9
  1. which coqtop whill give you the location. See:
(base) miranda9@Brandos-MBP bin % which coqtop
/Users/miranda9/.opam/qcert-env/bin/coqtop
  1. if you do not have coq install then install it. For me installing it with an opam switch <COMPILER> version and pinning it to that compiler/switch worked nicely and kept my “opam env” organized. Pheraps you should do that. For that check my previous comment here: Coqtop not found - #8 by brando90

then if you .emacs file copy:

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

you probably have to restart emacs.

(note for vscode make sure you install coq with opam and restard vscode worked for me)

related: proofing - Configuring Proof general for Coq in emacs - Super User

10

You shouldn’t put -emacs in coq-prog-name, and these quotes should be straight, not curvy: (setq coq-prog-name "/usr/bin/coqtop"). But since /usr/bin is typically already in your path, there’s no point in adding that line (and, since you’re installing from OPAM, that’s not actually the right path)

11

for vs code issues: visual studio code - How to tell vscode where Coq is? (fixing Could not start coqtop (coqtop)) - Stack Overflow

12

the same question, I modified the init.el like this,
“/Applications/Coq-Platform~8.17~2023.08.app/Contents/Resources/bin/coqtop.opt”

It can work well for my MAC.

Your answer was near to the result, you just missed the “.opt” behind the coqtop.

13

the same question, I modified the init.el like this,
“/Applications/Coq-Platform~8.17~2023.08.app/Contents/Resources/bin/coqtop.opt”

It can work well for my MAC.