lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard
verified publisher icon leanprover

feat: update toolchain on `lake update`

Open tydeu opened this issue 1 year ago • 4 comments

Lake will now update a package's lean-toolchain file on lake 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 via elan 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:

  • Logs emitted during package and workspace loading are now eagerly printed.
  • The Elan executable used by Lake is now configurable by the ELAN environment variable.
  • The --lean CLI option was removed. Use the LEAN environment variable instead.
  • Package.deps / Package.opaqueDeps have been removed. Use findPackage? with a dependency's name instead.
  • The dependency resolver now uses a pure breadth-first traversal to resolve dependencies. It also resolves dependencies in reverse order, which is done for consistency with targets. Latter targets shadow earlier ones and latter dependencies take precedence over earlier ones. These changes mean the order of dependencies in a Lake manifest will change after the first lake update on this version of Lake.

tydeu avatar Oct 12 '24 22:10 tydeu

Mathlib CI status (docs):

leanprover-community-bot avatar Oct 13 '24 00:10 leanprover-community-bot

!bench

tydeu avatar Oct 19 '24 18:10 tydeu

Here are the benchmark results for commit 5e8b29e6def9620f042fda07e488e2cdadc38b9d. There were significant changes against commit 682173d7c084de77bd948b458ef9a7bf48bcb34e:

  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 σ)

leanprover-bot avatar Oct 19 '24 18:10 leanprover-bot

The --lean CLI option was removed. The Lean setup is now configured solely through environment variables.

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 --lean worked best for this setup of proxy scripts.

Kha avatar Oct 21 '24 08:10 Kha