Zulip Chat Archive
Stream: new members
Topic: upgrading from lean 3 to lean 4
anton_shrdlu (Oct 12 2021 at 21:49):
Hi, I am trying to get the quickstart at https://leanprover.github.io/lean4/doc/quickstart.html going.
I ran it with standard options and everything runs fine, but when I check for version lean is still at 3.33.0
Is there some action I need to take first, if I previously installed lean 3?
I am also new to Zulip, so sorry if this is the wrong place for questions like this.
I tried to uninstall lean first via 'elan self uninstall' and got the following error message:
info: removing leanpkg home
info: removing elan binaries
error: failure during windows uninstall
info: caused by: Access is denied. (os error 5)
Scott Morrison (Oct 12 2021 at 22:52):
How are you checking the version? elan
automatically decides which version of Lean to use depending on what it sees. If you are not in a directory with either of leanpkg.toml
or a lakefile.lean
, you should not expect this to work automatically.
Scott Morrison (Oct 12 2021 at 22:53):
As lake
isn't quite ready for primetime, I would suggest you need a leanpkg.toml
file, which you can create by using leanpkg init
.
Last updated: Dec 20 2023 at 11:08 UTC