Я устанавливаю Coq, используя ссылки для загрузки из https://coq.inria.fr/ для Windows и Mac. Однако, когда я пытаюсь использовать coqc или coqtop в терминале или командной строке, я получаю сообщения об ошибках, говорящие, что команда не найдена. Хотя с учетом сказанного, я все еще могу запустить Coq почти отлично в среде Coq IDE, но когда я скомпилирую буфер, в частности упражнения от Software Foundations, я получаю следующее сообщение.Как установить Coq
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 или на оба таких, чтобы у меня не возникало проблем, о которых я упоминал выше?
Для Mac вы можете использовать [opam] (https://opam.ocaml.org) для установки coq (opam - это менеджер пакетов на основе для экосистемы OCaml). Для установки opam можно использовать [homebrew] (http://brew.sh), который является менеджером пакетов для macOS (homebrew использует как двоичные, так и исходные пакеты). –
@AntonTrunov: Эта рекомендация, похоже, немного задействована. Не удается установить Coq непосредственно из доморощенного? –
@ Zimmi48 О, да, вы правы :) Это просто, когда вы экспериментируете с версиями Coq и разными пакетами, мне проще использовать opam. –