2

I was trying to use coq in vscode but I can't seem to make it to work.

Error:

Could not start coqtop (coqtop)

I get this option: enter image description here

which is puzzling since my terminal seems to know just fine where coq is:

(meta_learning) brandomiranda~/sketching-learning-coq ❯ coqc -v
The Coq Proof Assistant, version 8.14.1
compiled with OCaml 4.10.2
(meta_learning) brandomiranda~/sketching-learning-coq ❯ echo $PATH
/Users/brandomiranda/.opam/__coq-platform.2022.01.0~8.14~2022.01/bin:/Users/brandomiranda/opt/anaconda3/envs/meta_learning/bin:/opt/homebrew/bin:/usr/bin:/bin:/usr/sbin:/sbin

So my questions are:

  1. Why is this error happening when I open vscode if my terminal can find coq just fine?
  2. How do I fix this? What path do I need to set and why?

I was suggested to do:

eval $(opam env); dirname $(which coqtop)

but it didn't do anything or at least it didn't fix the problem...

I did copy pasted:

/Users/brandomiranda/.opam/__coq-platform.2022.01.0~8.14~2022.01/bin

to the prompt vscode gives me and it seems to have fixed it since my script was checked correctly. However, I find this disturbing cu I don't know what it did or why this worked.

Can someone explain to me why this worked -- especially since looking at my PATH (printed above) coq is globally available already?

fyi to install code use their plataform install scripts: https://github.com/coq/platform/blob/main/doc/README_macOS.md I suppose after doing that the above PATH would have been updated to the right thing that I copy pasted to the set global from vscode.

related:

Charlie Parker
  • 5,884
  • 57
  • 198
  • 323
  • solns in coq discuss: https://coq.discourse.group/t/how-to-import-basics-v-in-induction-v-of-lf-using-vs-coq-extension/1633/8 and https://coq.discourse.group/t/how-to-have-vscode-find-coq/1582/6?u=brando90 – Charlie Parker Feb 24 '23 at 23:50

1 Answers1

0

Ok I fixed it I think. This is what I did:

  1. create a new switch e.g. opam switch create hammer_switch ocaml-base-compiler.4.12.0 and made sure I had xcode & hombrew/brew. (note you can have opam managed in coda in linux/ubuntu it seems)
  2. I installed the coq plataform using their binaries https://github.com/coq/platform/blob/main/doc/README_macOS.md and ran bash coq_platform_make.sh updated my path with $(opam env) (Q: not with eval $(opam env)? weird...)
  3. made sure coqtop path in the vscode settings (VSCode settings (usually with Cmd and comma ,)) had the path from my PATH e.g. /Users/brandomiranda/.opam/__coq-platform.2022.01.0~8.15~beta1/bin or do echo $PATH copy the coq part into vscode's setting. Note that your switch might not have the word coq in it but it istall has it installed so for me I copied /Users/brandomiranda/.opam/4.12.1/bin and that worked too. More details in extra bellow.
  4. restarted vscode several times to make sure it was running the above path.

see: https://coq.discourse.group/t/how-to-have-vscode-find-coq/1582/2?u=brando90

for the cotop vscode see (do VSCode settings (usually with Cmd and comma ,) to go there):

enter image description here

related but when installing new plugin: https://github.com/lukaszcz/coqhammer/issues/122

vscode gitissue: https://github.com/coq-community/vscoq/issues/243

--

Other way to install Coq not using the official plataform scripts (might be easier to set up HPC machines with coq?)

Seems you can install coq this way too:

# - install opam
# brew install opam # for mac
conda install -c conda-forge opam
opam init
# if doing local env? https://stackoverflow.com/questions/72522412/what-does-eval-opam-env-do-does-it-activate-a-opam-environment
# eval $(opam env)

# - install coq
# local install
#opam switch create . 4.12.1
#eval $(opam env)
#opam repo add coq-released https://coq.inria.fr/opam/released
#opam install coq

# If you want a single global (wrt conda) coq installation (for say your laptop):
opam switch create 4.12.1
opam switch 4.12.1
# eval $(opam env)  # why don't I need this in the global, what makes this global?
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq

though I need to figure out where eval $(opam env) goes.

Extra: discussion on path names to put in vscode

My path looked as follows:

(iit_synthesis) brandomiranda~ ❯ echo $PATH
/Users/brandomiranda/.opam/4.12.1/bin:/Users/brandomiranda/miniconda/envs/iit_synthesis/bin:/Users/brandomiranda/miniconda/condabin:/usr/local/bin:/Users/brandomiranda/.opam/4.12.1/bin:/opt/homebrew/bin:/usr/bin:/bin:/usr/sbin:/sbin

but I was already on the switch 4.12.1 already and installed coq in it because I ran:

# - install opam
brew install opam
# https://stackoverflow.com/questions/72522266/how-does-one-install-opam-with-conda-for-mac-apple-os-x
# conda install -c conda-forge opam
opam init
# if doing local env? https://stackoverflow.com/questions/72522412/what-does-eval-opam-env-do-does-it-activate-a-opam-environment
#eval $(opam env)

# - install coq
# local install
#opam switch create . 4.12.1
#eval $(opam env)
#opam repo add coq-released https://coq.inria.fr/opam/released
#opam install coq

# If you want a single global (wrt conda) coq installation (for say your laptop):
opam switch create 4.12.1
opam switch 4.12.1
eval $(opam env)
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq

In that state I test coq in terminal and it was there:

(iit_synthesis) brandomiranda~ ❯ opam switch
#  switch                                 compiler                    description
→  4.12.1                                 ocaml-base-compiler.4.12.1  4.12.1
   __coq-platform.2022.01.0~8.14~2022.01  ocaml-base-compiler.4.10.2  __coq-platform.2022.01.0~8.14~2022.01
(iit_synthesis) brandomiranda~ ❯ coqtop
Welcome to Coq 8.15.1

Coq < ^C
Error: User interrupt.

Coq < ^D

and the switch __coq-platform.2022.01.0~8.14~2022.01 ocaml-base-compiler.4.10.2 __coq-platform.2022.01.0~8.14~2022.01 must have been set up at a different time when I did plataform install but now I'm ignoring it and I'm not in that switch so I don't think it will matter much.

Charlie Parker
  • 5,884
  • 57
  • 198
  • 323