2014-12-05

Agda2.4.2.2のWindowsへのインストール（決定版？）

Agda

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
先週の記事で書いたようなプリプロセッサのエラーがでる。ここで、
1. 該当ファイルをエディタ等で開く
2. "__IMPOSSIBLE__"の直前で改行。つまり、"__IMPOSSIBLE__"という記述が行頭に来るようにする。適切にインデントもして、保存
3. 再度実行すると、エラーは消える
このエラーが\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年生向け授業でもこれを使ったので、比較的まともにインストールできるはず。。。

*1:何度も登場しますが、Agdaの開発者のひとり

*2:--globalはお好み

*3:agdaを起動した状態でインストールを実行すると、最後にpermission deniedで実行ファイルを上書きできずにエラーで終わるので注意。5分ぐらいハマった

2014-11-28

Agda2.4.2.2のWindowsへのインストール格闘

Agda

最近の修正で、ロケールをなおす必要はなくなって、普通に

cabal install agda -f -cpphs

と同僚Tさんから聞いてやってみたのだが、失敗。以下ログ。またあとでやってみる。cabalが古いかも。

C:\Windows\system32>cabal install agda -f -cpphs
Resolving dependencies...
Downloading Agda-2.4.2.2...
[1 of 1] Compiling Main ( C:\Users\Shuji\AppData\Local\Temp\Agda-2.4.2.2-8956\Agda-2.4.2.2\dist\setup\setup.

(中略)

[193 of 278] Compiling Agda.TypeChecking.Patterns.Abstract ( src\full\Agda\TypeChecking\Patterns\Abstract.hs, dist\build
\Agda\TypeChecking\Patterns\Abstract.o )
[194 of 278] Compiling Agda.TypeChecking.Patterns.Match[boot] ( src\full\Agda\TypeChecking\Patterns\Match.hs-boot, dist\
build\Agda\TypeChecking\Patterns\Match.o-boot )
[195 of 278] Compiling Agda.TypeChecking.Reduce ( src\full\Agda\TypeChecking\Reduce.hs, dist\build\Agda\TypeChecking\Red
uce.o )
[196 of 278] Compiling Agda.TypeChecking.Telescope ( src\full\Agda\TypeChecking\Telescope.hs, dist\build\Agda\TypeChecki
ng\Telescope.o )
src\full\Agda\TypeChecking\Telescope.hs:64:23:
Not in scope: `__IMPOSSIBLE__'
Failed to install Agda-2.4.2.2
cabal: Error: some packages failed to install:
Agda-2.4.2.2 failed during the building phase. The exception was:
ExitFailure 1

追記　2014.12.03
そもそもhaskell-platformが古い（つまりghcが古い）というのが原因ではないかと思い、明日以降そこを更新してみる。とりあえず2014の64bit版は入れたのだが古いのと混在してしまい、よけいにカオス。

2014-11-14

Agda2.4.2のWindowsへのインストール

Agda

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.WindowsNotes-2-4-2
きのう同僚Tさんから聞いて驚いたのだが、一度ロケールを英語にしないとインストールできないというcabalのバグ？らしい。すごいな。自分のバージョンはまだ2.3.2だった。

2014-11-10

David Spivakとデータベースの圏

論文

この2週間ぐらい、働いていた時代に自分が作っていたソフトウェアの定式化、みたいなことを考えていた。かなり新しいことを考えたと思ってたけれども、そのうちの一部分は（たぶん）David Spivakがすでにやっている仕事にかなり近い、と思った。
http://d.hatena.ne.jp/m-hiyama/20130128/1359349560

とりあえず元論文を読む。

2014-11-06

海の向こうでAgda本が出るらしい

Agda

本日Agda-MLに流れてきた話によると、Aaron Stumpさんという型方*1がAgda本を執筆中で、出版社とも交渉中とのこと。現在のドラフト版が
https://svn.divms.uiowa.edu/repos/clc/projects/agda/book/
にあります。興味がある方はご一読を。ドラフトを15年春までに、と仰っているので、出るのは2015年中ぐらいでしょうか・・・

*1:私は面識はありません