Как установить Coq
Я устанавливал Coq, используя ссылки для скачивания с https://coq.inria.fr/ для Windows и Mac. Тем не менее, когда я пытаюсь coqc или же coqtop в терминале или командной строке я получаю сообщения об ошибках, в которых говорится, что команда не найдена. Хотя с учетом вышесказанного, я все еще могу почти идеально запускать Coq в Coq IDE, но когда я компилирую буфер, в частности, упражнения из Software Foundations, я получаю следующее сообщение.
Running: coqc -I '/Users/zhangsheng/Desktop/G/repos/Coqy/cis500' '/Users/zhangsheng/Desktop/G/repos/Coqy/cis500/Basics.v' 2>&1
Из того, что я понимаю, 2>&1 кажется, какая-то форма неправильного направления, и я чувствую, что это причина, почему coqc а также coqtop кажется, не работает на моем терминале / командной строке.
Может кто-нибудь любезно предложить "лучший" способ установки Coq на Mac или Windows или на оба, чтобы у меня не возникло проблем, о которых я упоминал выше?
2 ответа
Хотя я не пользователь Windows или OSX, я думаю, что у вас возникла эта проблема, потому что установщик Coq не обновляет систему PATH переменная. Эта переменная представляет собой список каталогов, используемых терминалом для поиска программ, соответствующих введенным вами командам. Если вы не хотите устанавливать Coq другим способом, вы, вероятно, должны найти coqc а также coqtop двоичные файлы установлены, и добавьте эти каталоги в свой PATH, Вот несколько ссылок о том, как это сделать: OSX, Windows.