Skip to content
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.

Sign up for GitHub

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

Jump to bottom

refactor: lake: simplify load code #4371

Merged
merged 3 commits into from
Jun 13, 2024
Merged

refactor: lake: simplify load code #4371

merged 3 commits into from
Jun 13, 2024

Conversation

tydeu
Copy link
Member

@tydeu tydeu commented Jun 6, 2024

Simplifies the Lake dependency resolution code. Largely split from #3998.

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jun 6, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 6, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#4371
29814c2
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 6, 2024
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#4371
aaee7da
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Jun 6, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Jun 6, 2024 •
edited
Loading

Mathlib CI status (docs):

@tydeu
Copy link
Member Author

tydeu commented Jun 6, 2024

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit f4ce0be.
There were significant changes against commit 81f5b07:

  Benchmark   Metric   Change
  =======================================
+ stdlib      maxrss   -16.7% (-9116.7 σ)

@tydeu tydeu force-pushed the lake/load-refactor branch from f4ce0be to 9bb1bb0 Compare June 6, 2024 17:43
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 6, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4371
3612f76
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 6, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4371
a8f9820
@tydeu tydeu force-pushed the lake/load-refactor branch 4 times, most recently from 4b7e553 to d0ee8e1 Compare June 7, 2024 22:31
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 7, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4371
6fe7cd8
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 7, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4371
1bd30f4
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan release-ci Enable all CI checks for a PR, like is done for releases and removed builds-mathlib CI has verified that Mathlib builds against this PR labels Jun 7, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 8, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4371
01f5cd1
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 8, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4371
62d3216
@tydeu tydeu force-pushed the lake/load-refactor branch from d0ee8e1 to 0d528a6 Compare June 11, 2024 20:30
@tydeu tydeu force-pushed the lake/load-refactor branch from 0d528a6 to 401f0af Compare June 11, 2024 22:09
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 11, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4371
b6ab90c
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 11, 2024
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#4371
0775a82
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Jun 12, 2024
@tydeu tydeu marked this pull request as ready for review June 12, 2024 00:49
@tydeu
Copy link
Member Author

tydeu commented Jun 12, 2024

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 401f0af.
There were significant changes against commit ea46bf2:

  Benchmark          Metric         Change
  ====================================================
+ lake config elab   instructions    -2.5%  (-109.5 σ)
+ stdlib             dsimp           -1.7%   (-10.5 σ)
+ stdlib             maxrss         -16.3% (-1982.1 σ)

@tydeu tydeu added the will-merge-soon …unless someone speaks up label Jun 12, 2024
@tydeu tydeu added this pull request to the merge queue Jun 13, 2024
Merged via the queue into leanprover:master with commit f3274d3 Jun 13, 2024
26 checks passed
@tydeu tydeu deleted the lake/load-refactor branch June 13, 2024 16:23
@tydeu tydeu mentioned this pull request Jun 17, 2024
Merged
github-merge-queue bot pushed a commit that referenced this pull request Jun 19, 2024
@tydeu
fix: lake: visit direct deps before adding manifest entries (#4485)
bd45c0c 
Fixes a bug in #4371 where the version of a package used by a dependency
would take precedence over that of a the same package as a direct
dependency if that package had a a manifest. This was because the direct
dependency's manifest entries were added before all the direct
dependencies were visited.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
builds-mathlib CI has verified that Mathlib builds against this PR release-ci Enable all CI checks for a PR, like is done for releases toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN will-merge-soon …unless someone speaks up
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@tydeu @leanprover-community-mathlib4-bot @leanprover-bot