Skip to content

Conversation

@Garmelon
Copy link
Contributor

This PR adds a new radar-based temci-less bench suite that replaces the stdlib benchmarks from the old suite and also measures per-module instruction counts. All other benchmarks from the old suite are unaffected.

The readme at tests/bench-radar/README.md explains in more detail how the bench suite is structured and how it works. The readmes in the benchmark subdirectories explain what each benchmark does and which metrics it collects.

All metrics except stdlib//max dynamic symbols were ported to the new suite, though most have been renamed.

@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 Nov 19, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Nov 19, 2025

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5cc0a103468a8da333f1f07781e5b83799582f6f --onto 5a4226f2bdcc6299df76285b1d30f238546c09fe. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-19 18:46:30)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6da35eeccb726b67d9b32ab7bbd67ac00ed93589 --onto f2e191d0afbb5adcc6f12e1779c8b141fc9af996. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-24 15:48:36)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Nov 19, 2025

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 5cc0a103468a8da333f1f07781e5b83799582f6f --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-19 18:46:32)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 6da35eeccb726b67d9b32ab7bbd67ac00ed93589 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-24 15:48:37)

@Garmelon Garmelon marked this pull request as draft November 20, 2025 17:19
@Garmelon
Copy link
Contributor Author

I'm going to rename the stdlib benchmark to build first, then this PR should be ready.

@Garmelon Garmelon force-pushed the new-stdlib-bench-suite branch 2 times, most recently from d6d73e6 to 2c51e9e Compare November 24, 2025 17:25
@Garmelon Garmelon marked this pull request as ready for review November 24, 2025 17:33
@Garmelon
Copy link
Contributor Author

!radar

@leanprover-radar
Copy link

leanprover-radar commented Nov 24, 2025

Benchmark results for 2c51e9e against 6da35ee are in! @Garmelon

Runs (1)
  • other exited with code 1 (🟥)

@Garmelon Garmelon force-pushed the new-stdlib-bench-suite branch from 2c51e9e to 162edd5 Compare November 24, 2025 18:38
@Garmelon
Copy link
Contributor Author

!radar

@leanprover-radar
Copy link

leanprover-radar commented Nov 24, 2025

Benchmark results for 162edd5 against 6da35ee are in! @Garmelon

@Garmelon Garmelon requested a review from Kha November 24, 2025 19:20
@Garmelon Garmelon force-pushed the new-stdlib-bench-suite branch from 70da471 to f775d07 Compare November 25, 2025 12:45
@Garmelon Garmelon enabled auto-merge November 25, 2025 12:46
@Garmelon Garmelon added this pull request to the merge queue Nov 25, 2025
Merged via the queue into master with commit debafca Nov 25, 2025
14 checks passed
@Garmelon Garmelon deleted the new-stdlib-bench-suite branch November 28, 2025 12:54
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

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.

6 participants