Agda2をインストールする
カリー=ハワード同型対応とか難しい事は分からんが、型と証明が一対一で対応するらしい。 型理論の枠組みの中でプログラミングを行おうとする言語には、証明が出来るものがある。 という事で、Agdaというプログラミング言語を習得しようとインストールしてみた。
ここに書いてあることの大体は[Agda Wiki][agda-wiki]という所に書いてある。 というかAgdaに必要な知識の大体はここに書いてある。(英語の読めない自分には辛いけど。)
自分の環境はMac(Homebrew導入済み)なので、これを前提に進めていく。(というか、Debian系ディストリビューションにはパッケージがあるらしい…)
Haskell-Platformのインストール
Homebrewを使ってhaskell-platformをインストールする。
brew install haskell-platform
これだけ。ghcも必要になるけど、自動でインストールされる。
Mavericksの人へ
ghcはgccを使う事を前提としているようで、Xcode5のコンパイラ、clagnで使うには、フラグなどを適切にセットする必要がある。 ここを読んで知ったが、ghc-clang-wrapperというものがあるのでインストールした。
Agdaのインストール
haskell-platformがインストールできていれば、cabalというのが使えるようになる。 パッケージのアンインストールが手動なのが難点だけども、依存性解決とかが楽なのはうれしい。
cabal update
でパッケージ一覧をアップデートして、cabal install Agda
でインストール。
(Agda-Executableというのもあるけれど、よくわからないからAgdaの方をインストールしてしまった…)
Emacsのインストール
Agdaでの証明支援機能を使うには、コマンドラインツールかEmacsを使うらしい。
という事でEmacsをインストールした。今回インストールしたのはHomebrewからインストールできるEmacs24。
brew install emacs
するだけ。--japanese
フラッグを付けた方がいいかもしれない。
とりあえずインストールできたら、mkdir ~/.emacs.d
して、この下にinit.elを書いておく。
agda-modeの設定
agda-mode setup
する。これでEmacsからagdaが使えるようになるらしい。
Agdasのstandard libraryをインストール
[Agda Wiki][agda-wiki]のここからstandard libraryをインストールする。
.tar.gzファイルを解凍してどこか適当なところに置いておく。/usr/local/share/agda
とかがいいんじゃないだろうか。
次はEmacsの設定で、
M-x load-library RET agda2-mode RET M-x customize-group RET agda2 RET
として、Agda2 Include Dirsというオプションのツリーを開き、そこで置いておいたディレクトリの下にあるsrcのパスを挿入する。 STATUSのところをクリックして、Save for Future Sessionを選ぶ。
終わり
これでおわった(はず)。 基本ライブラリがロードできれば成功、できなければどうしようか?
[agda-wiki] http://wiki.portal.chalmers.se/agda/pmwiki.php "Agda Wiki"