せっかく Antergos をインストールしたのだからもっとそれっぽい話でも増やすべきなのかもしれないが, 今の所特に思い浮かんでいない. こんにちは515ひかるです.
なんか壁にぶち当たって解決したら記事にしようかと思っているのだけれど, そもそも壁にぶち当たらない. さっきも, あまりにも Coq の環境つくりが簡単に終わってしまって逆にビビっている.
とりあえず Coq をインストールしてみる.
% yaourt coq
インストールが済むまでひたすら待つ. 結構時間がかかった.
Proof General
Emacs と Proof General がいいらしいのでそれをとりあえず使う. インストール.
% yaourt proofgeneral
なんかメッセージが出てくる.
==> Put this in your /root/.emacs file to enable ProofGeneral mode
==> in emacs.
(load-file "/usr/share/emacs/site-lisp/ProofGeneral/generic/proof-site.el")
/root/.emacs は僕は使っていないので, ~/.emacs.d/init.el に指示されたように書き加える.
あとは, 拡張子が .v のファイルを試しに開いて動作確認.
% emacs test.v # -nw の場合は \emacs
無事終了. なんだこの簡単さは. 試しに記事っぽく書いたけど記事にする必要もないほど簡単だ. なんじゃこりゃ.
本当はこういうことを書きたいんだけど残念ながら書く機会も意味もなさそう.
