-
Notifications
You must be signed in to change notification settings - Fork 415
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat: update toolchain on lake update
#5684
base: master
Are you sure you want to change the base?
Conversation
Mathlib CI status (docs):
|
7af30ad
to
33cf999
Compare
f6b5758
to
5e8b29e
Compare
!bench |
Here are the benchmark results for commit 5e8b29e. Benchmark Metric Change
===============================================
+ ilean roundtrip parse -4.5% (-14.1 σ)
- import Lean task-clock 12.0% (11.5 σ)
- import Lean wall-clock 12.0% (10.8 σ) |
Could you please check this is compatible with https://github.com/leanprover-community/mathlib4/blob/master/scripts/bench/temci-config.run.yml#L10? It's been a while but AFAIR I tried using environment variables first but |
Lake will now update a package's
lean-toolchain
file onlake update
if it finds the package's direct dependencies use a newer compatible toolchain. To skip this step, use the--keep-toolchain
CLI option.Closes #2582. Closes #2752. Closes #5615.
Toolchain update details
To determine "newest compatible" toolchain, Lake parses the toolchain listed in the packages'
lean-toolchain
files into four categories: release , nightly, PR, and other. For newness, release toolchains are compared by semantic version (e.g.,"v4.4.0" < "v4.8.0"
and"v4.6.0-rc1" < "v4.6.0"
) and nightlies are compared by date (e.g.,"nightly-2024-01-10" < "nightly-2014-10-01"
). All other toolchain types and mixtures are incompatible. If there is not a single newest toolchain, Lake will print a warning and continue updating without changing the toolchain.If Lake does find a new toolchain, Lake updates the workspace's
lean-toolchain
file accordingly and restarts the update process on the new Lake. If Elan is detected, it will spawn the new Lake process viaelan riun
with the same arguments Lake was initially run with. If Elan is missing, it will prompt the user to restart Lake manually and exit with a special error code (4).Other changes
To implement this new logic, various other refactors were needed. Here are some key highlights:
ELAN
environment variable.--lean
CLI option was removed. Use theLEAN
environment variable instead.Package.deps
/Package.opaqueDeps
have been removed. UsefindPackage?
with a dependency's name instead.lake update
on this version of Lake.