Skip to content

test: lake: benchmark precompileLibrary - #15227

Merged
tydeu merged 1 commit into
leanprover:masterfrom
tydeu:lake/bench-precompileLibrary
Sep 20, 2026
Merged

tydeu merged 1 commit into
leanprover:masterfrom
tydeu:lake/bench-precompileLibrary

Conversation

@tydeu

@tydeu tydeu commented Sep 19, 2026

Copy link
Copy Markdown
Member

This PR adds a precompilleLibrary no-op and clean build benchmark and renames the previous build/precompile benchmark to precompileModules.

@tydeu tydeu added the changelog-no Do not include this PR in the release changelog label Sep 19, 2026
@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 Sep 19, 2026
@tydeu

tydeu commented Sep 19, 2026

Copy link
Copy Markdown
Member Author

!bench

@leanprover-radar

leanprover-radar commented Sep 19, 2026

Copy link
Copy Markdown

Benchmark results for dc4e78c against b318ba5 are in. No significant results found. @tydeu

  • 🟥 build//instructions: +96.5M (+0.00%)

Small changes (1✅, 1🟥)

  • compiled/treemap//instructions: -21.5k (-0.00%)
  • 🟥 lake/inundation/config/elab//instructions: +11.0M (+0.43%)

@tydeu
tydeu marked this pull request as ready for review September 20, 2026 01:32
@tydeu
tydeu added this pull request to the merge queue Sep 20, 2026
Merged via the queue into leanprover:master with commit 4199bb3 Sep 20, 2026
28 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-no Do not include this PR in the release changelog 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.

2 participants