Skip to content

chore: speed up test suite slightly#12969

Merged
Garmelon merged 12 commits intomasterfrom
joscha/slow-tests
Mar 20, 2026
Merged

chore: speed up test suite slightly#12969
Garmelon merged 12 commits intomasterfrom
joscha/slow-tests

Conversation

@Garmelon
Copy link
Copy Markdown
Contributor

@Garmelon Garmelon commented Mar 18, 2026

This PR speeds up some benchmarks when run as tests by lowering their workload. It also stops testing some of the more expensive benchmarks that can't be easily made smaller.

@Garmelon
Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 18, 2026

Benchmark results for cefdd2b against 09da0d2 are in. There are no significant changes. @Garmelon

  • build//instructions: -135.3M (-0.00%)

No significant changes detected.

@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 Mar 18, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing Bot commented Mar 18, 2026

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 09da0d22a1861d5d10e4a446458e3a44526e0717 --onto 61a3443a9569d548a235f785b9a33984bb7ff622. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-18 14:08:59)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0f730662de0bbaa6ed07484d8f0e411de2bcd1ea --onto 61a3443a9569d548a235f785b9a33984bb7ff622. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-19 18:03:13)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c6a89cc71647554b34018e1ae579b20fa965f9b1 --onto 87180a09c49c91577e54284703c73c5ca76be126. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-20 12:59:49)

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Mar 18, 2026

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 09da0d22a1861d5d10e4a446458e3a44526e0717 --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-18 14:09:00)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 0f730662de0bbaa6ed07484d8f0e411de2bcd1ea --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-19 18:03:15)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase c6a89cc71647554b34018e1ae579b20fa965f9b1 --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-20 12:59:51)

@Garmelon Garmelon force-pushed the joscha/slow-tests branch from 3fba80f to 6dcf599 Compare March 18, 2026 14:30
@Garmelon Garmelon changed the title chore: make some slow tests faster chore: speed up test suite Mar 18, 2026
@Garmelon
Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 18, 2026

Benchmark results for 6dcf599 against 09da0d2 are in. Significant changes detected! @Garmelon

  • 🟥 build//instructions: +310.4M (+0.00%)
  • 🟥 other exited with code 2

No significant changes detected.

@Garmelon Garmelon changed the title chore: speed up test suite chore: speed up test suite slightly Mar 18, 2026
@leanprover leanprover deleted a comment from leanprover-radar Mar 18, 2026
@Garmelon
Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 18, 2026

Benchmark results for ed803dd against 09da0d2 are in. There are no significant changes. @Garmelon

  • build//instructions: -878.7M (-0.01%)

No significant changes detected.

@Garmelon Garmelon force-pushed the joscha/slow-tests branch from 333f5f8 to c17df0c Compare March 19, 2026 17:11
@Garmelon
Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 19, 2026

Benchmark results for 3bb1903 against 0f73066 are in. Significant changes detected! @Garmelon

  • build//instructions: -325.1M (-0.00%)
  • 🟥 other exited with code 2

Small changes (1🟥)

  • 🟥 build/module/Init.Data.Nat.ToString//instructions: +32.9M (+0.10%)

@Garmelon Garmelon force-pushed the joscha/slow-tests branch from 3bb1903 to de10a6a Compare March 20, 2026 12:06
@Garmelon
Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 20, 2026

Benchmark results for de10a6a against c6a89cc are in. There are no significant changes. @Garmelon

  • build//instructions: -59.8M (-0.00%)

Small changes (1🟥)

  • 🟥 elab/charactersIn//instructions: +61.5M (+0.13%)

@Garmelon
Copy link
Copy Markdown
Contributor Author

From my (unreliable, because I didn't reduce parallelism) measurements, this reduces the total time for *_bench tests from 680s to 410s.

@Garmelon Garmelon added this pull request to the merge queue Mar 20, 2026
Merged via the queue into master with commit 492fda3 Mar 20, 2026
15 checks passed
@Garmelon Garmelon deleted the joscha/slow-tests branch March 20, 2026 13:05
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.

3 participants