feat: update toolchain on `lake update` #5684

tydeu · 2024-10-12T22:55:36Z

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 run 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 · 2024-10-13T00:12:10Z

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
💥 Mathlib branch lean-pr-testing-5684 build failed against this PR. (2024-10-29 00:19:41) View Log
✅ Mathlib branch lean-pr-testing-5684 has successfully built against this PR. (2024-10-29 16:56:23) View Log
✅ Mathlib branch lean-pr-testing-5684 has successfully built against this PR. (2024-10-29 20:10:02) View Log
🟡 Mathlib branch lean-pr-testing-5684 build against this PR was cancelled. (2024-10-30 13:22:55) View Log
✅ Mathlib branch lean-pr-testing-5684 has successfully built against this PR. (2024-10-30 13:58:22) View Log
✅ Mathlib branch lean-pr-testing-5684 has successfully built against this PR. (2024-11-05 00:51:46) View Log

tydeu · 2024-10-19T18:02:00Z

!bench

Changes `scripts/mk_all` to run `loadWorkspace` using Lake's `toBaseIO` utility. In addition to being a bit cleaner, this adaption will also be necessary once leanprover/lean4#5684 lands.

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 leanprover#2582. Closes leanprover#2752. Closes leanprover#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 run` 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.**

Adaption for leanprover/lean4#5684. Lake's `--lean` option has been removed, so this instead environment variables (`LEAN` with `LAKE_OVERRIDE_LEAN`) to configure the benchmark's fake Lean root.

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. 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 run` 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). 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/lean4#5684 (which landed in v4.14.0-rc3) has removed the `--lean` flag for `lake`, indicating that we should use the `LEAN` environment variable instead.

Trying again, this time using [#18354](#18354).

tydeu marked this pull request as draft October 12, 2024 22:55

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Oct 12, 2024

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 12, 2024

Update lean-toolchain for testing leanprover/lean4#5684

24aff27

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 12, 2024

Update lean-toolchain for testing leanprover/lean4#5684

9e3d563

leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Oct 13, 2024

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 16, 2024

Trigger CI for leanprover/lean4#5684

b9cc21d

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 16, 2024

Trigger CI for leanprover/lean4#5684

6fb296f

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 16, 2024

Trigger CI for leanprover/lean4#5684

dbea645

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 16, 2024

Trigger CI for leanprover/lean4#5684

c8c7ea3

tydeu force-pushed the lake/update-toolchain branch from 7af30ad to 33cf999 Compare October 16, 2024 05:30

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 16, 2024

Trigger CI for leanprover/lean4#5684

915c704

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 16, 2024

Trigger CI for leanprover/lean4#5684

58a564c

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 17, 2024

Trigger CI for leanprover/lean4#5684

ec49d1f

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 17, 2024

Trigger CI for leanprover/lean4#5684

8c7ebf3

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 17, 2024

Trigger CI for leanprover/lean4#5684

bb0bf2d

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 17, 2024

Trigger CI for leanprover/lean4#5684

8836011

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 17, 2024

Trigger CI for leanprover/lean4#5684

d37bd14

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 17, 2024

Trigger CI for leanprover/lean4#5684

ba78177

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 19, 2024

Trigger CI for leanprover/lean4#5684

0579b83

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 19, 2024

Trigger CI for leanprover/lean4#5684

2572d98

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 19, 2024

Trigger CI for leanprover/lean4#5684

02970d3

tydeu marked this pull request as ready for review October 19, 2024 02:26

tydeu added the will-merge-soon …unless someone speaks up label Oct 19, 2024

tydeu mentioned this pull request Oct 19, 2024

No progress indicator for a long time when downloading a project in VSCode #5615

Closed

tydeu force-pushed the lake/update-toolchain branch from f6b5758 to 5e8b29e Compare October 19, 2024 17:40

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 19, 2024

Trigger CI for leanprover/lean4#5684

01103fe

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 19, 2024

Trigger CI for leanprover/lean4#5684

52a289f

leanprover-community-bot removed the builds-mathlib CI has verified that Mathlib builds against this PR label Oct 19, 2024

tydeu added 4 commits October 30, 2024 08:59

chore: tweak tests/clone to avoid merge conflict

386cfb5

style touchups

fbf2914

rm overzealous update message

7a3e9b4

do not override Lake with LAKE_OVERRIDE_LEAN

51bf3ea

tydeu force-pushed the lake/update-toolchain branch from 3492a53 to 51bf3ea Compare October 30, 2024 12:59

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 30, 2024

Trigger CI for leanprover/lean4#5684

198da96

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 30, 2024

Trigger CI for leanprover/lean4#5684

79d43b6

chore: rm OpaquePackage

7490611

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 1, 2024

Trigger CI for leanprover/lean4#5684

0ef92f7

tydeu added this pull request to the merge queue Nov 4, 2024

Merged via the queue into leanprover:master with commit 99070bf Nov 4, 2024
14 checks passed

tydeu deleted the lake/update-toolchain branch November 4, 2024 15:05

Kha added release-ci Enable all CI checks for a PR, like is done for releases and removed release-ci Enable all CI checks for a PR, like is done for releases labels Nov 6, 2024

tydeu mentioned this pull request Nov 8, 2024

lake update should print a warning, if moving dependencies to a later toolchain than the local toolchain #4103

Closed

kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 1, 2024

chore: update benchmark runner for leanprover/lean4#5684

13c1075

kim-em mentioned this pull request Dec 1, 2024

[Merged by Bors] - chore: update benchmark runner for leanprover/lean4#5684 leanprover-community/mathlib4#19649

Closed

kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 1, 2024

chore: update benchmark runner for leanprover/lean4#5684

349a081

mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Dec 1, 2024

chore: update benchmark runner for leanprover/lean4#5684 (#19656)

9d16cdd

Trying again, this time using [#18354](#18354).

kim-em added the changelog-lake Lake label Jan 4, 2025

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: update toolchain on `lake update` #5684

feat: update toolchain on `lake update` #5684

tydeu commented Oct 12, 2024 •

edited

Loading

leanprover-community-bot commented Oct 13, 2024 •

edited

Loading

tydeu commented Oct 19, 2024

feat: update toolchain on lake update #5684

feat: update toolchain on lake update #5684

Conversation

tydeu commented Oct 12, 2024 • edited Loading

Toolchain update details

Other changes

leanprover-community-bot commented Oct 13, 2024 • edited Loading

tydeu commented Oct 19, 2024

feat: update toolchain on `lake update` #5684

feat: update toolchain on `lake update` #5684

tydeu commented Oct 12, 2024 •

edited

Loading

leanprover-community-bot commented Oct 13, 2024 •

edited

Loading