Coqインストール

「Coqインストール」の編集履歴(バックアップ)一覧はこちら

Coqインストール」の最新版変更点

追加された行は青色になります。

削除された行は赤色になります。

 *Coqインストール
 [[Coqダウンロード先ページ>>http://coq.inria.fr/download]]
 **Linuxの場合
 *** Ubuntu または Debian の場合
 - # sudo apt-get install coq coqide
 *** ソースから最新版をインストールする場合
 ソースからインストールするためにはocaml, camlp5が必要です。ソースにはREADMEの他にINSTALLというファイルがあって、そこにインストールするための詳細が記述されています。
 - OCamlがなければインストール (see [[http://ocaml.jp/インストール方法]])
 - camlp5のインストール ([[http://pauillac.inria.fr/~ddr/camlp5/]]からcamlp5-XXX.tgz をダウンロードする)
 -- $ ./configure --transitional
 -- $ make world.opt
 -- $ make install
 - Coqのインストール (coq-XXX.tar.gz をダウンロードする)
 -- $ ./configure
 -- $ make world
 -- $ make install
 **Macの場合
-- MacOS 10.6の場合、ダウンロード先の指示に従う
+- MacOS 10.6の場合 macportsを使うことになる
+-- [[http://www.cs.princeton.edu/courses/archive/fall09/cos441/coq-mac.html]] を参考にする。
+-- 但し、gmake@3.81, ocaml, camlp5, coq だけで良い。lablgtk2はatkが入らないので失敗し、Coqideは使えない。
 - MacOS 10.5の場合、バイナリイメージをそのまま導入可能
 - MacOS 10.4以下の場合上記のソースからインストールでO.K.
 **Windowsの場合
 - Coqダウンロード先ページよりインストーラをダウンロードしてインストール
 
 ----
 *Proof General のインストール
 コンソールのcoqtop, あるいはGUIのCoqIDEでも良いけど、emacsが好きな人はProof Generalを使うと良い。
 日本語も少なくともコメントでならばEUC-JPで入力可能なので、勉強会でデモするには便利。
 但し、MacOSXだとbackslashはコンソールのemacsでないとうまく入力出来ない?
 
 **入手先
 [[ProofGeneral入手先>>http://proofgeneral.inf.ed.ac.uk/]]のdownloadより入手。
 - 適当なディレクトリにProofGeneral-3.7.1.tgzを置く
 - $ tar xpzf ProofGeneral-3.7.1.tar.gz とかで展開
 - ~/.emacs に(load-file "dir/generic/proof-site.el") と書く。(dir=展開したファイルにpathが通る様に指定)
ツールボックス

下から選んでください:

新しいページを作成する
ヘルプ / FAQ もご覧ください。