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 と表示されたら成功です。

広告
コメントする

コメントを残す

以下に詳細を記入するか、アイコンをクリックしてログインしてください。

WordPress.com ロゴ

WordPress.com アカウントを使ってコメントしています。 ログアウト /  変更 )

Google+ フォト

Google+ アカウントを使ってコメントしています。 ログアウト /  変更 )

Twitter 画像

Twitter アカウントを使ってコメントしています。 ログアウト /  変更 )

Facebook の写真

Facebook アカウントを使ってコメントしています。 ログアウト /  変更 )

%s と連携中

%d人のブロガーが「いいね」をつけました。