elan not updating

Stream: general

[Bolton Bailey]

Every time I open mathlib, I get a pop-up saying

Lean's version manager Elan is outdated: the installed version is 1.4.2, but a version of 3.1.1 is recommended. Do you want to update Elan?

But when I run the following commands I get this. Why is elan not updating itself?

$ elan update
info: syncing channel updates for 'stable'
info: latest update on stable, lean version v3.51.1
info: syncing channel updates for 'nightly'
info: latest update on nightly, lean version nightly-2024-06-05
info: syncing channel updates for 'stable'
info: latest update on stable, lean version v4.8.0

                    stable unchanged - Lean (version 3.51.1, commit cce7990ea86a, Release)
  leanprover/lean4:nightly unchanged - Lean (version 4.9.0-nightly-2024-06-05, x86_64-apple-darwin22.6.0, commit fbb3055f82ff, Release)
   leanprover/lean4:stable unchanged - Lean (version 4.8.0, x86_64-apple-darwin22.6.0, commit df668f00e6c0, Release)

$ elan --version
elan 1.4.2 ( )

[Jannis Limperg]

Run elan self update.

[Bolton Bailey]

error: self-update is disabled for this build of elan
error: you should probably use your system package manager to update elan

[Bolton Bailey]

(Let me try that instead)

[Bolton Bailey]

brew upgrade elan                                                                     ✔  14:02:36 
Running `brew update --auto-update`...
==> Downloading https://ghcr.io/v2/homebrew/portable-ruby/portable-ruby/blobs/sha256:bbb73a9d86fa37128c54c74b020096a646c46c525fd5eb0c4a2467551fb2d377
############################################################################################################# 100.0%
==> Pouring portable-ruby-3.3.2.arm64_big_sur.bottle.tar.gz
Warning: Treating elan as a formula. For the cask, use homebrew/cask/elan or specify the `--cask` flag.
Error: elan not installed

[Bolton Bailey]

This seems pretty cursed, is there a way to simply uninstall elan and start over?

[Sebastian Ullrich]

It's elan-init on brew. Not our fault.

[Bolton Bailey]

brew upgrade elan-init gives me
Error: elan-init not installed

[Utensil Song]

You might need to brew uninstall elan-init then follow https://github.com/leanprover/elan?tab=readme-ov-file#manual-installation.

Maybe the section Homebrew should be removed from elan official README if it's not recommended.

[Utensil Song]

Generally repackaged elan/lean are not recommended (at least on Zulip), as others cannot help with extra issues caused by repackaging.

[Bolton Bailey]

Ok brew uninstalling seems not to work, should I just proceed with manual installation?

> brew uninstall elan-init
Error: No such keg: /opt/homebrew/Cellar/elan-init                         /1.6s

[Matthew Ballard]

which elan?

[Bolton Bailey]

> curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
shell-init: error retrieving current directory: getcwd: cannot access parent directories: Operation not permitted
info: downloading installer
chdir: error retrieving current directory: getcwd: cannot access parent directories: Operation not permitted
error: it looks like you have an existing installation of Lean at:
error: /usr/local/bin
error: elan cannot be installed alongside Lean. Please uninstall first
error: if this is what you want, restart the installation with `-y'
error: cannot install while Lean is installed                              /1.7s

!w ~/.elan ................................................... err 0|1 14:24:55
> which elan
/usr/local/bin/elan                                                        /0.0s

[Bolton Bailey]

should I nuke that too?

[Matthew Ballard]

MacOS?

[Matthew Ballard]

I am struggling to remember an install path that lands there

[Matthew Ballard]

M1,2,3?

[Bolton Bailey]

M2

[Matthew Ballard]

Ok, you must have a rosetta installed copy of homebrew

[Bolton Bailey]

Sounds likely

[Bhavik Mehta]

Utensil Song said:

Generally repackaged elan/lean are not recommended (at least on Zulip), as others cannot help with extra issues caused by repackaging.

Note that the community website recommends installing elan from brew for MacOS: https://leanprover-community.github.io/install/macos.html

[Bolton Bailey]

Note that this rosetta stuff I did was over a year ago. Also, I should mention I recently migrated my data from an M1

[Matthew Ballard]

arch -x86_64 /usr/local/bin/brew uninstall elan-init?

[Matthew Ballard]

I can't remember the flag you have to throw at it

[Bolton Bailey]

Seems to have worked, finally. Thanks!

> arch -x86_64 /usr/local/bin/brew uninstall elan-init
Uninstalling /usr/local/Cellar/elan-init/1.4.2... (20 files, 5.3MB)        /5.8s

!w /usr ........................................................... 6s 14:31:34
> which elan
elan not found                                                             /0.0s

[Matthew Ballard]

I would remove that copy of rosetta-based homebrew at some point but you can now proceed to reinstall elan

[Matthew Ballard]

(Hmm... I might still my rosetta based homebrew sitting on my machine...)

[Bolton Bailey]

> which brew
/opt/homebrew/bin/brew

So I think I'm not too scared of invoking it by mistake

[Matthew Ballard]

Yeah, I still have mine. You are very unlikely to trip over it unless you have already installed through it

[Matthew Ballard]

Bhavik Mehta said:

Utensil Song said:

Generally repackaged elan/lean are not recommended (at least on Zulip), as others cannot help with extra issues caused by repackaging.

Note that the community website recommends installing elan from brew for MacOS: https://leanprover-community.github.io/install/macos.html

You mean this: https://leanprover-community.github.io/install/macos_details.html right?

[Bhavik Mehta]

Matthew Ballard said:

Bhavik Mehta said:

Utensil Song said:

Generally repackaged elan/lean are not recommended (at least on Zulip), as others cannot help with extra issues caused by repackaging.

Note that the community website recommends installing elan from brew for MacOS: https://leanprover-community.github.io/install/macos.html

You mean this: https://leanprover-community.github.io/install/macos_details.html right?

I mean the link that I sent, as well as your link. They both recommend using brew. In fact, in the one I mentioned, it installs brew if you don't have it.

[Matthew Ballard]

Ah! I just thought the command was the elan-sanctioned one

[Matthew Ballard]

Didn't even read it

[Matthew Ballard]

#13967

[Shreyas Srinivas]

In general, if you migrated to an apple silicon mac, please purge brew out of the system and reinstall it.

[Matthew Ballard]

leanprover.github.io#493

[Kyle Miller]

I've had this problem on an M2 mac as well, and I just got around to fixing it. My method was to brew uninstall elan-init and then use then "reload window" in VS Code to trigger getting the Lean extension to reinstall elan for me (which just runs the https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh script as seen in the instructions at https://github.com/leanprover/elan).