「Coqインストール」の編集履歴（バックアップ）一覧はこちら
「Coqインストール」(2010/10/17 (日) 19:35:25) の最新版変更点
追加された行は緑色になります。
削除された行は赤色になります。
*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.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が通る様に指定)
*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の場合 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が通る様に指定)
