feat: update toolchain on lake update

[tydeu]

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.

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-5684 has successfully built against this PR. (2024-10-13 00:12:09) View Log
• ✅ Mathlib branch lean-pr-testing-5684 has successfully built against this PR. (2024-10-16 04:47:57) View Log
• 🟡 Mathlib branch lean-pr-testing-5684 build against this PR was cancelled. (2024-10-16 05:49:23) View Log
• ✅ Mathlib branch lean-pr-testing-5684 has successfully built against this PR. (2024-10-16 06:24:08) View Log
• ✅ Mathlib branch lean-pr-testing-5684 has successfully built against this PR. (2024-10-17 18:14:43) View Log
• ✅ Mathlib branch lean-pr-testing-5684 has successfully built against this PR. (2024-10-17 21:26:17) View Log
• ✅ Mathlib branch lean-pr-testing-5684 has successfully built against this PR. (2024-10-17 22:59:29) View Log
• 🟡 Mathlib branch lean-pr-testing-5684 build this PR didn't complete normally. (2024-10-19 01:27:09) View Log
• 💥 Mathlib branch lean-pr-testing-5684 build failed against this PR. (2024-10-19 18:02:56) View Log
• 🟡 Mathlib branch lean-pr-testing-5684 build this PR didn't complete normally. (2024-10-19 19:07:12) View Log
• 🟡 Mathlib branch lean-pr-testing-5684 build this PR didn't complete normally. (2024-10-19 19:22:54) View Log
• ✅ Mathlib branch lean-pr-testing-5684 has successfully built against this PR. (2024-10-19 19:29:35) View Log
• ✅ Mathlib branch lean-pr-testing-5684 has successfully built against this PR. (2024-10-19 23:23:45) View Log
• ✅ Mathlib branch lean-pr-testing-5684 has successfully built against this PR. (2024-10-20 00:29:52) View Log

[tydeu]

!bench

[leanprover-bot]

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

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

[Kha]

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.