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