まず、以前のLeanを削除する。
- elan self uninstall
vscodeが上がってたいので、プロセスが使われている云々のエラーが出たが、アンインストールはされた。
- https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1 を何でもいいからgetして elan-init.ps1 を手に入れる。
- powershell -f elan-init.ps1 --default-toolchain leanprover/lean4:nightly としてlean4のチャネルを設定する。
オプション --default-toolchain が効かなかったようなので、elan default leanprover/lean4:nightly としてデフォルトツールチェインを設定した。設定状況は elan show で分かる。
elanを使えるようにならないとキビシイ。
