読者です 読者をやめる 読者になる 読者になる

Diary over Finite Fields

515ひかるが書き溜めたメモとコラムと雑記

Coq と Proof general をインストールした

せっかく 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


無事終了. なんだこの簡単さは. 試しに記事っぽく書いたけど記事にする必要もないほど簡単だ. なんじゃこりゃ.

本当はこういうことを書きたいんだけど残念ながら書く機会も意味もなさそう.

キーバインド

以前一度紹介した ProofCafe 様だけれど, そこにこんなページがあった.

ProofCafe - ProofGeneral

なるほど, あたりまえだけどキーバインドで進んだり後ろ行ったりできるのか. 使えるようにしたいところだ.