Coqをインストールするには

WindowsとMacの両方でhttps://coq.inria.fr/のダウンロードリンクを使用してCoqをインストールしています。しかし、端末またはコマンドプロンプトでcoqcまたはcoqtopを試すと、コマンドが見つからないというエラーメッセージが表示されます。 Coq IDEでCoqをほぼ完璧に動かすことができますが、バッファをコンパイルすると、特に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は私のターミナル/コマンドプロンプト上で動作していないようだ理由であると感じています。

誰かが、私が上記の問題を抱えていないように、MacやWindows、あるいは両方でCoqをインストールするための「最良の」方法をお勧めしますか？

出典

2017-01-25 Zhangsheng

Macの場合、[opam]（https://opam.ocaml.org）を使用してcoqをインストールできます（opamはOCamlエコシステムのソースベースのパッケージマネージャです）。 opamをインストールするには、[homebrew]（http://brew.sh）を使用します。これはmacOSのパッケージマネージャーです（自作ではバイナリとソースベースの両方のパッケージを使用します）。 –

@AntonTrunov：この勧告は多少複雑です。 Coqを自作ソフトから直接インストールすることはできませんか？ –

@ Zimmi48ああ、そうだよ、それはちょうどCoqのバージョンとパッケージを試してみると、（私にとっては）opamを使うのが簡単だ。 –

私はWindowsまたはOSXユーザーではありませんが、CoqインストーラはシステムのPATH変数を更新しないため、この問題が発生していると思います。この変数は、入力したコマンドに対応するプログラムをルックアップするために端末が使用するディレクトリのリストです。別の方法でCoqをインストールしたくない場合は、coqcとcoqtopバイナリがインストールされている場所を見つけ、PATHに追加してください。これを行う方法に関する参考資料をいくつか示します：OSX、Windows

出典

2017-01-27 12:03:21

Coqをインストールするには

答えて

関連する問題