Skip to content

perf: bump priority of zsmul#13746

Open
hargoniX wants to merge 1 commit into
masterfrom
bump_zsmul
Open

perf: bump priority of zsmul#13746
hargoniX wants to merge 1 commit into
masterfrom
bump_zsmul

Conversation

@hargoniX
Copy link
Copy Markdown
Contributor

@hargoniX hargoniX commented May 15, 2026

No description provided.

@hargoniX hargoniX added the fast-ci Forces the use of large runners so that e.g. PR releases are created faster label May 15, 2026
@hargoniX
Copy link
Copy Markdown
Contributor Author

hargoniX commented May 15, 2026

!bench mathlib

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented May 15, 2026 •
edited
Loading

Benchmark results for leanprover-community/mathlib4-nightly-testing@01b2397 against leanprover-community/mathlib4-nightly-testing@b1620a8 are in. There are significant results. @hargoniX

  • 🟥 build//instructions: +176.6G (+0.10%)

Large changes (1✅)

  • ✅ build/module/Mathlib.CategoryTheory.Triangulated.TriangleShift//instructions: -34.5G (-18.68%)

Medium changes (1✅, 1🟥)

  • ✅ build/module/Mathlib.Analysis.Calculus.Taylor//instructions: -2.0G (-2.59%)
  • 🟥 build/module/Mathlib.LinearAlgebra.Alternating.Uncurry.Fin//instructions: +2.9G (+16.45%)

Small changes (7✅, 7🟥)

  • 🟥 build/module/Mathlib.Algebra.FreeAbelianGroup.Finsupp//instructions: +358.5M (+4.39%)
  • 🟥 build/module/Mathlib.Algebra.Lie.Basis//instructions: +2.9G (+2.36%)
  • 🟥 build/module/Mathlib.Algebra.Module.ZLattice.Summable//instructions: +2.7G (+4.71%)
  • 🟥 build/module/Mathlib.Analysis.Fourier.AddCircle//instructions: +1.9G (+4.13%)
  • ✅ build/module/Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation//instructions: -2.5G (-1.60%)
  • 🟥 build/module/Mathlib.Geometry.Euclidean.Angle.Oriented.Basic//instructions: +1.8G (+2.28%)
  • 🟥 build/module/Mathlib.GroupTheory.DivisibleHull//instructions: +1.6G (+3.85%)
  • ✅ build/module/Mathlib.LinearAlgebra.TensorProduct.Graded.External//instructions: -2.3G (-3.49%)
  • ✅ build/module/Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun//instructions: -568.1M (-1.02%)
  • ✅ build/module/Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable//instructions: -661.8M (-2.18%)
  • ✅ build/module/Mathlib.MeasureTheory.Measure.Prokhorov//instructions: -1.0G (-2.26%)
  • ✅ build/module/Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula//instructions: -927.5M (-1.78%)
  • ✅ build/module/Mathlib.RingTheory.Congruence.Opposite//instructions: -196.2M (-4.03%)
  • 🟥 build/module/Mathlib.Tactic//instructions: +200.9M (+2.74%)

@hargoniX hargoniX changed the title experiment: bump priority of zsmul perf: bump priority of zsmul May 15, 2026
@hargoniX hargoniX marked this pull request as ready for review May 15, 2026 23:23
@github-actions github-actions Bot added toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN labels May 15, 2026
@leanprover-bot leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label May 15, 2026
@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented May 15, 2026 •
edited
Loading

Reference manual CI status:

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request May 15, 2026
Update lean-toolchain for leanprover/lean4#13746
91a3175
mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request May 16, 2026
Update lean-toolchain for leanprover/lean4#13746
77bf889
@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added the builds-mathlib CI has verified that Mathlib builds against this PR label May 16, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing Bot commented May 16, 2026

Mathlib CI status (docs):

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

builds-manual CI has verified that the Lean Language Reference builds against this PR builds-mathlib CI has verified that Mathlib builds against this PR fast-ci Forces the use of large runners so that e.g. PR releases are created faster mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@hargoniX @leanprover-radar @leanprover-bot