自宅のマシン (Windows 7) の VMware player に CentOS 6.5 (64bit) の仮想マシンを作成しようとしている．
coq, ssreflect, Java PathFinder を利用する予定．
以下，作業メモ．
http://ftp.riken.jp/Linux/centos/6.5/isos/x86_64/
から CentOS-6.5-x86_64-bin-DVD1.iso
と CentOS-6.5-x86_64-bin-DVD2.iso
をダウンロードして使う．DVD1.iso のダウンロードには15分くらいかかる．
sudoers を追加．/etc/sudoers.d/01user というファイルを作って，
そこに username ALL=(ALL) ALL という行を追加．
vmware tools をインストール
ホームディレクトリの下の日本語名のファイルを英語名に変更
$ LANG=C xdg-user-dirs-gtk-update
起動時にネットワークをONにするため，
/etc/sysconfig/network-scripts/ifcfg-eth0 で
ONBOOT=yes
と指定する．
dropboxをインストール．rpmファイルがダウンロードできるので，
以下を実行
# rpm -ivh hoge.rpm
良くはわからないが，どうも
/etc/yum.repos.d/dropbox.repo が作られて，その内容が
正しくないようで，このあと yum が失敗するようになる．
上記ファイルを削除しておく．
gccなどをインストール．
# yum install gcc gtk2-devel libXpm-devel libjpeg-turbo-devel libtiff-devel giflib-devel ncurses-devel
emacs24.3をインストール
$ ./configure --without-gsettings $ make $ src/emacs -Q (テスト) $ sudo make install
このうち，--without-gsettingsは，
CentOS6.5のビルド問題回避のために必要らしい．
既存マシンから .bashrc や .emacs などをコピー (dropboxにしまってある)
OCaml4.01をインストール．
(現時点の最新は4.02だが，Camlp5がまだ対応していないようだ
$ ./configure $ make world $ make bootstrap $ make opt $ make opt.opt $ sudo make install $ make clean
Camlp5 をインストール
$ ./configure --transitional $ make world.opt $ sudo make install
coq 8.4 pl4 をインストール
$ ./configure -local -opt $ make world
make install しないで使うと想定．Ltac を書きたいときにはこうしろ，
と書いてある….
以下を .bashrc などに追加
export COQDIR=/directory/where/coq/was/built
export PATH=${PATH}:${COQDIR}/bin
SSReflect 1.5 をインストール
$ export COQBIN=${COQDIR}/bin (coqtop等のバイナリがあるディレクトリ)
$ make
$ make install
この make install は，一般ユーザでよい．
${COQDIR}/user-contrib/Ssreflect に入る．
Mathcomp 1.5 をインストール
$ make $ make install
この make install は，一般ユーザでよい．
${COQDIR}/user-contrib/MathComp に入る．
ProofGeneral 4.2 をインストール．
Emacs 24.3 で使うには，
generic/pg-response.elに以下の修正が必要．
--- before/pg-response.el 2012-09-25 18:44:18.000000000 +0900
+++ after/pg-response.el 2013-03-14 22:57:29.000000000 +0900
@@ -101,9 +101,9 @@
pg-response-special-display-regexp
proof-multiframe-parameters)))
(if proof-multiple-frames-enable
- (add-to-list 'special-display-regexps spdres)
- (setq special-display-regexps
- (delete spdres special-display-regexps))))
+ (add-to-list 'display-buffer-alist spdres)
+ (setq display-buffer-alist
+ (delete spdres display-buffer-alist))))
(proof-layout-windows))
(defun proof-three-window-enable ()
この変更を加えた上で，以下のようにビルド
$ make clean $ make compile ルートになって # make install
.emacsの編集
(setq my-src-top "...")
(load-file (concat my-src-top "/ssreflect-1.5/pg-ssr.el"))
(load-file "/usr/share/emacs/site-lisp/ProofGeneral/generic/proof-site.el")
(setq coq-prog-args
(cons "-R"
(cons (concat my-src-top "/ssreflect-1.5/theories")
(cons "Ssreflect"
(cons "-R"
(cons (concat my-src-top "/mathcomp-1.5/theories")
(cons "MathComp"
(cons "-emacs"
nil))))))))
(setq proof-auto-raise-buffers nil)
(setq proof-three-window-enable t)