chore: switch to new test/bench suite by Garmelon · Pull Request #12590 · leanprover/lean4

Garmelon · 2026-02-19T13:49:01Z

This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting.

For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.

Garmelon · 2026-02-19T13:49:18Z

!bench

leanprover-radar · 2026-02-19T13:49:24Z

Benchmark results for 9606b24 against 2ce55ba are in! @Garmelon

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

Bench repo commit hashes for run build differ between commits.
Bench repo commit hashes for run other differ between commits.

🟥 other exited with code -1

No significant changes detected.

Garmelon · 2026-02-19T17:56:27Z

!bench

leanprover-radar · 2026-02-19T17:56:34Z

Benchmark results for bdc35ad against 2ce55ba are in! @Garmelon

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

Bench repo commit hashes for run build differ between commits.
Bench repo commit hashes for run other differ between commits.

🟥 build//instructions: +19.9G (+0.16%)

Small changes (1🟥)

🟥 build/module/Lake.Config.Context//instructions: +6.0M (+1.80%)

Garmelon · 2026-02-19T18:46:00Z

!bench

leanprover-radar · 2026-02-19T18:46:06Z

Benchmark results for 5cf0e47 against 2ce55ba are in! @Garmelon

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

Bench repo commit hashes for run build differ between commits.
Bench repo commit hashes for run other differ between commits.

🟥 build//instructions: +19.1G (+0.15%)

No significant changes detected.

Garmelon · 2026-02-23T18:33:18Z

!bench

leanprover-radar · 2026-02-23T18:33:25Z

Benchmark results for 1fd7517 against ed0fd1e are in! @Garmelon

🟥 build//instructions: +20.3G (+0.16%)

No significant changes detected.

mathlib-lean-pr-testing · 2026-02-23T19:26:23Z

Mathlib CI status (docs):

❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-02-23-rev1 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-23 19:26:22)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 65f112a165d54aa43766d72ad9e91fd07f142b72 --onto ed0fd1e933239beaa7aaa12598f961c260062ab6. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-24 15:46:08)

leanprover-bot · 2026-02-23T19:26:25Z

Reference manual CI status:

❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-02-23-rev1 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-02-23 19:26:24)
❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 65f112a165d54aa43766d72ad9e91fd07f142b72 --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-24 15:46:09)

Garmelon · 2026-02-24T15:12:51Z

!bench

leanprover-radar · 2026-02-24T15:12:56Z

Benchmark results for 8cf223a against 65f112a are in! @Garmelon

🟥 build//instructions: +19.5G (+0.15%)

Large changes (6✅, 5🟥)

✅ compiled/hashmap//instructions: -8.8M (-0.24%)
✅ compiled/iterators//instructions: -8.9M (-1.81%)
✅ compiled/nat_repr//instructions: -8.7M (-0.27%)
✅ compiled/sigmaIterator//instructions: -8.8M (-0.44%)
🟥 elab/big_beq_rec//instructions: +458.4M (+2.47%)
🟥 elab/charactersIn//instructions: +8.1G (+20.15%)
🟥 elab/workspaceSymbols//instructions: +8.1G (+31.47%)
✅ lake/inundation/startup//instructions: -20.7M (-9.49%)
✅ misc/re-elab Init.Data.List.Sublist//instructions: -179.0G (-54.61%)
🟥 misc/re-elab watchdog Init.Data.List.Sublist//instructions: +358.1G (+202.48%)
🟥 size/compile/.out//bytes: +1GiB (+84.01%)

Medium changes (11✅, 2🟥)

✅ compiled/binarytrees.st//instructions: -9.2M (-0.01%)
✅ compiled/deriv//instructions: -8.7M (-0.11%)
✅ compiled/liasolver//instructions: -9.6M (-0.23%)
✅ compiled/qsort//instructions: -8.7M (-0.05%)
✅ compiled/rbmap//instructions: -8.5M (-0.05%)
✅ compiled/rbmap_checkpoint//instructions: -8.6M (-0.06%)
✅ compiled/rbmap_checkpoint2//instructions: -9.7M (-0.06%)
✅ compiled/rbmap_fbip//instructions: -8.3M (-0.11%)
✅ compiled/rbmap_library//instructions: -9.2M (-0.07%)
✅ compiled/treemap//instructions: -9.0M (-0.04%)
✅ compiled/unionfind//instructions: -8.8M (-0.04%)
🟥 elab/riscv-ast//instructions: +701.9M (+0.69%)
🟥 misc/re-elab Init.Data.BitVec.Lemmas//instructions: +84.9G (+11.87%)

Small changes (13✅, 5🟥)

✅ compiled/binarytrees//instructions: -8.6M (-0.01%)
✅ compiled/const_fold//instructions: -26.0M (-0.31%)
✅ compiled/server_startup//instructions: -9.3M (-2.40%)
✅ compiled/workspaceSymbolsNewRanges//instructions: -9.0M (-1.14%)
🟥 elab/big_deceq_rec//instructions: +40.9M (+0.64%)
✅ elab/big_do//instructions: -15.5M (-0.06%)
🟥 elab/big_match//instructions: +28.1M (+0.25%)
✅ elab/big_omega//instructions: -37.0M (-0.16%)
✅ elab/big_omega_MT//instructions: -42.8M (-0.18%)
🟥 elab/grind_ring_5//instructions: +14.8M (+0.17%)
✅ elab/iterators//instructions: -13.5M (-0.46%)
🟥 elab/mut_rec_wf//instructions: +114.8M (+0.41%)
🟥 elab/simp_congr//instructions: +50.6M (+0.47%)
✅ interpreted/iterators//instructions: -24.5M (-0.07%)
✅ lake/inundation/config elab//instructions: -20.7M (-0.79%)
✅ lake/inundation/config import//instructions: -21.6M (-1.77%)
✅ lake/inundation/config tree//instructions: -20.7M (-1.65%)
✅ lake/inundation/env//instructions: -20.9M (-1.69%)

Garmelon · 2026-02-24T16:34:48Z

!bench

leanprover-radar · 2026-02-24T16:34:56Z

Benchmark results for dd59e33 against 65f112a are in! @Garmelon

🟥 build exited with code -1
🟥 other exited with code -1

No significant changes detected.

Garmelon · 2026-02-25T13:02:39Z

!bench

leanprover-radar · 2026-02-25T13:02:50Z

Benchmark results for 5ec17e4 against e96d969 are in! @Garmelon

🟥 build//instructions: +19.6G (+0.16%)

Large changes (5✅, 5🟥)

✅ compiled/iterators//instructions: -9.0M (-1.85%)
✅ compiled/nat_repr//instructions: -9.0M (-0.28%)
✅ compiled/sigmaIterator//instructions: -9.0M (-0.45%)
🟥 elab/big_beq_rec//instructions: +455.8M (+2.45%)
🟥 elab/charactersIn//instructions: +8.1G (+20.16%)
🟥 elab/workspaceSymbols//instructions: +8.1G (+31.44%)
✅ lake/inundation/startup//instructions: -20.7M (-9.47%)
✅ misc/re-elab Init.Data.List.Sublist//instructions: -178.8G (-54.64%)
🟥 misc/re-elab watchdog Init.Data.List.Sublist//instructions: +358.2G (+202.71%)
🟥 size/compile/.out//bytes: +1GiB (+84.02%)

Medium changes (12✅, 1🟥)

✅ compiled/binarytrees.st//instructions: -8.6M (-0.01%)
✅ compiled/deriv//instructions: -8.9M (-0.12%)
✅ compiled/hashmap//instructions: -8.5M (-0.23%)
✅ compiled/liasolver//instructions: -9.6M (-0.23%)
✅ compiled/qsort//instructions: -9.0M (-0.05%)
✅ compiled/rbmap//instructions: -8.9M (-0.06%)
✅ compiled/rbmap_checkpoint//instructions: -8.6M (-0.06%)
✅ compiled/rbmap_checkpoint2//instructions: -8.1M (-0.05%)
✅ compiled/rbmap_fbip//instructions: -8.8M (-0.12%)
✅ compiled/rbmap_library//instructions: -8.9M (-0.06%)
✅ compiled/treemap//instructions: -8.3M (-0.04%)
✅ compiled/unionfind//instructions: -8.7M (-0.03%)
🟥 misc/re-elab Init.Data.BitVec.Lemmas//instructions: +81.4G (+11.39%)

Small changes (13✅, 5🟥)

✅ compiled/binarytrees//instructions: -9.1M (-0.01%)
✅ compiled/const_fold//instructions: -18.2M (-0.22%)
✅ compiled/server_startup//instructions: -8.5M (-2.20%)
✅ compiled/workspaceSymbolsNewRanges//instructions: -9.0M (-1.14%)
🟥 elab/big_deceq_rec//instructions: +39.2M (+0.62%)
✅ elab/big_do//instructions: -19.3M (-0.08%)
✅ elab/big_omega//instructions: -30.5M (-0.13%)
✅ elab/big_omega_MT//instructions: -34.6M (-0.14%)
🟥 elab/grind_ring_5//instructions: +16.3M (+0.18%)
✅ elab/iterators//instructions: -13.8M (-0.47%)
🟥 elab/mut_rec_wf//instructions: +111.4M (+0.40%)
🟥 elab/riscv-ast//instructions: +661.1M (+0.65%)
🟥 elab/simp_congr//instructions: +66.8M (+0.62%)
✅ interpreted/iterators//instructions: -25.1M (-0.07%)
✅ lake/inundation/config elab//instructions: -20.6M (-0.79%)
✅ lake/inundation/config import//instructions: -22.3M (-1.83%)
✅ lake/inundation/config tree//instructions: -21.3M (-1.69%)
✅ lake/inundation/env//instructions: -22.3M (-1.79%)

Based on the cmake features we're currently using, the project won't build correctly on any cmake below 3.20 anyways. 3.21 has some nice small language improvements, and I couldn't find a distro that stocks 3.20 but not 3.21.

Garmelon force-pushed the joscha/bench-suite branch 2 times, most recently from 149769f to bdc35ad Compare February 19, 2026 17:56

Garmelon force-pushed the joscha/bench-suite branch from bdc35ad to 5cf0e47 Compare February 19, 2026 18:45

Garmelon force-pushed the joscha/bench-suite branch 4 times, most recently from 7240ea2 to a940235 Compare February 23, 2026 18:09

Garmelon marked this pull request as ready for review February 23, 2026 18:10

Garmelon requested a review from kim-em as a code owner February 23, 2026 18:25

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Feb 23, 2026

Garmelon force-pushed the joscha/bench-suite branch 2 times, most recently from 214b43a to 8cf223a Compare February 24, 2026 14:19

Garmelon force-pushed the joscha/bench-suite branch from 8cf223a to dd59e33 Compare February 24, 2026 16:34

Garmelon changed the title ~~chore: set up new test/bench suite~~ chore: switch to new test/bench suite Feb 24, 2026

Garmelon force-pushed the joscha/bench-suite branch 2 times, most recently from d07a787 to 5ec17e4 Compare February 25, 2026 13:01

Garmelon enabled auto-merge February 25, 2026 13:29

Garmelon added 19 commits February 25, 2026 14:29

Bump minimum required cmake version to 3.21

e8e812b

Based on the cmake features we're currently using, the project won't build correctly on any cmake below 3.20 anyways. 3.21 has some nice small language improvements, and I couldn't find a distro that stocks 3.20 but not 3.21.

Tweak gitignores

677d073

Set up new test/bench infrastructure

a16918b

Migrate some tests from CMakeLists.txt to tests/misc

00c5a96

Migrate tests/lean

b537793

Migrate tests/lean/run

893f628

Migrate tests/compiler

5921113

Migrate elab benchmarks

31adbf0

Migrate compile benchmarks

9c9e875

Migrate lake inundation benchmarks

7d94ce9

Migrate import/re-elab benchmarks

985947a

Migrate leanchecker benchmark

75f6dc7

Migrate compile binary size benchmark

c1269d8

Migrate bench-radar/size

073da8d

Migrate bench-radar/build

29a1c62

Remove remains of bench-radar

232434d

Lint test suite

e6bc74e

Document new test suite

49d4402

Fix CI

0319418

Garmelon force-pushed the joscha/bench-suite branch from 5ec17e4 to 0319418 Compare February 25, 2026 13:39

Garmelon added this pull request to the merge queue Feb 25, 2026

Merged via the queue into master with commit 08eb78a Feb 25, 2026
16 checks passed

Garmelon deleted the joscha/bench-suite branch February 25, 2026 14:13

fiforeach mentioned this pull request Mar 3, 2026

fix: make option linter.unusedSimpArgs respect linter.all #12560

Merged

Conversation

Garmelon commented Feb 19, 2026

Uh oh!

Garmelon commented Feb 19, 2026

Uh oh!

leanprover-radar commented Feb 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Garmelon commented Feb 19, 2026

Uh oh!

leanprover-radar commented Feb 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Garmelon commented Feb 19, 2026

Uh oh!

leanprover-radar commented Feb 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Garmelon commented Feb 23, 2026

Uh oh!

leanprover-radar commented Feb 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib-lean-pr-testing bot commented Feb 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-bot commented Feb 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Garmelon commented Feb 24, 2026

Uh oh!

leanprover-radar commented Feb 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Garmelon commented Feb 24, 2026

Uh oh!

leanprover-radar commented Feb 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Garmelon commented Feb 25, 2026

Uh oh!

leanprover-radar commented Feb 25, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

leanprover-radar commented Feb 19, 2026 •

edited

Loading

leanprover-radar commented Feb 19, 2026 •

edited

Loading

leanprover-radar commented Feb 19, 2026 •

edited

Loading

leanprover-radar commented Feb 23, 2026 •

edited

Loading

mathlib-lean-pr-testing bot commented Feb 23, 2026 •

edited

Loading

leanprover-bot commented Feb 23, 2026 •

edited

Loading

leanprover-radar commented Feb 24, 2026 •

edited

Loading

leanprover-radar commented Feb 24, 2026 •

edited

Loading

leanprover-radar commented Feb 25, 2026 •

edited

Loading