У меня есть код, который компилирует только код coq в Coq 8.09.0. Версия, которую я обычно использую, является самой современной версией, которая является Coq 8.11.0. Я смог создать новую среду с помощью переключателя opam и установил там Coq 8.09.0. Я успешно скомпилировал все файлы с этой версией; Тем не менее, я не могу использовать доказательство общего в Emacs, поскольку он по-прежнему использует Coq 8.11.0. Мне было интересно, как я могу заставить Proof General использовать другой экземпляр opam с помощью переключателя opam в Emacs. Я попытался сделать следующее в eshell
opam switch vst
eval $(opam env)
, где vst - это имя коммутатора, как видно из вывода opam switch в моем терминале:
# 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
Однако, вывод строки eval $(opam env) выглядит следующим образом:
Symbol’s function definition is void: opam
Что не имеет смысла, так как он понимает, что означает opam, поскольку он смог выполнить первую команду нормально. Есть ли правильный способ сделать opam switch, чтобы изменить то, что использует emacs? Есть ли способ явно указать Proof General, какой экземпляр Coq он должен использовать? Должен ли я просто удалить Coq 8.11.0 и установить Coq 8.09.0 напрямую, используя pacman (я использую manjaro)?