コンテンツにスキップ

確認チェックリスト

ローカルに環境が準備できていることを確認するためのリストです． まず

したあとに，以下のリストで足りないものを確認してください．

作業フォルダ

A. 基本コマンド

ターミナルを新しく開いて確認します．

git --version
curl --version
code --version
elan --version
lean --version
lake --version

チェック:

  • git --version が表示される
  • curl --version が表示される
  • code --version が表示される
  • elan --version が表示される
  • lean --version が表示される
  • lake --version が表示される

動かない場合:

lake がないと言われる場合

OS のパッケージマネージャで別の lake や elan を入れようとしないでください．Lean 公式の elan が PATH に入っているかを確認します．

B. GitHub CLI

GitHub CLI を使う場合だけ確認します．

gh --version
gh auth status
gh config get git_protocol

チェック:

  • gh --version が表示される
  • gh auth status でログイン済みと表示される
  • gh config get git_protocol が https になっている

動かない場合:

C. 講義用リポジトリ

以下では例として作業フォルダを LeanProjects とする．

確認コマンド:

Windows PowerShell:

cd C:\LeanProjects\lean-math-note
Get-ChildItem
Get-Content lean-toolchain

macOS / Linux:

cd ~/LeanProjects/lean-math-note
ls
cat lean-toolchain

チェック:

  • 作業フォルダが存在する
  • lean-toolchain がある
  • lakefile.toml または lakefile.lean がある
  • lake-manifest.json がある

動かない場合:

Lean

D. プロジェクトの Lean バージョン

プロジェクトルートで実行します

elan show
lean --version
lake --version

成功時メッセージ例 

# 成功時メッセージ例（elan）
# active toolchain
# ----------------
# leanprover/lean4:v4.30.0 (overridden by '/Users/shosonoda/work/temp/temp-math-mdgen/lean-toolchain')
# Lean (version 4.30.0, arm64-apple-darwin24.6.0, commit d024af099ca4bf2c86f649261ebf59565dc8c622, Release)
#
# 成功時メッセージ例（lean）
# Lean (version 4.30.0, arm64-apple-darwin24.6.0, commit d024af099ca4bf2c86f649261ebf59565dc8c622, Release)
#
# 成功時メッセージ例（lake）
# Lake version 5.0.0-src+d024af0 (Lean version 4.30.0)

チェック:

  • elan show の active toolchain が，このフォルダの lean-toolchain に対応している
  • lean --version が表示される
  • lake --version が表示される

動かない場合:

E. Mathlib キャッシュ取得

lake exe cache get

成功時メッセージ例（数値は変動する） 

# Completed successfully in 44928 ms!

チェック:

  • エラーで止まらない
  • .lake フォルダができている
  • 途中でネットワークエラー，認証エラー，SSH エラーが出ない
  • Completed successfully という成功メッセージが出る

動かない場合:

F. ビルド

lake build
成功時メッセージ（数値は変動する） 
# Build completed successfully (8479 jobs).

チェック:

  • lake build がエラーなく終了する
  • Build completed successfully という成功メッセージが出る
  • Mathlib 全体を何時間もビルドし始めていない

動かない場合:

長時間ビルドになったら

lake exe cache get が失敗している，またはキャッシュが正しく展開されていない可能性があります．無理に数時間待つ前に，リカバリー手順の「キャッシュを取り直す」を試します．

VS Code

G. VS Code

プロジェクトルート（~/LeanProjects/lean-math-note/ 直下）で:

code .

実行例: VS Code + Lean InfoView で test.lean を開いた例

チェック:

  • VS Code が起動して lean-math-note フォルダを直接開いている．親フォルダ（LeanProjects）ではない．
  • Lean 4 拡張機能が有効（操作コマンドに ∀ ボタンが出る）
  • 適当な .lean ファイルを開くと右側に Lean Infoview が出る
  • import Mathlib がエラーにならない
  • #eval 1 + 1 の結果が見える

動かない場合:

H. Markdown プレビュー

この機能は必須ではありませんが， .md ファイルを編集する際に便利です．

チェック:

  • README.md を開ける
  • Windows/Linux で Ctrl+Shift+V，macOS で Cmd+Shift+V によりプレビューが表示される
  • Markdown: Open Preview to the Side が使える

動かない場合:

実行例: VS Code + Markdown Preview で README.md を開いた例