Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

tc speed test #12810

Closed
wants to merge 11 commits into from
Closed

tc speed test #12810

wants to merge 11 commits into from

Conversation

FR-vdash-bot
Copy link
Collaborator

@FR-vdash-bot FR-vdash-bot commented May 10, 2024


Open in Gitpod

@FR-vdash-bot
Copy link
Collaborator Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit b6f4a43.Found no runs to compare against.

@FR-vdash-bot FR-vdash-bot changed the base branch from bump/nightly-2024-05-09 to master May 10, 2024 23:27
@FR-vdash-bot
Copy link
Collaborator Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit b6f4a43.
There were significant changes against commit 51625e9:

  Benchmark                                           Metric         Change
  =========================================================================
+ build                                               elaboration     -8.9%
+ ~Batteries.Data.Array.Lemmas                        instructions   -87.8%
+ ~Batteries.Data.List.Lemmas                         instructions   -39.5%
+ ~Mathlib.Algebra.DirectLimit                        instructions   -15.2%
+ ~Mathlib.Algebra.Lie.Quotient                       instructions   -72.0%
- ~Mathlib.Algebra.Module.PID                         instructions     7.6%
+ ~Mathlib.Algebra.Module.Submodule.Localization      instructions   -51.3%
+ ~Mathlib.Analysis.Normed.Group.Quotient             instructions   -75.0%
+ ~Mathlib.CategoryTheory.Generator                   instructions   -41.7%
+ ~Mathlib.Combinatorics.Additive.PluenneckeRuzsa     instructions   -69.0%
+ ~Mathlib.FieldTheory.AbelRuffini                    instructions   -35.1%
+ ~Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure   instructions   -43.8%
+ ~Mathlib.GroupTheory.Coset                          instructions   -78.7%
+ ~Mathlib.GroupTheory.GroupAction.Quotient           instructions   -76.5%
+ ~Mathlib.GroupTheory.QuotientGroup                  instructions   -33.5%
+ ~Mathlib.LinearAlgebra.Isomorphisms                 instructions   -57.3%
+ ~Mathlib.LinearAlgebra.Quotient                     instructions   -27.8%
+ ~Mathlib.LinearAlgebra.QuotientPi                   instructions   -67.9%
+ ~Mathlib.LinearAlgebra.SModEq                       instructions   -89.3%
+ ~Mathlib.LinearAlgebra.Semisimple                   instructions   -16.0%
+ ~Mathlib.MeasureTheory.Measure.Haar.Quotient        instructions   -54.5%
+ ~Mathlib.RingTheory.Smooth.Basic                    instructions   -42.0%
+ ~Mathlib.RingTheory.Valuation.ValuationSubring      instructions   -22.3%
+ ~Mathlib.Topology.Algebra.InfiniteSum.Module        instructions   -60.0%
+ ~Mathlib.Topology.Instances.AddCircle               instructions   -58.2%

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 10, 2024
@FR-vdash-bot
Copy link
Collaborator Author

FR-vdash-bot commented May 10, 2024

I'm still worried about other changes having an effect on the results. (upd: indeed...)

@FR-vdash-bot FR-vdash-bot changed the base branch from master to bump/nightly-2024-05-09 May 10, 2024 23:39
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 10, 2024
@FR-vdash-bot
Copy link
Collaborator Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit b6f4a43.
There were significant changes against commit c8ba1f8:

  Benchmark                           Metric         Change
  =========================================================
+ ~Mathlib.LinearAlgebra.Semisimple   instructions   -16.0%

@FR-vdash-bot
Copy link
Collaborator Author

!bench

@FR-vdash-bot
Copy link
Collaborator Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit ba1eb0b.
There were significant changes against commit c8ba1f8:

  Benchmark                           Metric         Change
  =========================================================
+ ~Mathlib.LinearAlgebra.Semisimple   instructions   -16.0%

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 9b3fad2.
There were no significant changes against commit c8ba1f8.

@FR-vdash-bot
Copy link
Collaborator Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 4f80ca8.
There were no significant changes against commit c8ba1f8.

@FR-vdash-bot
Copy link
Collaborator Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 30da8c1.
There were no significant changes against commit c8ba1f8.

@mathlib-bors mathlib-bors bot deleted the branch bump/v4.9.0 May 13, 2024 02:08
@mathlib-bors mathlib-bors bot closed this May 13, 2024
@mathlib-bors mathlib-bors bot changed the base branch from bump/nightly-2024-05-09 to bump/v4.9.0 May 13, 2024 02:08
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.

4 participants