Leanのファイル配置、環境変数など

Lean メモ

以下は、$USERPROFILE/.elan/toolchains/stable/bin/leanpkg.bat

@ECHO OFF

SET LEANDIR=%~dp0%../
SET LIBDIR=%LEANDIR%\lib\lean
IF NOT EXIST "%LIBDIR%" SET LIBDIR=%LEANDIR%
SET LEAN_PATH=%LIBDIR%\library;%LIBDIR%\leanpkg
SET PATH=%LEANDIR%\bin;%PATH%

lean --run "%LIBDIR%\leanpkg\leanpkg\main.lean" %*

色々分かる。

使っている環境変数は：

  1. LEANDIR
  2. LIBDIR
  3. LEAN_PATH

LEANDIRは $USERPROFILE/.elan/toolchains/stable/、LEAN_PATHは $USERPROFILE/.elan/toolchains/stable/lib/lean/library ; $USERPROFILE/.elan/toolchains/stable/lib/lean/leanpkg （空白は取る）。

LEAN_PATHはディレクトリのリストで、各ディレクトリはライブラリ形式で、直下に名前空間ディレクトリが置かれる。他に、leanpkg.toml と文書（Markdownファイル）も置かれる。.lean と .olean は同じディレクトリに置かれる。新しいコンパイル済み形式ができても対応できる、例えば、.olean2 。

lenaコマンド（実体は、$USERPROFILE/.elan//toolchains/stable/bin/lean.exe）は、どうやらコマンドライン・フロントエンドのようだ。これは使えるし、使っているとLeanの構造が分かる。lean --run でLeanプログラムのエントリーポイントである main を実行する。

つまり、OSコマンド lenapkg は、Leanで実装されている。ドキュメントは https://leanprover.github.io/reference/using_lean.html#using-the-package-manager