Skip to content

bench leanprover/lean4#2714#7933

Closed
collares wants to merge 678 commits intomasterfrom
lean-pr-testing-2714
Closed

bench leanprover/lean4#2714#7933
collares wants to merge 678 commits intomasterfrom
lean-pr-testing-2714

Conversation

@collares
Copy link
Copy Markdown
Contributor


Open in Gitpod

@collares
Copy link
Copy Markdown
Contributor Author

!bench

@collares
Copy link
Copy Markdown
Contributor Author

collares commented Oct 25, 2023

Maybe this should be compared against 7bb49c27fecb8f554983c6d54afd79f6416c36d2 but I'm not sure it matters much.

@leanprover-bot
Copy link
Copy Markdown
Collaborator

Here are the benchmark results for commit 282b3ac.
There were significant changes against commit 8c5a066:

  Benchmark                                                  Metric         Change
  ================================================================================
- ~Mathlib.Analysis.NormedSpace.Multilinear                  instructions     2.7%
- ~Mathlib.CategoryTheory.Monoidal.Mon_                      instructions     2.9%
- ~Mathlib.FieldTheory.RatFunc                               instructions     2.2%
+ ~Mathlib.LinearAlgebra.FreeModule.PID                      instructions   -10.7%
- ~Mathlib.RepresentationTheory.Action                       instructions     3.4%
- ~Mathlib.RepresentationTheory.GroupCohomology.Resolution   instructions     3.1%

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.

8 participants