VS Code を使わずに Lean と相互作用する

VS Code 拡張は Lean language server の使いやすいフロントエンドです． しかし，Lean 自体はコマンドラインからも使えます．

このプロジェクトでは，まず lake env を付けるのが安全です． これにより，Mathlib など，Lake workspace の依存関係を含んだ環境で lean が起動します．

lake env lean LeanMathNote/basic/chapter06.lean
lake lean LeanMathNote/basic/chapter06.lean
lake build

lean に直接入力を渡すこともできます．

printf '#check Nat\n#eval 2 + 3\n' | lake env lean --stdin

エラーや情報を機械可読にしたい場合は --json が使えます．

lake env lean --json LeanMathNote/basic/chapter06.lean

language server をエディタなしで起動するには次を使います．

lake serve
lake env lean --server

lean --server は LSP クライアントと通信するためのモードです． 人間が直接対話する REPL というより，エディタや外部ツールが Lean と通信するための入口です．

便利な調査コマンドもあります．

lake env lean --deps LeanMathNote/basic/chapter06.lean
lake env lean --src-deps LeanMathNote/basic/chapter06.lean
lake env lean --profile LeanMathNote/basic/chapter06.lean
lean --print-prefix
lean --print-libdir
lake query LeanMathNote

--deps は import されるモジュールの依存関係を調べます． --profile は定義や定理ごとの処理時間を見ます． --print-prefix と --print-libdir は，現在の Lean toolchain がどこにあるかを確認します．