Agda2.5.1のWindowsへのインストール/バージョンアップ

Agda

このたびAgdaを最新の2.5.1にバージョンアップしたので、手順を記録しておく。
特に、新しくなったライブラリ管理の設定方法がややこしかった。手順は主に以下に従った。
http://hackage.haskell.org/package/Agda-2.5.1/changelog
何にせよ、ようやくまともにインストールできるようになって嬉しい！

Agdaのインストール

  1. 古いHaskell Platformをアンインストール(バージョンアップの人は)
  2. 新しいHaskell Platformをインストール
  3. cabal update*1
  4. cabal install -f -cpphs
    • 相変わらず日本語環境だと-f -cpphsが必要な模様。

Emacsの設定

  1. 以下の2行を.emacsに追加する*2。

    (load-file (let ((coding-system-for-read 'utf-8))
                (shell-command-to-string "agda-mode locate")))


  2. emacsを起動して以下のhoge.agdaを作成する。

    module hoge where


  3. Ctrl-c Ctrl-lで型検査ができればインストールOK。

標準ライブラリのインストールと設定

  1. The Agda Wiki - Standard Libraryからダウンロードするか、Githubからとってくる。適当な場所に展開する。
  2. これからlibrariesという名前のテキストファイルを作る。まず、その置き場を以下のようにして探す。

    C:\Users\Shuji>agda -l hoho piyo.agda
Library 'hoho' not found.
Add the path to its .agda-lib file to
  'C:\Users\Shuji\AppData\Roaming\agda\libraries'
to install.

    この場合C:\Users\Shuji\AppData\Roaming\agda\の下にlibrariesという名前のファイルを置く。agdaというフォルダがない場合は自分で作る。


  3. librariesには、さきほど展開した標準ライブラリの中にある、standard-library.agda-libというファイルのフルパスを書く。つまり、こんな感じ。

    C:\Users\Shuji\Documents\agda-stdlib\standard-library.agda-lib


  4. defaultsという名前のファイルを作成し、同じ場所に置く。中身は以下の1行。

    standard-library


このやり方はchangelogに書いてある3通りの方法のうち、3番目に該当する。何か作るのに標準ライブラリしか使わない人は、これでよいと思う。

あと、最初はgnupackのemacsにインストールしようと試みたのだが、どうもシェルの扱いかディレクトリ構成の扱いかが特殊のようで、よくわからず断念したことをメモしておく。

*1:このときwhere cabalなど入力して、新しいHPのcabalを叩いていることを確認したほうがよい。新しくインストールしたcabalが実行されるようになっていなければ、環境変数PATHの優先順位を見直す

*2:emacsを使っていない人には、NTEmacs / Emacs for Windowsの「24.5簡易IME対応版」をおすすめしておく。また、環境変数HOMEは適当な場所に設定されているものと仮定する。HOMEの下に.emacsができる