Skip to content

chore: update bench suite - #728

Merged
MackieLoeffel merged 5 commits into
leanprover-community:masterfrom
Garmelon:update-bench-suite
Oct 27, 2026
Merged

MackieLoeffel merged 5 commits into
leanprover-community:masterfrom
Garmelon:update-bench-suite

Conversation

@Garmelon

Copy link
Copy Markdown
Contributor

This PR brings the benchmark suite back into alignment with the other ones. It fixes how wall-clock and how maxrss are measured, and adds support for precompilation (which will be used by #722).

@Garmelon

Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar

leanprover-radar commented Oct 26, 2026 •

Copy link
Copy Markdown

Benchmark results for 4fb28a9 against 3f808f5 are in. There are significant results. @Garmelon

  • ✅ build//instructions: -149.3G (-5.87%)

Large changes (1✅)

  • 1 hidden

Small changes (241✅)

  • ✅ build/module/Iris.Algebra.Agree//instructions: -394.5M (-3.31%)
  • ✅ build/module/Iris.Algebra.Auth//instructions: -363.7M (-2.43%)
  • ✅ build/module/Iris.Algebra.BigOp//instructions: -392.4M (-2.21%)
  • ✅ build/module/Iris.Algebra.CMRA//instructions: -605.1M (-0.89%)
  • ✅ build/module/Iris.Algebra.CMRABigOp//instructions: -310.5M (-15.87%)
  • ✅ build/module/Iris.Algebra.COFESolver//instructions: -346.1M (-2.65%)
  • ✅ build/module/Iris.Algebra.Chain//instructions: -315.4M (-9.09%)
  • ✅ build/module/Iris.Algebra.Csum//instructions: -376.6M (-1.14%)
  • ✅ build/module/Iris.Algebra.DFrac//instructions: -353.8M (-1.95%)
  • ✅ build/module/Iris.Algebra.DynReservationMap//instructions: -372.6M (-2.58%)
  • ✅ build/module/Iris.Algebra.Excl//instructions: -334.7M (-6.18%) (reduced significance based on absolute threshold)
  • ✅ build/module/Iris.Algebra.Frac//instructions: -336.7M (-4.50%)
  • ✅ build/module/Iris.Algebra.Functions//instructions: -316.4M (-7.81%) (reduced significance based on absolute threshold)
  • ✅ build/module/Iris.Algebra.GenMap//instructions: -340.5M (-2.58%)
  • ✅ build/module/Iris.Algebra.Heap//instructions: -409.3M (-1.19%)
  • ✅ build/module/Iris.Algebra.HeapView//instructions: -362.2M (-1.57%)
  • ✅ build/module/Iris.Algebra.IProp//instructions: -313.2M (-9.25%)
  • ✅ build/module/Iris.Algebra.IsOp//instructions: -316.9M (-17.98%) (reduced significance based on absolute threshold)
  • ✅ build/module/Iris.Algebra.LeibnizMultiSet//instructions: -323.5M (-9.96%) (reduced significance based on absolute threshold)
  • ✅ build/module/Iris.Algebra.LeibnizSet//instructions: -369.5M (-4.12%)
  • and 221 more

@MackieLoeffel

Copy link
Copy Markdown
Collaborator

Thanks for the PR! One brief question: The description says "adds support for precompilation", but I don't see anything related to that in this PR. Do I miss something or is something missing from this PR? (Or is this referring to the changes in #722?)

@Garmelon

Garmelon commented Oct 27, 2026 •

Copy link
Copy Markdown
Contributor Author

I meant that after this PR, the bench suite no longer crashes when you try to use pre compilation. #722 had to include the same changes in order not to crash the bench suite.

@Garmelon

Copy link
Copy Markdown
Contributor Author

Now that I'm looking more closely, looks like I missed exactly those changes in this PR. One moment

@Garmelon

Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar

leanprover-radar commented Oct 27, 2026 •

Copy link
Copy Markdown

Benchmark results for 984c5ba against 3f808f5 are in. There are significant results. @Garmelon

  • ✅ build//instructions: -149.3G (-5.87%)

Large changes (1✅)

  • 1 hidden

Small changes (242✅)

  • ✅ build/module/Iris.Algebra.Agree//instructions: -391.9M (-3.29%)
  • ✅ build/module/Iris.Algebra.Auth//instructions: -364.4M (-2.43%)
  • ✅ build/module/Iris.Algebra.BigOp//instructions: -395.1M (-2.22%)
  • ✅ build/module/Iris.Algebra.CMRA//instructions: -622.7M (-0.92%)
  • ✅ build/module/Iris.Algebra.CMRABigOp//instructions: -310.6M (-15.88%)
  • ✅ build/module/Iris.Algebra.COFESolver//instructions: -343.6M (-2.63%)
  • ✅ build/module/Iris.Algebra.Chain//instructions: -315.5M (-9.10%)
  • ✅ build/module/Iris.Algebra.Csum//instructions: -378.1M (-1.15%)
  • ✅ build/module/Iris.Algebra.DFrac//instructions: -351.8M (-1.94%)
  • ✅ build/module/Iris.Algebra.DynReservationMap//instructions: -370.9M (-2.57%)
  • ✅ build/module/Iris.Algebra.Excl//instructions: -333.6M (-6.16%) (reduced significance based on absolute threshold)
  • ✅ build/module/Iris.Algebra.Frac//instructions: -333.8M (-4.46%)
  • ✅ build/module/Iris.Algebra.Functions//instructions: -316.6M (-7.82%) (reduced significance based on absolute threshold)
  • ✅ build/module/Iris.Algebra.GenMap//instructions: -338.2M (-2.56%)
  • ✅ build/module/Iris.Algebra.Heap//instructions: -405.3M (-1.18%)
  • ✅ build/module/Iris.Algebra.HeapView//instructions: -358.7M (-1.55%)
  • ✅ build/module/Iris.Algebra.IProp//instructions: -311.5M (-9.20%)
  • ✅ build/module/Iris.Algebra.IsOp//instructions: -316.9M (-17.98%) (reduced significance based on absolute threshold)
  • ✅ build/module/Iris.Algebra.LeibnizMultiSet//instructions: -323.5M (-9.96%) (reduced significance based on absolute threshold)
  • ✅ build/module/Iris.Algebra.LeibnizSet//instructions: -369.9M (-4.13%)
  • and 222 more

@MackieLoeffel

Copy link
Copy Markdown
Collaborator

Perfect, thanks! Merging.

@MackieLoeffel
MackieLoeffel merged commit f4429f2 into leanprover-community:master Oct 27, 2026
5 checks passed
@Garmelon
Garmelon deleted the update-bench-suite branch October 27, 2026 10:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants