数学とプログラミングとくだらないこと

プログラミングの事とか数学のこととかを書いていきます。

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"