Opened 9 months ago
Last modified 9 months ago
#69345 assigned update
lean: Update to Lean 4
Reported by: | szhorvat (Szabolcs Horvát) | Owned by: | kakuhen |
---|---|---|---|
Priority: | Normal | Milestone: | |
Component: | ports | Version: | |
Keywords: | Cc: | ||
Port: | lean |
Description
Please update the lean
port to Lean 4, or alternatively provide Lean 4 through a new port.
The official Lean installation instructions suggest executing a shell script directly from GitHub, which then proceeds to install Homebrew, and thus doesn't play well with an existing MacPorts installation. Installing Lean would be much easier for MacPorts users if it were provided as a port.
Change History (2)
comment:1 Changed 9 months ago by szhorvat (Szabolcs Horvát)
Type: | defect → update |
---|
comment:2 Changed 9 months ago by ryandesign (Ryan Carsten Schmidt)
Cc: | kakuhen removed |
---|---|
Owner: | set to kakuhen |
Status: | new → assigned |
Summary: | Lean: Update to Lean 4 → lean: Update to Lean 4 |
Note: See
TracTickets for help on using
tickets.
Looks like their shell script installs Homebrew, configures it to add a non-standard collection of formulas, uses that to install Microsoft Visual Studio Code, and then uses VS Code to install lean 4. Obviously a MacPorts port won't be doing any of those things. We build from source.
The lean port is currently downloading from https://github.com/leanprover-community/lean at which the latest version is 3.51.1. The port could probably be updated to that version easily.
The README there says:
where "Lean 4" is a link to the main lean web site which, if you look for a source download link, leads to https://github.com/leanprover/lean4 at which the latest version is 4.5.0. So your request to update to version 4 is a request to switch from the community edition to the official version. I don't know how much effort is involved in doing that or what the differences between the editions are or why this port has always used the community edition instead of the official version but presumably there was a reason.