test

[hargoniX]

Read this section before submitting

• Ensure your PR follows the External Contribution Guidelines.
• Please make sure the PR has excellent documentation and tests. If we label it missing documentation or missing tests then it needs fixing!
• Include the link to your RFC or bug issue in the description.
• If the issue does not already have approval from a developer, submit the PR as draft.
• The PR title/description will become the commit message. Keep it up-to-date as the PR evolves.
• For feat/fix PRs, the first paragraph starting with "This PR" must be present and will become a
  changelog entry unless the PR is labeled with no-changelog. If the PR does not have this label,
  it must instead be categorized with one of the changelog-* labels (which will be done by a
  reviewer for external PRs).
• A toolchain of the form leanprover/lean4-pr-releases:pr-release-NNNN for Linux and M-series Macs will be generated upon build. To generate binaries for Windows and Intel-based Macs as well, write a comment containing release-ci on its own line.
• If you rebase your PR onto nightly-with-mathlib then CI will test Mathlib against your PR.
• You can manage the awaiting-review, awaiting-author, and WIP labels yourself, by writing a comment containing one of these labels on its own line.
• Remove this section, up to and including the --- before submitting.

---

This PR <short changelog summary for feat/fix, see above>.

Closes <RFC or bug issue number fixed by this PR, if any>

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 15f380e against f9b2f6b are in. Significant changes detected! @hargoniX

• ✅ build//instructions: -200.2G (-1.66%)

Large changes (20✅)

• ✅ build/module/Std.Data.DHashMap.Internal.RawLemmas//instructions: -8.1G (-3.10%)
• ✅ compiled/binarytrees.st//instructions: -1.8G (-2.80%)
• ✅ compiled/binarytrees//instructions: -1.8G (-2.79%)
• ✅ compiled/deriv//instructions: -182.6M (-2.40%)
• ✅ compiled/hashmap//instructions: -145.8M (-3.88%)
• ✅ compiled/ilean_roundtrip//instructions: -265.3M (-1.04%)
• ✅ compiled/liasolver//instructions: -42.5M (-0.98%)
• ✅ compiled/parser//instructions: -431.0M (-1.15%)
• ✅ compiled/phashmap//instructions: -198.9M (-2.09%)
• ✅ compiled/qsort//instructions: -192.2M (-1.04%)
• ✅ compiled/rbmap//instructions: -376.4M (-3.97%)
• ✅ compiled/rbmap_checkpoint//instructions: -391.7M (-2.69%)
• ✅ compiled/rbmap_checkpoint2//instructions: -379.1M (-3.78%)
• ✅ compiled/rbmap_fbip//instructions: -255.0M (-3.27%)
• ✅ compiled/rbmap_library//instructions: -253.6M (-2.49%)
• ✅ compiled/treemap//instructions: -220.3M (-1.22%)
• ✅ compiled/unionfind//instructions: -985.9M (-3.35%)
• ✅ elab/big_do//instructions: -386.3M (-1.63%)
• ✅ elab/grind_bitvec2//instructions: -2.8G (-1.45%)
• ✅ misc/import Std.Data.DHashMap.Internal.RawLemmas//instructions: -8.2G (-3.20%)

Medium changes (52✅)

Too many entries to display here. View the full report on radar instead.

Small changes (1791✅)

Too many entries to display here. View the full report on radar instead.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f9b2f6b597ecd8ff257f08021d9972823bd31f93 --onto e0a29f43d2e4685febd0ed6bcfad511f7a235b6f. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-10 16:25:07)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase cd697eac812e1233bed8d452cc3ad16510d44718 --onto d76e5a1886956bb38dc6bd2868260550dc66c309. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-13 14:38:45)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase f9b2f6b597ecd8ff257f08021d9972823bd31f93 --onto 861bc19e0c1c45b5766cc5c9ef0488568368b236. You can force reference manual CI using the force-manual-ci label. (2026-04-10 16:25:09)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase cd697eac812e1233bed8d452cc3ad16510d44718 --onto 861bc19e0c1c45b5766cc5c9ef0488568368b236. You can force reference manual CI using the force-manual-ci label. (2026-04-13 14:38:47)

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for d77feff against cd697ea are in. Significant changes detected! @hargoniX

• 🟥 build//instructions: +1.4T (+11.99%)

Large changes (1✅, 138🟥)

Too many entries to display here. View the full report on radar instead.

Medium changes (314🟥)

Too many entries to display here. View the full report on radar instead.

Small changes (2119🟥)

Too many entries to display here. View the full report on radar instead.

[Garmelon]

!bench

[leanprover-radar]

Benchmark results for d77feff against cd697ea are in. (These commits have already been benchmarked in a previous command.) There are significant results. @Garmelon

• 🟥 build//instructions: +1.4T (+11.99%)

Large changes (1✅, 138🟥)

Too many entries to display here. View the full report on radar instead.

Medium changes (315🟥)

Too many entries to display here. View the full report on radar instead.

Small changes (2117🟥)

Too many entries to display here. View the full report on radar instead.