Skip to content

Instantly share code, notes, and snippets.

@Seasawher

Seasawher/sample.md

Created March 21, 2024 15:52
Show Gist options
  • Save Seasawher/611d70e5a87aedc5e8cb0aab5527fb72 to your computer and use it in GitHub Desktop.
Save Seasawher/611d70e5a87aedc5e8cb0aab5527fb72 to your computer and use it in GitHub Desktop.
Download ZIP
Lean4 のエラー: toolchain 'leanprover/lean4:v4.7.0-rc2' does not have the binary `~\.elan\toolchains\leanprover--lean4---v4.7.0-rc2\bin\lake.exe` への対処法
Raw
sample.md

lake update 時に表題のエラーが出て，mathlib のアップデートができないときの対処法．

以下はあくまで私の環境での一例です．

  1. 次のコマンドでツールチェインをアンインストール.
elan toolchain uninstall leanprover/lean4:v4.7.0-rc2
  1. 再びインストール．
elan toolchain install leanprover/lean4:v4.7.0-rc2
  1. もう一度 lake update を実行する
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment