リカバリー手順書¶

ここでは，環境構築でよくある失敗と復旧手順をまとめます．

まず大原則です．

エラーメッセージを消す前にコピーまたはスクリーンショットを保存する．
いきなり全部を再インストールしない．
プロジェクトルート，つまり lean-toolchain と lakefile.toml があるフォルダで実行しているか確認する．
Windows では，ターミナルを閉じて開き直すだけで PATH 問題が直ることがあります．

0. `git`, `curl`, `code` が見つからない¶

症状:

git: command not found
curl: command not found
code: command not found

または Windows で:

'git' is not recognized as an internal or external command
'curl' is not recognized as an internal or external command
'code' is not recognized as an internal or external command

対処:

ターミナルを閉じて開き直す．
git / curl は作業マニュアル 2 に戻る．
code は作業マニュアル 1 に戻る．

Windows で code だけ見つからない場合は，VS Code を起動してコマンドパレットから Shell Command: Install 'code' command in PATH を実行するか，インストール時の Add to PATH 設定を確認してください．

急ぐ場合は，code . の代わりに VS Code の File > Open Folder... からプロジェクトフォルダを開いてください．

1. `gh` が見つからない¶

症状:

gh: command not found

または:

'gh' is not recognized as an internal or external command

対処:

GitHub CLI をインストールする．
ターミナルを閉じて開き直す．
次を確認する．

gh --version

急ぐ場合は，GitHub CLI を使わずに HTTPS で clone します．

git clone https://github.com/shosonoda/lean-math-note.git

2. GitHub の SSH まわりで失敗する¶

症状の例:

Permission denied (publickey).
Could not read from remote repository.
Host key verification failed.

講義では SSH を使わず，HTTPS に寄せるのが簡単です．

2.1 GitHub CLI のプロトコルを HTTPS にする¶

gh config set git_protocol https
gh auth login

ログイン時に次を選びます．

GitHub.com
HTTPS
Authenticate Git with your GitHub credentials: Yes

確認:

gh config get git_protocol
gh auth status

2.2 clone 済みリポジトリの remote を HTTPS に変える¶

プロジェクトフォルダで:

git remote -v

git@github.com:... のように SSH になっていたら，HTTPS に変えます．

git remote set-url origin https://github.com/shosonoda/lean-math-note.git
git remote -v

2.3 Git の global 設定で HTTPS が SSH に書き換えられていないか見る¶

一部の環境では，HTTPS URL を自動で SSH に書き換える設定が入っていることがあります．

git config --global --get-regexp url

insteadOf で GitHub の URL が SSH に書き換えられている場合は，講師に相談してください．自分で消す場合は，消す対象を必ず確認してから行います．

例:

git config --global --unset-all url.git@github.com:.insteadof

設定削除は慎重に

研究室や会社の PC では，Git 設定が意図的に管理されていることがあります．共有 PC や管理 PC では勝手に削除せず，管理者または講師に確認してください．

3. `elan`, `lean`, `lake` が見つからない¶

症状:

elan: command not found
lean: command not found
lake: command not found

または Windows で:

'elan' is not recognized as an internal or external command

3.1 まずターミナルを開き直す¶

インストール直後は PATH が反映されていないことがあります．ターミナルを完全に閉じて，新しく開いてください．

確認:

Windows:

where elan
where lean
where lake

macOS / Linux:

which elan
which lean
which lake

3.2 Windows で手動インストールする¶

PowerShell または Command Prompt で:

curl -O --location https://elan.lean-lang.org/elan-init.ps1
powershell -ExecutionPolicy Bypass -f elan-init.ps1
del elan-init.ps1

選択肢が出たら 1 を選びます．

終わったらターミナルを開き直し，確認します．

elan --version
lean --version
lake --version

3.3 `curl` も PowerShell スクリプトも失敗する場合¶

ブラウザから手動でインストーラを入れる方法があります．

ブラウザで https://github.com/leanprover/elan/releases を開く．
最新リリースを開く．
Windows なら x86_64-pc-windows-msvc を含む zip を選ぶ．
zip を展開する．
中にある elan-init.exe を実行する．
画面の指示に従い，通常は 1 を入力する．
ターミナルを開き直して確認する．

elan --version
lean --version
lake --version

ARM Windows の場合

ARM 版 Windows など特殊な環境では，ファイル名が異なる場合があります．リリースページで自分の OS / CPU に合ったものを選んでください．

4. `lake exe cache get` が失敗する¶

症状の例:

error: external command ... exited with code ...
network error
could not resolve host
SSL certificate problem
Permission denied (publickey)

4.1 プロジェクトルートにいるか確認する¶

Windows:

Get-ChildItem
Get-Content lean-toolchain

macOS / Linux:

ls
cat lean-toolchain

lean-toolchain と lakefile.toml が見えない場合，フォルダが違います．

4.2 ネットワークを確認する¶

curl -I https://github.com
curl -I https://elan.lean-lang.org/elan-init.ps1

大学・会社・公共 Wi-Fi では，GitHub や外部バイナリのダウンロードが制限されることがあります．可能なら別回線，テザリング，またはプロキシ設定を確認してください．

4.3 SSH エラーなら HTTPS に寄せる¶

このページの「GitHub の SSH まわりで失敗する」を実行します．

4.4 キャッシュを取り直す¶

まず軽い復旧から試します．

lake clean
lake exe cache get!
lake build

get! は，ローカルに既にあると見なされているキャッシュも取り直すためのコマンドです．

5. `lake build` が Mathlib を長時間ビルドし始める¶

症状:

PC のファンが回り続ける．
Mathlib... が大量にビルドされる．
何十分も終わらない．

原因候補:

lake exe cache get が失敗していた．
キャッシュの展開に失敗していた．
.lake が古い状態のまま残っている．

対処:

lake clean
lake exe cache get!
lake build

まだダメなら .lake を削除します．

Windows PowerShell:

Remove-Item -Recurse -Force .lake
lake exe cache get
lake build

Windows Command Prompt:

rmdir /s /q .lake
lake exe cache get
lake build

macOS / Linux:

rm -rf .lake
lake exe cache get
lake build

6. Lean / Mathlib のバージョン違いで壊れる¶

症状の例:

unknown package
unknown module prefix 'Mathlib'
invalid manifest
package configuration has changed
error: toolchain ... does not have the binary ... lake

6.1 勝手に `lean-toolchain` を変えない¶

Lean プロジェクトでは，lean-toolchain がそのプロジェクトの Lean バージョンを指定します．

講義用リポジトリでは，受講者が elan default stable や lean-toolchain の編集で直そうとすると，逆に壊れることがあります．

まず，配布リポジトリの状態に戻します．

git status --short
git restore lean-toolchain lakefile.toml lake-manifest.json
git pull

git restore が失敗する場合は，変更を講師に見せてください．

6.2 `.lake` を消して取り直す¶

lake clean

それでもダメなら:

Windows PowerShell:

Remove-Item -Recurse -Force .lake
lake exe cache get
lake build

macOS / Linux:

rm -rf .lake
lake exe cache get
lake build

6.3 `lake-manifest.json` について¶

lake-manifest.json は，単なる一時キャッシュではなく，依存パッケージのバージョンを固定する重要ファイルです．

講義用リポジトリでは，原則として受講者が削除・再生成しない方が安全です．講師から「manifest を再生成してください」と指示があった場合だけ，次を実行します．

rm -f lake-manifest.json
lake update
lake exe cache get
lake build

Windows PowerShell の場合:

Remove-Item -Force lake-manifest.json
lake update
lake exe cache get
lake build

lake update の意味

lake update は依存関係を更新します．プロジェクトの状態が講義用の固定状態から変わる可能性があります．受講者個人の判断ではなく，講師の指示で実行してください．

6.4 Lean toolchain 自体が壊れている場合¶

lean-toolchain の中身を確認します．

Windows:

Get-Content lean-toolchain

macOS / Linux:

cat lean-toolchain

例えば leanprover/lean4:v4.xx.x のような文字列が出ます．

その toolchain を入れ直します．以下の <TOOLCHAIN> を実際の文字列に置き換えてください．

elan toolchain uninstall <TOOLCHAIN>
elan toolchain install <TOOLCHAIN>
lake build

7. VS Code で Lean が動かない¶

症状:

.lean ファイルがただのテキストとして開く．
Lean Infoview が出ない．
import Mathlib が赤い．
コマンドラインでは lake build が成功するのに VS Code だけ失敗する．

対処:

VS Code で開いているフォルダがプロジェクトルートか確認する．
正: lean-math-note
誤: その親フォルダ LeanProjects
File > Open Folder... で lean-math-note を開き直す．
Trust authors を選ぶ．
.lean ファイルを開く．
コマンドパレットで Lean 4: Restart File を実行する．
それでもダメなら VS Code を再起動する．

確認用ファイル:

import Mathlib

#eval 1 + 1

example : 1 + 1 = 2 := by
  norm_num

8. Markdown プレビューが開かない¶

症状:

.md ファイルがプレビューできない．
ショートカットが効かない．

対処:

.md ファイルを VS Code で開く．
コマンドパレットを開く．
Markdown: Open Preview to the Side を実行する．
それでもダメなら VS Code を再起動する．
必要なら Markdown All in One 拡張機能を入れる．

9. それでも直らない場合の最小再構築¶

講義中に時間がない場合は，プロジェクトだけを作り直すのが早いことがあります．

cd C:\LeanProjects
ren lean-math-note lean-math-note-broken

git clone https://github.com/shosonoda/lean-math-note.git
cd lean-math-note
lake exe cache get
lake build
code .

macOS / Linux:

cd ~/LeanProjects
mv lean-math-note lean-math-note-broken

git clone https://github.com/shosonoda/lean-math-note.git
cd lean-math-note
lake exe cache get
lake build
code .

壊れたフォルダは後で調査できます．作業中のファイルがある場合は，削除せずリネームしてください．

10. Codespaces を利用する¶

ローカル PC の復旧が講義時間内に間に合わない場合は，GitHub Codespaces を使ってブラウザ上の VS Code で作業できます．

手順は Codespaces 利用手順を見てください．

注意点:

GitHub アカウントが必要です．
ローカル PC の Lean / VS Code インストール状態には依存しません．
使い終わった codespace は停止または削除してください．

リカバリー手順書¶

0. git, curl, code が見つからない¶

1. gh が見つからない¶

2. GitHub の SSH まわりで失敗する¶

2.1 GitHub CLI のプロトコルを HTTPS にする¶

2.2 clone 済みリポジトリの remote を HTTPS に変える¶

2.3 Git の global 設定で HTTPS が SSH に書き換えられていないか見る¶

3. elan, lean, lake が見つからない¶

3.1 まずターミナルを開き直す¶

3.2 Windows で手動インストールする¶

3.3 curl も PowerShell スクリプトも失敗する場合¶

4. lake exe cache get が失敗する¶

4.1 プロジェクトルートにいるか確認する¶

4.2 ネットワークを確認する¶

4.3 SSH エラーなら HTTPS に寄せる¶

4.4 キャッシュを取り直す¶

5. lake build が Mathlib を長時間ビルドし始める¶

6. Lean / Mathlib のバージョン違いで壊れる¶

6.1 勝手に lean-toolchain を変えない¶

6.2 .lake を消して取り直す¶

6.3 lake-manifest.json について¶

6.4 Lean toolchain 自体が壊れている場合¶

7. VS Code で Lean が動かない¶

8. Markdown プレビューが開かない¶

9. それでも直らない場合の最小再構築¶

10. Codespaces を利用する¶

0. `git`, `curl`, `code` が見つからない¶

1. `gh` が見つからない¶

3. `elan`, `lean`, `lake` が見つからない¶

3.3 `curl` も PowerShell スクリプトも失敗する場合¶

4. `lake exe cache get` が失敗する¶

5. `lake build` が Mathlib を長時間ビルドし始める¶

6.1 勝手に `lean-toolchain` を変えない¶

6.2 `.lake` を消して取り直す¶

6.3 `lake-manifest.json` について¶