κeenです。最近にわかにIdrisが話題になってるようですね。 私の知ってる範囲でIdrisの環境構築について書こうと思います。

多分話題になったのはMisreading Chatが震源地でかね。私はまだ聞いてないです。

Idrisは依存型のある汎用プログラミング言語で、Haskellっぽい雰囲気の構文を持ちます。 バックエンドはいくつかありますが、デフォルトではCが選ばれるのでおおむねネイティブコンパイルされると思ってよさそうです。他にはJavaScriptなどもあります。 Idrisそのものについてはこちらのブログを案内しておきます。 私からはインストールとかその辺を書きます。

インストール

macOSではbrewがあるようですがLinuxだとバイナリがありません。 cabalでインストールすると失敗しがちなのでstackでインストールしましょう。 だいたい以下のような感じで入ると思います。

$ git clone https://github.com/idris-lang/Idris-dev.git
$ cd Idris-dev
$ git checkout v1.3.1
$ stack build
$ stack install

Emacsの設定

idris-modeがあります。 処理系と対話しながらサポートしてくれるので中々便利です。 プログラムを書くのか証明を書くのかで結構変わりますが、 C-c C-s 、 C-c C-c 、 C-c C-a 、 C-c C-l あたりはよく使います。後述のipkgファイルもちゃんと認識してくれます。

Vimのサポートとatomのサポートもあるようなのでそちらもどうぞ。

ビルド

原始的には1ファイル単位でコンパイルすればいいのですがビルドシステムも一応あります。 ipkgファイルの書き方はあまりドキュメントがかかれてないのでこの辺とかこの辺見ながら書くとよいでしょう。

パッケージマネージャ

ない。お前がパッケージマネージャになるんだよ。

使いたいライブラリはダウンロードしてきて idris --install hoge.ipkg するとインストールされます。使うときにipkgファイルで opts = "-p hoge" とかするとリンクしてくれるので使えます。 使いたいライブラリはWikiとかから探してきましょう。

新興の elba というパッケージマネージャ/ビルドツールがありますがまだ未熟なところがあり使いづらいようです(0.2.0時点)。 具体的には既存の ipkg と互換性がない点と、登録されているパッケージを検索するインターフェースがないので何が登録されているか分からない点です。

その他

Idrisのメイン開発者がIdris 2を開発しているらしい。