Agda2.4.2.2のWindowsへのインストール（決定版？）
2016-05-30追記
Agda2.5.1は割と素直にインストールできるようになりました。
先週うまくいかないと書いていたAgda新バージョンのインストールの話。改めて同僚Tさん*1にエラーについて聞いてみたら、原因が判明し、そしてインストールもできたので以下展開。
手順
- Hackageから http://hackage.haskell.org/package/Agda-2.4.2.2/Agda-2.4.2.2.tar.gz をダウンロード、展開
- 展開したディレクトリで cabal install -f -cpphs*2
- 先週の記事で書いたようなプリプロセッサのエラーがでる。ここで、
- 該当ファイルをエディタ等で開く
- "__IMPOSSIBLE__"の直前で改行。つまり、"__IMPOSSIBLE__"という記述が行頭に来るようにする。適切にインデントもして、保存
- 再度実行すると、エラーは消える
- このエラーが\src\full\Agda\TypeCheckingの下にあるTelescope.hsとInjectivity.hsで出るはず。どちらも上記のように改行、インデントで修正して実行すると、以下インストールはうまくいくはず。*3
原因
- Windows環境では、cppのHaskell版であるcpphsがうまく動かないらしく、-cpphsとして、cpphsではなくcppをつかわなければならない
- が、cppには上記のようなバグがあるので、cabalのネットワークインストールではなく、ソースをDLして直接修正してやる必要がある
ということらしい。
とりあえずAgda触ってみたい、と思って流れ着いてきた人のために
最新機能を使う必要はないと思うので、
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Windows
にあるAgda-2.3.0.1-20121108-setup.exeあたりを使うことをオススメします。神奈川大学理学部情報科学科の3年生向け授業でもこれを使ったので、比較的まともにインストールできるはず。。。
