idris を始めた話

date: 2025-04-12
author: Akihito Kirisaki
プログラミング
idris

最近は LLM とアイディアを色々壁打ちするのが日課になっている。そのことはまた話すとしてその中で出てきたのが Idris2 の DSL で記述された型安全な CAD といういかついアイディアである。千里の道も一歩から、偉大なプロジェクトも環境構築からである。そんなわけで Idris2 の環境構築の仕方を記しておく。

前提条件

Linux(Ubuntu 22.04)
Emacs 29

pack を導入する

pack は Idris2 のパッケージ管理ツールだ。インストールガイドを見ればインストールできる。 Chezscheme が必要なので apt で入手しておこう。

sudo apt install chezscheme

入手したあとはインストールガイドのスクリプトを実行すれば良い。結構長いので待つべし。

pack は Haskell で言うところの ghcup + cabal, Rust で言うところの rustup + cargo のようなものでこれを入れれば Idris2 本体も入ってしまう。 ~/.pack/bin と ~/.idris2/bin 以下に入るのでそれぞれパスを通しておこう。

export PATH="$HOME/.pack/bin:$HOME/.idris2/bin:$PATH"

idris2, pack で実行できたら成功だ。

planaktia on  main took 2s 
❯ idris2
     ____    __     _         ___
    /  _/___/ /____(_)____   |__ \
    / // __  / ___/ / ___/   __/ /     Version 0.7.0-6c6ee58eb
  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org
 /___/\__,_/_/  /_/____/   /____/      Type :? for help

Welcome to Idris 2.  Enjoy yourself!
Main> 
Bye for now!

planaktia on  main took 2s 
❯ pack
Usage: pack [options] <cmd> [<args>]

Options:
...

プロジェクトを開始する

プロジェクトを作るには pack new を実行すればいい。プロジェクトに必要なソースコード生成と git の初期化をしてくれる。

pack new bin hello

bin を選ぶと .ipkg というパッケージの設定ファイルに executable が設定され pack run で実行できる。

test on  master [?] 
❯ pack run
Hello from Idris2!

これでプロジェクトの設定は終わりである。ちなみに bin の代わりに lib を選ぶとライブラリ用の設定になる。が、大して変わらないのであとから手作業で直しても大丈夫だ。

Emacs の設定

エディタには Emacs を利用した。VS Code は拡張の対応が微妙らしい。とりあえず Emacs はインストールしてあるとする。 LSP 自体は pack でインストールすることができる。

pack install-app idris2-lsp

バージョンが出れば精巧である。

test on  master [?] 
❯ idris2-lsp --version
Idris2 LSP: 0.1.0-2736cd1a8
Idris2 API: 0.7.0-6c6ee58eb

続いて Emacs 自体の設定に映る。正直めんどくさかったので init.el は LLM に生成させた。lsp-mode が必要だがすでに入っているかもしれない。ない場合は以下のようにしておく。

(use-package lsp-mode
  :ensure t
  :commands lsp
  :hook ((prog-mode . lsp))
  :custom
  (lsp-completion-provider :capf)
  (read-process-output-max (* 1024 1024))
  (lsp-idle-delay 0.1)
  (lsp-headerline-breadcrumb-enable t)
  (lsp-modeline-diagnostics-enable t)
  (lsp-modeline-code-actions-enable t)
  :init
  (setq lsp-keymap-prefix "C-c l"))

(use-package lsp-ui
  :ensure t
  :commands lsp-ui-mode
  :hook (lsp-mode . lsp-ui-mode)
  :init
  (setq lsp-ui-doc-enable t)) ;; ← sideline 系の設定は不要 or 別方式に変更

use-package を使っているがこれは個々人好みとかあると思うのでよしなにしてほしい。初めてでめんどくさければ LLM に全投げじゃ。あと GUI から起動すると LSP のパスをうまく見つけられなかったりするので以下を入れておく。

(use-package exec-path-from-shell
  :ensure t
  :config
  (exec-path-from-shell-initialize))

これで先程作ったプロジェクトの src/Main.idr を開けばソースコードがハイライトされているはずだ。C-c C-z を押すと REPL が起動し下のような画面になる。

使い方はまだ自分が慣れていないので慣れた頃にまとめるかもしれない。