Homebrew Tap

Stream: general

[Julian Berman]

Hi! I installed Lean maybe a few months ago (via a nonstandard install in a few ways I wanted to modify) and then didn't touch it much, but am about to try again -- on macOS, it looks like the version that's in the Homebrew core repo is the 3.4.2 non-community version -- does anyone know if there's someone maintaining a tap for the community-maintained one that I can use? (If not I guess I'll try making one...)

[Alex J. Best]

The recommended install on mac is via, https://leanprover-community.github.io/install/macos.html the homebrew tap is completely outdated if you want to use mathlib at this point, as the community version is on 3.17.1. Nobody is maintaining a tap, as we use the lean specific elan to manage lean versions rather than brew.

[Julian Berman]

Got it, yeah I found that page, ok cool, will figure something out. Appreciated!

[Scott Morrison]

We're planning, starting hopefully next week, to try to remove the 3.4.2 packages in apt-get, homebrew, etc. Ideally these packages would instead install elan+leanproject, and leave it to elan to obtain Lean versions.

[Scott Morrison]

I guess we never did this (try to boot Lean 3.4.2 out of apt-get, homebrew, etc, replacing them instead with elan). Does anyone have experience with this who could take on at least one of these package managers?

[Scott Morrison]

(even if we don't replace with elan, getting rid of them would be a step forward)

[Chris Wong]

Lean doesn't seem to be in the Ubuntu repository, so we should be okay in that respect?
https://packages.ubuntu.com/search?keywords=lean&searchon=names&suite=eoan&section=all

[Chris Wong]

There was a PPA but it's gone now
https://github.com/leanprover/ppa-updater

[Chris Wong]

And the homebrew one is using the community version (3.18)
https://github.com/Homebrew/homebrew-core/blob/master/Formula/lean.rb

[Scott Morrison]

I would say that the homebrew one is not ideal. We'd like people to have elan manage their lean installation, providing whatever a leanpkg.tomlasks for.

[Julian Berman]

Probably should have came back to check on this thread for activity before putting the comment I just put on that ticket (which maybe I'll go delete), but yeah if it at all counts (which legitimately it shouldn't count for much given how new I am), I'd way rather not use elan for that personally, which is why I initially asked the question here.

[Bryan Gin-ge Chen]

Out of curiosity, why do you prefer not to use elan?

[Julian Berman]

(And again ignore me if need be :D) -- but in general I want my OS's package manager installing things, including compilers, and then use the language's package manager for installing language packages but not making arbitrary modifications to the system (this is what I do for Python, ruby, clojure, etc.)

[Reid Barton]

elan installs stuff to ~/.elan

[Julian Berman]

OK cool! That's good to know -- (two other reasons as well then just to fully list them out)

[Julian Berman]

One is quite petty but I didn't want to carefully read elan-init.sh to see what it was doing

[Julian Berman]

If there was just a self-contained pre-built thing (as e.g. proposed on that ticket -- if elan was bottled as part of Homebrew) that'd make that go away

[Reid Barton]

What ticket are you talking about?

[Julian Berman]

And the second one (also would be solved by having elan in homebrew) is that I manage all my OS packages via a Brewfile (so when I get a new machine, running brew bundle install) sets up a full development environment with all the packages I want

[Julian Berman]

Uh sorry, it's not actually linked above, my mistake. It's...

[Julian Berman]

https://github.com/Homebrew/homebrew-core/pull/59612

[Reid Barton]

I'm not really familiar with the Mac OS software ecosystem, but packaging elan (and not lean) in brew makes sense to me.

[Patrick Massot]

And then he will complain he doesn't want to use pip (or any variation on pip)...

[Julian Berman]

Hopefully none of the above is complaining!

[Julian Berman]

But as I say I'm quite fine with having a package manager manage packages for the language (I'm a python developer, so I'm quite OK with pip, and I don't want homebrew managing python packages)

[Julian Berman]

I just don't want things modifying PATH in the background, or asking to run arbitrary shell code in a shell rc (I don't know if elan does the latter? Seemed like it might, e.g. pyenv and rbenv do)

[Reid Barton]

In any case, you simply have to use elan to keep up with mathlib, or else take everything into your own hands. Otherwise, you'll be stuck after a week or two.

[Patrick Massot]

Julian, I hope you don't find this unwelcoming. People tried hard to find something easy to install which is able to keep up with the crazy pace and full backward incompatibility. But we do have some docs for people who want to understand how things fit together and bundle it their way: https://leanprover-community.github.io/toolchain.html

[Patrick Massot]

This is the best we can currently do to accommodate as many habits as we can (for instance your desire to use brew for Lean but not for python is a rather uncommon combination, I don't think we ever met it before).

[Julian Berman]

I don't find it unwelcoming at all :) -- I know I'm in that bucket (of "rolled my own". And I've read that page). I would have kept quiet too :), I just mentioned it since I saw someone else was the same kind of crazy obviously (given someone else other than me submitted that PR)

[Julian Berman]

I do the same for Python as what I'm talking about

[Julian Berman]

Homebrew installs Python, from that point forward I use Python's package manager

[Reid Barton]

Python generally doesn't release new versions of python with breaking changes every 1-2 weeks, though.

[Julian Berman]

Yeah, fair.

[Simon Hudon]

I wonder if we should package elan on brew, apt-get, chocolate, what have you, and name it lean. It's really the standard and strongly encouraged way of using Lean

[Julian Berman]

(/me -> back to actually trying to learn lean instead of cause trouble. Hopefully again none of the above is complaining, and I'm happy to come back with egg on my face if/when my setup gets me stuck.)

[Patrick Massot]

Don't worry and have fun!

[Scott Morrison]

Simon Hudon said:

I wonder if we should package elan on brew, apt-get, chocolate, what have you, and name it lean. It's really the standard and strongly encouraged way of using Lean

This sounds ideal.

[Rob Lewis]

For homebrew, is there more to this than editing https://github.com/Homebrew/homebrew-core/blob/master/Formula/lean.rb#L27 to stick in the elan install script?

[Sebastian Ullrich]

I'm not sure I'm happy with packaging elan under the name lean. It would be very confusing if updating a package named lean did not, you know, update Lean. As long as "Lean" is mentioned in the package description, and there is no other "lean" package, should that not be sufficient?

[Rob Lewis]

I'm not sure I follow -- are you proposing to delete the lean package I linked and add an elan package that mentions "Lean" in the description? That seems fine too. Anything that avoids people installing a fixed version of Lean is good.

[Rob Lewis]

As long as that current package exists, people will type brew install lean or whatever without reading anything and get confused.

[Sebastian Ullrich]

Yes, I would prefer that

[Alex Peattie]

I wonder if instead of immediately deleting the lean package whether it would be worth deprecating it with a message pointing people to run brew install elan instead. (Here's an example of a deprecated formula: https://github.com/Homebrew/homebrew-core/blob/master/Formula/acmetool.rb)

[Julian Berman]

Alex Peattie said:

I wonder if instead of immediately deleting the lean package whether it would be worth deprecating it with a message pointing people to run brew install elan instead. (Here's an example of a deprecated formula: https://github.com/Homebrew/homebrew-core/blob/master/Formula/acmetool.rb)

if it helps, according to brew analytics, the lean package has...:

==> Analytics
install: 101 (30 days), 132 (90 days), 418 (365 days)
install-on-request: 100 (30 days), 131 (90 days), 416 (365 days)
build-error: 0 (30 days)

[Julian Berman]

(Or alternatively again as a random nobody, I personally wouldn't mind no deprecation and just switching over. Homebrew is generally pretty terrible about backwards compatibility, so as a user I'm used to cursing at it for breaking something.)

[Scott Morrison]

Sebastian Ullrich said:

I'm not sure I'm happy with packaging elan under the name lean. It would be very confusing if updating a package named lean did not, you know, update Lean. As long as "Lean" is mentioned in the package description, and there is no other "lean" package, should that not be sufficient?

The problem is that currently brew install lean gives you something useless, that doesn't work with modern mathlib, because it installs some fixed version of Lean which is inevitably outdated.

[Scott Morrison]

If we made the "tap" for lean actually install elan, couldn't we arrange so that that actually updated lean (but via elan)?

[Patrick Massot]

@Sebastian Ullrich is it easy for elan to be installed globally (in something like /usr/bin) and still do its magic inside each $HOME/.lean?

[Patrick Massot]

And also, will elan be automatically able to handle Lean4 when the time will come?

[Sebastian Ullrich]

Yes, that should just work

[Sebastian Ullrich]

We're using elan for Lean 4 development right now

[Patrick Massot]

Great, thanks!

[Mario Carneiro]

Is there an easy thing to type to e.g switch mathlib to lean 4 using elan?

[Patrick Massot]

Yes, good old elan --magic-port

[Patrick Massot]

And mathlib is ported to Lean4!

[Mario Carneiro]

I mean is the install procedure more complicated than just changing the version number in mathlib

[Mario Carneiro]

obviously it won't work but I guess this would be step 0.0.1

[Sebastian Ullrich]

There is no GitHub release for elan to find automatically yet. We use local elan toolchain links.

[Patrick Massot]

Do you know why rust doesn't use, say apt or brew to install rustup globally and then let it do its magic in user space?

[Ruben Van de Velde]

My suspicion is "packagers don't like that approach"

[Sebastian Ullrich]

There is some discussion in https://github.com/rust-lang/rustup/issues/800. Looks more like "nobody volunteered to do it".

[Patrick Massot]

Indeed.

[Patrick Massot]

Are there build instructions for elan somewhere?

[Sebastian Ullrich]

I'm pretty sure it's just cargo build --release, same as for any other Rust project

[Gabriel Ebner]

Patrick Massot said:

Do you know why rust doesn't use, say apt or brew to install rustup globally and then let it do its magic in user space?

NixOS has both rustup and elan packages. ArchLinux has a rustup package.

[Adam Topaz]

In arch, at least, if I recall correctly, there is a rustc in /usr/bin which is symlinked to rustup in the same directory, which then figures everything out when you call rust.

[Sebastian Ullrich]

Yes, this is how rustup (and thus elan) works in general

[Alex Peattie]

It looks like rustup is installable via Homebrew: https://github.com/Homebrew/homebrew-core/blob/master/Formula/rustup-init.rb

I guess this could be lightly modified to make it work for elan :thinking: ?

Edit: Ah I see that it actually "installs" rustup-init, then the user has to run rustup-init to actually install rustup. So installing elan via Homebrew with this approach would mean doing:

brew install elan
elan-init

[Gabriel Ebner]

Wow, this is badly packaged. Both the arch and nixos packages work out of the box. You just have to create the right symlinks at installation time: https://github.com/NixOS/nixpkgs/blob/ade0eba99ddb4f559ce3daea2d073c92eeada5eb/pkgs/applications/science/logic/elan/default.nix#L23-L35

[Alex Peattie]

It looks like there was a proposed formula which would "just work": homebrew#9617

But it was rejected for various reasons discussed in the PR: for example, because it writes things to ~./rustup rather than the Homebrew directory... So it was replaced with homebrew#14236 instead.

I actually think it might not be worth the effort to get elan and lean playing nice in the Homebrew ecosystem, since they have much stricter rules than other package managers. I think it might be better to either:

• Delete lean from Homebrew completely, have people follow the official install procedure instead
• Keep the lean formula as is, implement something like homebrew-bump-formula to keep it always up-to-date with the latest lean (happy to help with the latter if people want to go that direction :smile: )

[Sebastian Ullrich]

Alex Peattie said:

But it was rejected for various reasons discussed in the PR: for example, because it writes things to ~./rustup rather than the Homebrew directory...

I'm not sure how you came to that conclusion, the last statement seems to say the opposite:

Ok so my position is if we can install this from source, from a stable URL, without it installing to paths that will conflict with Homebrew (i.e. not to /usr/local/bin but instead /usr/local/var or ~/.rustup) and without it having any sort of self-update features possible at runtime: I'd be fine with accepting it as then it will feel similar to rbenv and friends. It looks like to do that it should only install a single binary (rustup) and any completions/manpages but not things like rustc so it doesn't conflict.

Everything but the conflicts is already true for elan; and that part would be automatically resolved as well if we want to remove the conflicting lean package anyway.

[Sebastian Ullrich]

But all of this only makes sense if leanproject is packaged (with a dependency on elan) at the same time, doesn't it? Having just one of the tools packaged is worse than having none of them.

[Alex Peattie]

Sebastian Ullrich said:

Alex Peattie said:

But it was rejected for various reasons discussed in the PR: for example, because it writes things to ~./rustup rather than the Homebrew directory...

I'm not sure how you came to that conclusion, the last statement seems to say the opposite

Mm yes I should have been clearer, I think my understanding is that generally most tools (good Homebrew citizens) should stick to only writing to the /usr/local directory:

I'm disappointed by that, actually. Those caveats were useful if you installed (e.g.) rbenv from Homebrew expecting it to behave like a good Homebrew citizen and store its data in /usr/local. Automatically changing the default behavior of those tools could be problematic (backwards compatibility, expectations of users not familiar with Homebrew), and those caveats communicated not only that the tools were ill-behaved citizens, but how I could coerce them to behave properly.

But for some tools, like rbenv, rustup etc. they make special exceptions because they install additional binaries that could conflict with other binaries installed by Homebrew.

[Alex Peattie]

I'm not an expert though on Homebrew at all! I was just trying to understand why rustup is packaged on Homebrew the way it is, and not in an "it just works" way

[Rob Lewis]

Sebastian Ullrich said:

But all of this only makes sense if leanproject is packaged (with a dependency on elan) at the same time, doesn't it? Having just one of the tools packaged is worse than having none of them.

I think the current setup (homebrew packages one fixed version of Lean) is worse than just packaging elan, which is worse than packaging elan and leanproject. I just want to avoid the stream of people who blindly grab Lean from homebrew without reading anything, get something incompatible with the recommended workflow, and come here complaining that things don't work. At least bare elan is compatible.

[Rob Lewis]

I haven't used a mac in ages and know nothing about homebrew. If there's a reasonable way to package any part of the Lean ecosystem that doesn't conflict with installing the rest, then great. If not, then too bad. Either way the current package should probably be deleted.

[Sebastian Ullrich]

I agree, the lean package should be deleted in either case. Which might be hard to convince the Homebrew people of without providing an elan package as an alternative.

[Alexandre Rademaker]

Yes. Please one vote to have elan as a package in Homebrew before remove the Lean package

[Alexandre Rademaker]

I have been using the Lean installed with Homebrew, mainly because I am very uncomfortable with the scripts from https://leanprover-community.github.io/install/macos.html

As far as I understood, the https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/install_macos.sh will try to modify the .profile and .bash_profile files, but MacOs recently moved from bash to zsh (see https://support.apple.com/en-us/HT208050), and I am already using zsh. I had a hard time fixing all issues once I adopted zsh, and I am afraid to break things.

Then we have this script calling another script, the https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh. This second script is a little obscure. In the beginning, it says that it will just detect the OS, download and execute the installer. But I know nothing about what the installer will do. I know that it is a fork of rustup, but I never used rust.

Surely I understand that all of these points are my problems and I am very grateful for all that this community is doing!

[Johan Commelin]

@Alexandre Rademaker How does packaging elan in Homebrew change any of these considerations? It doesn't become magically more secure by doing that, right?

[Alexandre Rademaker]

Good question and thank you for asking. I was thinking about it. Homebrew makes very clear right from his homepage that

Homebrew won’t install files outside its prefix and you can place a Homebrew installation wherever you like.

Packages are installed from formulas. I am not a ruby programmer but the DSL is clean to read and we can make a good sense of what will be done.

Packages have dependencies and it means I will not have unnecessary duplications of softwares in my system (ideally).

[Johan Commelin]

Ok, that makes sense

[Bryan Gin-ge Chen]

It'd be good to see if we can either remove Lean from homebrew or change it to something which works, given that it still seems to be tripping people up. Does anyone want to take this on / know what the steps are?

[Julian Berman]

I just threw together a Homebrew formula for elan-init. I tested it builds, but can't really fully test it, because it'll only work on Intel macs. If anyone cares to give it a shot and tell me it gives you working Lean versions I can send it to the Homebrew folks for PR and see what they say. You can find it here: https://github.com/Julian/homebrew-tap/blob/master/Formula/elan-init.rb (so you can install it via brew install julian/tap/elan-init if you've got an intel mac)

[Scott Morrison]

Fails for me with:

==> Tapping julian/tap
Cloning into '/usr/local/Homebrew/Library/Taps/julian/homebrew-tap'...
remote: Enumerating objects: 112, done.
remote: Counting objects: 100% (4/4), done.
remote: Compressing objects: 100% (4/4), done.
remote: Total 112 (delta 0), reused 3 (delta 0), pack-reused 108
Receiving objects: 100% (112/112), 24.01 KiB | 1.09 MiB/s, done.
Resolving deltas: 100% (37/37), done.
Error: Invalid formula: /usr/local/Homebrew/Library/Taps/julian/homebrew-tap/Formula/libxcb.rb
libxcb: Unsupported special dependency :x11
Error: Invalid formula: /usr/local/Homebrew/Library/Taps/julian/homebrew-tap/Formula/xcb-proto.rb
xcb-proto: Unsupported special dependency :x11
Error: Invalid formula: /usr/local/Homebrew/Library/Taps/julian/homebrew-tap/Formula/xcb-util-xrm.rb
xcb-util-xrm: Unsupported special dependency :x11
Error: Cannot tap julian/tap: invalid syntax in tap!

[Julian Berman]

Ech, sorry, that's unrelated old formulas in my tap that were getting in the way. Fixed now hopefully.

[Scott Morrison]

This succeeds, but why does it want to install rust at all? Running the usual elan install script doesn't need this.

==> Tapping julian/tap
Cloning into '/usr/local/Homebrew/Library/Taps/julian/homebrew-tap'...
remote: Enumerating objects: 122, done.
remote: Counting objects: 100% (14/14), done.
remote: Compressing objects: 100% (12/12), done.
remote: Total 122 (delta 3), reused 9 (delta 2), pack-reused 108
Receiving objects: 100% (122/122), 26.47 KiB | 1.56 MiB/s, done.
Resolving deltas: 100% (40/40), done.
Tapped 9 formulae (36 files, 88.0KB).
==> Installing elan-init from julian/tap
==> Downloading https://ghcr.io/v2/homebrew/core/rust/manifests/1.51.0
######################################################################## 100.0%
==> Downloading https://ghcr.io/v2/homebrew/core/rust/blobs/sha256:d33f8c8aac0b0d6e3527048fd7f687074046d5ce2d
==> Downloading from https://pkg-containers.githubusercontent.com/ghcr1/blobs/sha256:d33f8c8aac0b0d6e3527048f
######################################################################## 100.0%
==> Downloading https://github.com/leanprover/elan/archive/v1.0.3.tar.gz
==> Downloading from https://codeload.github.com/leanprover/elan/tar.gz/v1.0.3
######################################################################## 100.0%

==> Installing dependencies for julian/tap/elan-init: rust
==> Installing julian/tap/elan-init dependency: rust
==> Pouring rust--1.51.0.mojave.bottle.tar.gz
==> Caveats
Bash completion has been installed to:
  /usr/local/etc/bash_completion.d
==> Summary
🍺  /usr/local/Cellar/rust/1.51.0: 20,186 files, 695.4MB
==> Installing julian/tap/elan-init
==> cargo install --features no-self-update
🍺  /usr/local/Cellar/elan-init/1.0.3: 10 files, 5MB, built in 1 minute 5 seconds
==> Caveats
==> rust
Bash completion has been installed to:
  /usr/local/etc/bash_completion.d

[Scott Morrison]

Also, this doesn't actually give me elan or lean:

idaeus:~ scott$ lean
-bash: lean: command not found
idaeus:~ scott$ elan
-bash: elan: command not found

[Julian Berman]

The only thing it gives you is elan-init -- that's how I see the rustup formula works, they don't package rustup, they package rustup-init

[Julian Berman]

(It installs rust because that's a dependency for building elan-init, but if/when there are homebrew bottles, that wouldn't be needed for users who install elan-init)

[Julian Berman]

But if you have suggestions for a different way I should do this let me know obviously

[Gabriel Ebner]

You just need to make symlinks for lean, etc. Then it will work out of the box: https://github.com/NixOS/nixpkgs/blob/838e396944e3d9fe16faf155c6bf869f85f924d0/pkgs/applications/science/logic/elan/default.nix#L45-L61

[Julian Berman]

Oh, cool! I see.

[Julian Berman]

I see that nix expression doesn't set RELEASE_TARGET_NAME right? How come it doesn't need to? For me elan wouldn't build if I didn't set it (to a junk value), even though it doesn't look like it uses that at all except for naming the releases in GH

[Julian Berman]

OK made that tweak, so now symlinks to all those are created automatically. @Scott Morrison if I trouble you a last time hopefully for feedback.

[Scott Morrison]

Seems to work!

[Scott Morrison]

(Can we rename it to just elan, given that now we don't expect people to run elan-init?)

[Julian Berman]

Yeah that will be easy, when I submit it, I'll add aliases to the formula for both elan and lean

[Julian Berman]

(And then try to convince them to remove the lean formula)

[Julian Berman]

https://github.com/Homebrew/homebrew-core/pull/77349 (especially if anyone has suggestions for how to word the recommendation to use elan)

[Julian Berman]

There's an existing formula I see called elan (a cask technically). Hopefully that won't be an issue.

[Gabriel Ebner]

* GitHub repository not notable enough (<30 forks, <30 watchers and <75 stars)

:rofl: You might also want to remove the left-over reference to elan-init

[Julian Berman]

As in rename the formula fully to elan rather than just aliasing it to that?

[Julian Berman]

I can do that (somehow I guess I thought that may make the cask conflict issue more of a big deal) but yeah let me know.

[Sebastian Ullrich]

Sounds like y'all should star the heck out of elan

[Kevin Buzzard]

Is there a link?

[Bryan Gin-ge Chen]

https://github.com/leanprover/elan

[Patrick Massot]

73 stars, we're almost there

[Johan Commelin]

you got my star

[Julian Berman]

I don't think this matters, the person just reviewed and didn't really bring it up (but yeah feel free to star regardless :P)

[Floris van Doorn]

And we reached 75 :)

[Julian Berman]

https://github.com/Homebrew/homebrew-core/pull/77349#issuecomment-841691253 not looking like they'll want to remove the lean formula

[Julian Berman]

OK, this is merged, so brew install elan should work now. Also brew install mathlibtools should work in a few minutes, so you should be able to get a fully working env from brew install elan mathlibtools, albeit just on Intel macs. They did not on the other hand want to remove the lean formula (I kind of expected that personally), so users may still end up doing that, but yeah at least there's a working setup one can get via Homebrew?

[Johan Commelin]

So brew uninstall lean; brew install elan mathlibtools is the default troubleshooting responce for Macs? :rofl: sounds good
Thanks a lot for your effort!

[Johan Commelin]

Does mathlibtools depend on elan? I guess that would make sense

[Julian Berman]

It does yeah, so technically just brew install mathlibtools works, but yeah adding elan doesn't hurt.

[Scott Morrison]

Thanks for this! We should include this in the installation instructions: could you make a PR for this?

[Carlo Cabrera]

Hi Julian! Thanks for getting elan into Homebrew/core. I had looked into it before, but the notability check got in the way :)