4

I have some code that only compiles coq code in Coq 8.09.0 . The version that I normally use is the most up-to-date version now which is Coq 8.11.0. I was able to create a new environment using opam switch and installed Coq 8.09.0 there. I successfully compiled all of the files with this version; however, I can't use proof general in emacs as it is still using Coq 8.11.0. I was wondering how I could make Proof General use a different opam instance using opam switch in Emacs. I have tried doing the following in the eshell

opam switch vst
eval $(opam env)

where vst is the name of the switch as seen in the output of opam switch in my terminal:

#   switch   compiler                                                                         description
    4.10.0   ocaml-base-compiler.4.10.0                                                       4.10.0
    default  base-bigarray.base,base-threads.base,base-unix.base,ocaml.4.02.3,ocaml-config.1  default
->  vst      ocaml-base-compiler.4.09.0                                                       vst

However, the output of the eval $(opam env) line is the following:

Symbol’s function definition is void: opam

Which doesn't make sense since it understands what opam means as it was able to do the first command fine. Is there a proper way of doing opam switch to change what emacs uses? Is there a way to explicitly tell Proof General which instance of Coq it should use? Should I just uninstall Coq 8.11.0 and install Coq 8.09.0 directly using pacman (I am using manjaro)?

Notemaster
  • 465
  • 1
  • 3
  • 15
  • I use this [hack](https://gist.github.com/anton-trunov/b55fae56f92c35531fc480232bc74160). You might want to check the relevant issue here: https://github.com/ProofGeneral/PG/issues/210 – Anton Trunov Apr 22 '20 at 08:48
  • Oh that's interesting! I eventually found an answer that was suitably convenient because I already had tuareg installed. – Notemaster Apr 22 '20 at 13:34
  • If you know the path, you can add this line to the top of your `.v` file: `(* -*- coq-prog-name: "/home/myuser/bin/coqtop" -*- *)` – larsr Apr 23 '20 at 07:32

1 Answers1

3

Using M-x and searching for "opam version" gave me the promising option 

tuareg-opam-update-env

which allows one to switch environments. Doing this to switch to vst before opening a coq file and not autochecking the version of Coq seemed to work fine. Of course, this assumes one has tuareg already installed.

Notemaster
  • 465
  • 1
  • 3
  • 15