Как перейти на конкретную версию Coq? - PullRequest
Новая
       10

Как перейти на конкретную версию Coq?

0 голосов
/ 28 января 2019

Я в настоящее время использую стандартный, который я установил стандартным способом (вероятно, через веб-сайт).Но я хочу использовать 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.Как мне сделать такую ​​вещь?

1 Ответ

0 голосов
/ 29 января 2019

Не очень интересный ответ, но я просто следовал инструкциям снова, и это, кажется, работает.Перейдите на 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/
...