「AI支援形式証明への道 報告-1」に書いたように、表〈おもて〉はMarkdown文書だが、裏方・黒子としてLeanファイルを使うコンテンツを考えています。
裏方の道具一式がLeanシステム／Lean環境なので、Lean（Lean 4）のインストールが必要です。最近は、VSCodeにインストールしてもらう方法がよく紹介され、推奨もされているようです。しかし、VSCodeにインストールしてもらうと、何が行われたかよく分からないままで使い始めることになるので、トラブルのときに途方に暮れるかも知れません。
次のブートストラップ手順を自分でやっておいたほうがいいんじゃないのかなー、と思います。
- インストール用スクリプト elan-init.sh などを curl で入手。
- インストール用スクリプトをシェルで実行する。
- スクリプトが elan-init というバイナリをダウンロードして実行する。
- elan, lake, lean などのコマンドが使えるようになる。
- その後のツールチェイン管理は elan により行う。
インストール用スクリプトの入手は次のようなコマンドで行います。
curl -O --location https://elan.lean-lang.org/elan-init.sh
Windows の場合は、elan-init.sh が elan-init.ps1 になります。
入手したインストール用スクリプトを sh ./elan-init.sh のように実行します。PowerShell なら & .\elan-init.ps1 です。これでうまく実行できなかったら、
powershell -ExecutionPolicy Bypass -f elan-init.ps1
を試してください。インストール用スクリプトの実行が終わればインストール完了です。
ここで重要な注意を述べると； elan やLean本体は、一般的パッケージマネージャーからもインストール可能かも知れません。しかし、一般的パッケージマネージャーでインストールするのはやめましょう。Leanツールチェインの管理がうまくいきません。
僕は、elan だけをパッケージマネージャーでインストールして、Lean本体を elan でインストールする方法をとったのですが、それでもトラブルが起きました。elan self update で失敗したのです。インストールは、専用のインストール用スクリプトを使うのが一番です。
インストールが済むと、必要なファイルはすべて ~/.elan/ の下に置かれます。実行ファイルは ~/.elan/bin/ の下です。インストール用スクリプトが環境変数 Path の設定もやってくれますが、環境変数の設定が効くタイミングはプラットフォームにより違います。場合により（Windows ですが）PCの再起動が必要かも知れません。
ツールチェインマネージャー elan は非常によくできています（Rust言語の rustup のフォークだそうです）。Leanシステムの更新と管理は、elan 一本で完全にできます。elan --help でヘルプが出るので、これをたよりに elan による管理をはじめてください。
