Windows にきちんと idris をインストールする

前回の記事では、Cygwin をつかう前提で記事を書いてしまいましたが、後で調べたらまともに動きませんでした←。お詫びします。

1. MinGW 環境の整備
MinGW がどんなものであるかについてはこの記事が参考になります。 このウィキペディアの記事でも触れられていますが、MinGW は Cygwin から派生したものであり、UNIX 的なツールを Windows で動かすためのプロジェクトという意味では基本的に似ています。 しかし、Cygwin が POSIX 互換を目指しているのに対し MinGW はもっと基本的な環境のみを実現するものです。

MinGW のインストールは http://sourceforge.net/projects/mingw/files/ においてある mingw-get-inst-xxxxyyzz.exe を用いて行えます。 これについては、対象となっている少しバージョンは古いですがこの記事が参考になります。

後で説明しますが idris-lang 導入のためには開発環境が必要になりますから、インストールのときの画面でコンパイルなどに必要なツールを選択しておくと良いです。
12

2. MinGW シェルの起動
MinGWで導入されたツールは、基本的にはMinGWシェルから呼ぶことになります。
スタートメニューから「mingw」ぐらいまで入れると出てくると思います。
3

3. cabal の更新
idris-lang を入れる前に、 cabal を更新しておきます。

$ cabal update

cabal 自体のアップデートを要求される事もあるかもしれません。

$ export LANG=en_US.UTF-8
$ cabal install cabal-install

4. gmp のインストール
続いて、gmp のインストールを行います。

$ export LANG=en_US.UTF-8
$ mingw-get install mingw32-gmp

5. idris のインストール

$ export LANG=en_US.UTF-8
$ cabal install idris

これで idris がインストールできるはずです。 gmp が欠けていると次のようなエラーが出て失敗すると思います。

Type checking .\System\Concurrency\Raw.idr
Type checking .\System\Concurrency\Process.idr
Type checking .\Language\Reflection.idr
Type checking .\Data\Morphisms.idr
Type checking .\Data\Bits.idr
Type checking .\Data\Word.idr
Type checking .\Control\Monad\Identity.idr
Type checking .\Control\Monad\State.idr
Type checking .\Control\Category.idr
Type checking .\Control\Arrow.idr
"make": Leaving directory `/tmp/idris-0.9.6-43096/idris-0.9.6/lib'
"make": Entering directory `/tmp/idris-0.9.6-43096/idris-0.9.6/rts'
gcc -O2 -Wall -c -o idris_rts.o idris_rts.c
gcc -O2 -Wall -c -o idris_gc.o idris_gc.c
gcc -O2 -Wall -c -o idris_gmp.o idris_gmp.c
idris_gmp.c:2:17: fatal error: gmp.h: No such file or directory
compilation terminated.
"make": *** [idris_gmp.o] Error 1
"make": Leaving directory `/tmp/idris-0.9.6-43096/idris-0.9.6/rts'
cabal.exe: Error: some packages failed to install:
idris-0.9.6 failed during the building phase. The exception was:
ExitFailure 2

6. idris を動かしてみる
インストールに成功したら、早速 idris のチュートリアル(PDF注意)に載っているサンプルを試してみましょう。 テキストファイル

module Main
main : IO ()
main = putStrLn "Hello world"

を hello.idr というタイトルで MinGW のホーム(多分C:\MinGW\msys\1.0\home\Usernameのあたりです)に保存し、idris でコンパイルし、実行してみましょう。

$ idris hello.idr -o hello
$ ./hello

ちゃんと Hello world と表示されたら成功です。

Windows に idris をインストールする

★追記 20130404★: 
この記事のCygwinを使った方法では問題があるようです。
Windows にきちんと idris をインストールする に修正版の記事を載せました。

idris-lang
idris という言語があるそうです : http://idris-lang.org/

idrisのインストール失敗と対処の記録
idris は Haskellの拡張らしいです。 上のリンクから色々たどれますが、とにかくインストールしようと思いました。 http://idris-lang.org/download を見ると

 >cabal install idris

でインストールできるはずです。 しかし、 Windows のコマンドプロンプトから試したところ

gcc -O2 -Wall -c -o idris_gc.o idris_gc.c
gcc -O2 -Wall -c -o idris_gmp.o idris_gmp.c
idris_gmp.c:2:17: fatal error: gmp.h: No such file or directory
compilation terminated.
: recipe for target `idris_gmp.o' failed
make: *** [idris_gmp.o] Error 1
make: Leaving directory `/cygdrive/c/Users/.../AppData/Local/Temp/idris-0.9
.6-10360/idris-0.9.6/rts'
cabal: Error: some packages failed to install:
idris-0.9.6 failed during the building phase. The exception was:
ExitFailure 2

となって止まってしまいました。 

@tanakh さんに gmp がインストールされていない事が原因なのではとご指摘いただき、cygwin に(gmp.h が参照されているのでソースも必要)インストールしましたが、Windowsのコマンドプロンプトから gcc を呼んだ場合に gcc から gmp.h が見えていないせいか、やはりコンパイルに失敗しました。

Windowsのコマンドプロンプトではなく Cygwin terminal から cabal install idris すれば gcc から gmp.h が見えているのではと期待しましたが、今度は文字コードの問題 lexical error (UTF-8 decoding error) で失敗しました。 どうやら en_JP だと駄目なようです。 そこで、次のようにしたところ、無事に idris がインストール出来ました:

$ export LANG=en_US.UTF-8
$ cabal install idris

まとめ
散漫になったのでまとめておきます。

    1. idris のコンパイルに必要なので、cygwin に gmp とそのソースをインストールした。
    2. idris を cabal でインストールする際の文字コード問題を回避するために cygterm で export LANG=en_US.UTF-8 した。
    3. cygterm から cabal install idris した。