Как переключиться на конкретную версию Coq?

Question

В настоящее время я использую стандартный, который я установил стандартным способом (вероятно, через веб-сайт). Но я хочу использовать tcoq. Я полагаю, что установил его правильно, потому что у меня есть файл bin и все обычные вещи Coq, кажется, там:

pinno:~/gamepad/tcoq $ ls bin
coq-tex     coqc        coqchk.byte coqdep_boot coqmktop    coqtop.byte coqworkmgr  gallina
coq_makefile    coqchk      coqdep      coqdoc      coqtop      coqwc       fake_ide    ocamllibdep

Я попытался сделать псевдоним:

alias tcoq="/Users/pinno/gamepad/tcoq/bin/coqc"

к нему в моем vimrc, который выполняет правильную команду, но затем я получаю дальнейшие ошибки, такие как:

pinno:~/gamepad $ tcoq examples/foo1.v > examples/foo1.dump
Error: cannot guess a path for Coq libraries; please use -coqlib option

что заставляет меня думать, что я не создал команду для полного перехода на эту версию coq. Как мне сделать такую ​​вещь?

Answer 1

Не очень интересный ответ, но я просто следовал инструкциям снова, и это, кажется, работает. Перейдите на https://github.com/ml4tp/gamepad и выполните файл read me. Команда, которая устанавливает PATH:

ВАЖНО: установите в своем терминале указатель на встроенную версию tcoq (установив правильный PATH) source build_config.sh

который содержит:

COQBUILD=$PWD/tcoq/build

export PATH=$COQBUILD/bin:$PATH
export COQ_MK=$COQBUILD/bin/coq_makefile
export COQBIN=$COQBUILD/bin/

Answer 2

Мне предложили сделать так:opam pin add coq <version>для конкретной версии coq. Хотя не совсем уверен, что это делает или с чем сравниваетсяcoq install coq <version>. Pin сохраняет его в этой версии независимо от будущих команд opam.