Skip to content

Conversation

@tydeu
Copy link
Member

@tydeu tydeu commented Jun 14, 2025

This PR aims to reintegrate lean --setup with Lake fix its performance issues. (WIP)

Reverts #8736 and reimplements #8447.

@tydeu tydeu added the changelog-lake Lake label Jun 14, 2025
@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 14, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-06-12 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-14 20:34:30)

@tydeu
Copy link
Member Author

tydeu commented Jun 14, 2025

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit e36dff1.
There were significant changes against commit faffe86:

  Benchmark          Metric                  Change
  ===========================================================
- lake build no-op   instructions             22.8%  (39.2 σ)
- lake build no-op   task-clock              634.9%  (48.0 σ)
- lake build no-op   wall-clock               19.1%  (27.3 σ)
+ stdlib             attribute application    -1.5% (-48.6 σ)
- stdlib             dsimp                     3.3%  (24.2 σ)

@tydeu tydeu force-pushed the lake/setup-perf branch from e36dff1 to e8353be Compare June 16, 2025 14:39
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 16, 2025
@tydeu
Copy link
Member Author

tydeu commented Jun 16, 2025

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 8e1dd6a.
There were significant changes against commit 957b904:

  Benchmark          Metric         Change
  =================================================
- lake build no-op   instructions     2.9% (29.2 σ)
- rbmap_1            task-clock       2.6% (21.8 σ)
- rbmap_1            wall-clock       2.6% (21.6 σ)

@tydeu
Copy link
Member Author

tydeu commented Jun 17, 2025

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit d10751d.
There were significant changes against commit 957b904:

  Benchmark          Metric          Change
  ====================================================
+ big_do             wall-clock       -4.3%  (-20.7 σ)
- lake build clean   instructions     20.6%  (206.5 σ)
- lake build clean   maxrss           50.6%   (71.2 σ)
+ lake build clean   task-clock      -16.5% (-610.8 σ)
- lake build clean   wall-clock       88.7%   (32.5 σ)
- lake build no-op   instructions   1225.8%  (546.1 σ)
- lake build no-op   maxrss           13.7%  (176.2 σ)
- lake build no-op   task-clock      645.3%   (90.0 σ)
- lake build no-op   wall-clock      592.9%   (63.7 σ)

@tydeu
Copy link
Member Author

tydeu commented Jun 17, 2025

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 07844dc.
There were significant changes against commit 957b904:

  Benchmark          Metric          Change
  =====================================================
- lake build clean   instructions     20.5% (19126.5 σ)
- lake build clean   maxrss           49.2%    (63.5 σ)
+ lake build clean   task-clock      -16.6%   (-59.4 σ)
- lake build clean   wall-clock       88.1%   (135.7 σ)
- lake build no-op   instructions   1221.5%  (1130.7 σ)
- lake build no-op   maxrss           13.7%    (64.8 σ)
- lake build no-op   task-clock      637.6%    (68.1 σ)
- lake build no-op   wall-clock      593.6%    (58.7 σ)
+ riscv-ast.lean     task-clock       -7.2%   (-23.2 σ)
+ stdlib             grind dsimp     -10.6%  (-110.0 σ)
+ stdlib size        lines C          -1.3%
+ workspaceSymbols   task-clock       -5.3%   (-36.9 σ)
+ workspaceSymbols   wall-clock       -5.3%   (-37.3 σ)

github-merge-queue bot pushed a commit that referenced this pull request Jun 18, 2025
This PR reintroduces the basics of `lean --setup` integration into Lake
without the module computation which is still undergoing performance
debugging in #8787.

Partially reverts #8736 and partially reimplements #8447.
algebraic-dev pushed a commit to algebraic-dev/lean4 that referenced this pull request Jun 18, 2025
This PR reintroduces the basics of `lean --setup` integration into Lake
without the module computation which is still undergoing performance
debugging in leanprover#8787.

Partially reverts leanprover#8736 and partially reimplements leanprover#8447.
wkrozowski pushed a commit to wkrozowski/lean4 that referenced this pull request Jun 24, 2025
This PR reintroduces the basics of `lean --setup` integration into Lake
without the module computation which is still undergoing performance
debugging in leanprover#8787.

Partially reverts leanprover#8736 and partially reimplements leanprover#8447.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants