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)?
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.