Lean をインストールしてみた

Lean 本体

最初，github にあるソースを自分でコンパイルしようとしたらうまくいかなかった。apt-get で入るので始めからそうすればよかった。

https://leanprover.github.io/download/ に環境ごとのインストールのしかたが書いてある。

Emacs の lean-mode

Emacs のモードがけっこうちゃんとしているみたい。インストールのしかたは https://github.com/leanprover/lean/blob/master/src/emacs/README.md に書いてある。

なんかいろんなパッケージに依存しているらしいけど，Installation のセクションの最初に書いてあるコードを何も考えずに *scratch* に貼り付けて評価したら全部勝手に入った（多分）。最近は elisp のパッケージ管理のための仕組みも整備されてきているようだけど，時代に追いつけていないのでよくわからない。

あとは，本体を apt-get で入れたので Case 2 に書いてあるやつを見て適当にいじって init.el に設定を書いた。

;;; lean-mode
(when (file-exists-p "/usr/share/emacs/site-lisp/lean/")
  (add-to-list 'load-path "/usr/share/emacs/site-lisp/lean/")
  (autoload 'lean-mode "lean-mode" nil t)
  (setq lean-rootdir "/usr")
  (add-to-list 'auto-mode-alist '("\\.h?lean$" . lean-mode)))

lean-rootdir をちゃんとセットしないと lean-mode の挙動がなんかおかしなことになった。lean のプロセスを起動してそれとやりとりしようとしてうまくいってないように見えた。

ドキュメント

https://leanprover.github.io/documentation/ に置いてある tutorial がかなり充実してそう。

まだ Chapter 4 までしか目を通していない（しかも斜め読み）けど，説明は丁寧そうなので証明支援系にそんなに慣れてなくても読めるかも。Curry-Howard 同型の説明とかもしてる。