🥯
lake update 時に toolchain does not have the binary というエラーが出たときの対処例
あらまし
既存プロジェクトの Lean のバージョンと mathlib のバージョンを更新しようとして，lake update を実行したところ，以下のようなエラーが出ました．
toolchain 'leanprover/lean4:v4.7.0-rc2' does not have the binary
~\.elan\toolchains\leanprover--lean4---v4.7.0-rc2\bin\lake.exe
解決策の例
まず，次のコマンドでツールチェインをアンインストールします．これは，既にインストールされているツールチェインに問題があるかもしれないので，それを解消するためです．
elan toolchain uninstall leanprover/lean4:v4.7.0-rc2
次に，以下のコマンドで再インストールします．
elan toolchain install leanprover/lean4:v4.7.0-rc2
終わったら，再度 lake update を実行します．以上です．
Discussion