chore: golf using custom elaborators by grunweg · Pull Request #30357 · leanprover-community/mathlib4

grunweg · 2025-10-09T04:58:37Z

Test the elaborators on a large scale by trying them out. They mostly work very well.
Benchmarking results so far are very positive!

Unexpected errors:

the defeq check on the set fails in Riemannian/Basic.lean; TODO minimise and investigate
Atlas.lean: coercion on I itself does not fire?
SpecificFunctions.lean: more normed-space-like thingies, perhaps wontfix?

XXX: revert ContMDiffOn.smul_section_of_tsupport rename!
TODO: check if there are further opportunities to golf, with newly added lemmas
re-bench!

depends on: [Merged by Bors] - feat: support products and disjoint unions in the differential geometry elaborators #30463

github-actions · 2025-10-09T04:59:45Z

PR summary 4166dc3b98

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Geometry.Manifold.Complex	2553	2556	+3 (+0.12%)
Mathlib.Geometry.Manifold.ContMDiffMap	2211	2213	+2 (+0.09%)
Mathlib.Geometry.Manifold.VectorBundle.Tangent	2219	2221	+2 (+0.09%)
Mathlib.Geometry.Manifold.BumpFunction	2528	2530	+2 (+0.08%)
Mathlib.Geometry.Manifold.MFDeriv.FDeriv	2210	2211	+1 (+0.05%)
Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions	2212	2213	+1 (+0.05%)
Mathlib.Geometry.Manifold.Algebra.Monoid	2215	2216	+1 (+0.05%)
Mathlib.Geometry.Manifold.Algebra.LieGroup	2216	2217	+1 (+0.05%)
Mathlib.Geometry.Manifold.Algebra.Structures	2217	2218	+1 (+0.05%)
Mathlib.Geometry.Manifold.Algebra.SmoothFunctions	2218	2219	+1 (+0.05%)
Mathlib.Geometry.Manifold.VectorBundle.SmoothSection	2225	2226	+1 (+0.04%)
Mathlib.Geometry.Manifold.MFDeriv.Atlas	2226	2227	+1 (+0.04%)
Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable	2226	2227	+1 (+0.04%)
Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential	2227	2228	+1 (+0.04%)
Mathlib.Geometry.Manifold.VectorBundle.Hom	2228	2229	+1 (+0.04%)
Mathlib.Geometry.Manifold.Diffeomorph	2229	2230	+1 (+0.04%)
Mathlib.Geometry.Manifold.MFDeriv.Tangent	2230	2231	+1 (+0.04%)
Mathlib.Geometry.Manifold.IntegralCurve.Basic	2231	2232	+1 (+0.04%)
Mathlib.Geometry.Manifold.LocalDiffeomorph	2232	2233	+1 (+0.04%)
Mathlib.Geometry.Manifold.ContMDiffMFDeriv	2235	2236	+1 (+0.04%)
Mathlib.Geometry.Manifold.VectorBundle.Riemannian	2243	2244	+1 (+0.04%)
Mathlib.Geometry.Manifold.VectorField.Pullback	2253	2254	+1 (+0.04%)
Mathlib.Geometry.Manifold.VectorField.LieBracket	2254	2255	+1 (+0.04%)
Mathlib.Geometry.Manifold.GroupLieAlgebra	2258	2259	+1 (+0.04%)
Mathlib.Geometry.Manifold.Instances.Icc	2290	2291	+1 (+0.04%)
Mathlib.Geometry.Manifold.Instances.Sphere	2328	2329	+1 (+0.04%)
Mathlib.Geometry.Manifold.Sheaf.Smooth	2507	2508	+1 (+0.04%)
Mathlib.Geometry.Manifold.Riemannian.PathELength	2539	2540	+1 (+0.04%)
Mathlib.Geometry.Manifold.PartitionOfUnity	2550	2551	+1 (+0.04%)
Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff	2559	2560	+1 (+0.04%)
Mathlib.Geometry.Manifold.WhitneyEmbedding	2559	2560	+1 (+0.04%)
Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique	2563	2564	+1 (+0.04%)
Mathlib.Geometry.Manifold.IntegralCurve.UniformTime	2564	2565	+1 (+0.04%)
Mathlib.Analysis.Complex.UpperHalfPlane.Manifold	2565	2566	+1 (+0.04%)
Mathlib.Geometry.Manifold.Riemannian.Basic	2569	2570	+1 (+0.04%)
Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable	2588	2589	+1 (+0.04%)
Mathlib.NumberTheory.ModularForms.Basic	2597	2598	+1 (+0.04%)

Import changes for all files

Files	Import difference
48 files `Mathlib.Analysis.Calculus.Rademacher` `Mathlib.Analysis.Complex.UpperHalfPlane.Manifold` `Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff` `Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation` `Mathlib.Geometry.Manifold.Algebra.LieGroup` `Mathlib.Geometry.Manifold.Algebra.Monoid` `Mathlib.Geometry.Manifold.Algebra.SmoothFunctions` `Mathlib.Geometry.Manifold.Algebra.Structures` `Mathlib.Geometry.Manifold.ContMDiffMFDeriv` `Mathlib.Geometry.Manifold.DerivationBundle` `Mathlib.Geometry.Manifold.Diffeomorph` `Mathlib.Geometry.Manifold.GroupLieAlgebra` `Mathlib.Geometry.Manifold.Instances.Icc` `Mathlib.Geometry.Manifold.Instances.Sphere` `Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra` `Mathlib.Geometry.Manifold.IntegralCurve.Basic` `Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique` `Mathlib.Geometry.Manifold.IntegralCurve.Transform` `Mathlib.Geometry.Manifold.IntegralCurve.UniformTime` `Mathlib.Geometry.Manifold.LocalDiffeomorph` `Mathlib.Geometry.Manifold.MFDeriv.Atlas` `Mathlib.Geometry.Manifold.MFDeriv.FDeriv` `Mathlib.Geometry.Manifold.MFDeriv.NormedSpace` `Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions` `Mathlib.Geometry.Manifold.MFDeriv.Tangent` `Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential` `Mathlib.Geometry.Manifold.PartitionOfUnity` `Mathlib.Geometry.Manifold.PoincareConjecture` `Mathlib.Geometry.Manifold.Riemannian.Basic` `Mathlib.Geometry.Manifold.Riemannian.PathELength` `Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace` `Mathlib.Geometry.Manifold.Sheaf.Smooth` `Mathlib.Geometry.Manifold.VectorBundle.Hom` `Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable` `Mathlib.Geometry.Manifold.VectorBundle.Riemannian` `Mathlib.Geometry.Manifold.VectorBundle.SmoothSection` `Mathlib.Geometry.Manifold.VectorField.LieBracket` `Mathlib.Geometry.Manifold.VectorField.Pullback` `Mathlib.Geometry.Manifold.WhitneyEmbedding` `Mathlib.NumberTheory.ModularForms.Basic` `Mathlib.NumberTheory.ModularForms.Bounds` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable` `Mathlib.NumberTheory.ModularForms.LevelOne` `Mathlib.NumberTheory.ModularForms.NormTrace` `Mathlib.NumberTheory.ModularForms.Petersson` `Mathlib.NumberTheory.ModularForms.QExpansion` `Mathlib.Topology.Compactification.OnePoint.Sphere`	1
4 files `Mathlib.Geometry.Manifold.BumpFunction` `Mathlib.Geometry.Manifold.ContMDiffMap` `Mathlib.Geometry.Manifold.VectorBundle.Pullback` `Mathlib.Geometry.Manifold.VectorBundle.Tangent`	2
`Mathlib.Geometry.Manifold.Complex`	3

Declarations diff

++-- hasMFDerivWithinAt
++--+- mdifferentiableWithinAt
+-+- coeFn_mk
+-+- contMDiffAt
+-+- contMDiff_smul
+-+- mdifferentiable'
+-+-++--+- mdifferentiableOn
+-+-++--+-+- mdifferentiableAt
+-+-+-+++--- mdifferentiable
+-+-+-+- contMDiff
--++ hasMFDerivAt
--++ mfderiv_eq

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for scripts/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

grunweg · 2025-10-10T04:47:03Z

!bench

leanprover-bot · 2025-10-10T05:21:43Z

Here are the benchmark results for commit 816828b.
There were no significant changes against commit c7bb793.

github-actions · 2025-10-10T05:22:14Z

File	Instructions	%
`build`	-13.862⬝10⁹	(+0.00%)
`Mathlib.Geometry.Manifold.Notation`	+2.492⬝10⁹	(+11.26%)
`Mathlib.Topology.Sheaves.Stalks`	+1.16⬝10⁹	(+1.36%)

2 files, Instructions -2.0⬝10⁹

File	Instructions	%
`Mathlib.Geometry.Manifold.VectorField.Pullback`	-1.98⬝10⁹	(-1.67%)
`Mathlib.Geometry.Manifold.VectorField.LieBracket`	-1.693⬝10⁹	(-1.99%)

File	Instructions	%
`Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable`	-6.363⬝10⁹	(-9.15%)
CI run Lakeprof report

mathlib4-merge-conflict-bot · 2025-10-14T18:10:28Z

This pull request has conflicts, please merge master and resolve them.

grunweg · 2025-10-27T19:53:54Z

!bench

grunweg · 2025-10-27T19:54:06Z

Let's benchmark again, now that the list of features is much more complete.

leanprover-bot · 2025-10-27T20:42:04Z

Here are the benchmark results for commit d4a0bdb.
The entire run failed.
Found no significant differences.

mathlib4-merge-conflict-bot · 2025-10-28T11:12:20Z

This pull request has conflicts, please merge master and resolve them.

Whenever the `T%` elaborator succeeds, head beta reduce the resulting application. This enables applying it with anonymous functions or inside big operators without issue. (For instance, all changes to `SmoothSection` in #30357 are now possible without additional `dsimp` steps.) In the process, also extract the workhorse component of the elaborator into an independent function and improve its doc-string to mention the corresponding tracing option. Co-authored-by: thorimur <thomasmurrills@gmail.com> Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>

grunweg · 2026-02-27T14:33:05Z

!bench

leanprover-radar · 2026-02-27T14:33:22Z

Benchmark results for 289de6f against 4166dc3 are in! @grunweg

🟥 build//instructions: +8.5G (+0.00%)

Small changes (2✅)

✅ build/module/Mathlib.Geometry.Manifold.ContMDiffMFDeriv//instructions: -1.1G (-2.11%)
✅ build/module/Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable//instructions: -3.1G (-5.10%)

mathlib-merge-conflicts · 2026-03-02T21:49:46Z

This pull request has conflicts, please merge master and resolve them.

The final pieces from leanprover-community#30357.

The final pieces from #30357.

grunweg · 2026-03-07T12:26:50Z

This PR has been merged in pieces now, closing.

The final pieces from leanprover-community#30357.

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 9, 2025

grunweg added t-differential-geometry Manifolds etc awaiting-bench This PR needs to be benchmarked before merging labels Oct 10, 2025

grunweg force-pushed the diffgeo-use-custom-elaborators branch from 7cecfcf to e80c292 Compare October 10, 2025 03:54

grunweg mentioned this pull request Oct 10, 2025

[Merged by Bors] - feat: miscellaneous improvements to the differential geometry elaborators #28032

Closed

1 task

grunweg force-pushed the diffgeo-use-custom-elaborators branch 4 times, most recently from ac20338 to 60035cc Compare October 13, 2025 08:29

grunweg mentioned this pull request Oct 13, 2025

Tracking issue for differential geometry elaborators #30503

Open

26 tasks

mathlib4-merge-conflict-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 Oct 14, 2025

grunweg force-pushed the diffgeo-use-custom-elaborators branch from 60035cc to 7e6eb01 Compare October 25, 2025 11:42

github-actions 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 Oct 25, 2025

grunweg force-pushed the diffgeo-use-custom-elaborators branch 4 times, most recently from 44eca30 to 5644ca6 Compare October 25, 2025 22:36

grunweg mentioned this pull request Oct 27, 2025

[Merged by Bors] - feat: beta reduce in the T% elaborator #30879

Closed

1 task

mathlib4-merge-conflict-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 Oct 28, 2025

Support Euclidean half-space (with tests)

643cf57

grunweg added 2 commits February 23, 2026 19:16

Merge branch 'master' into diffgeo-use-custom-elaborators

1bb2ea2

Fix outdated comment

2e335fd

github-actions 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 Feb 23, 2026

grunweg added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-bench This PR needs to be benchmarked before merging labels Feb 23, 2026

One more

289de6f

mathlib-merge-conflicts 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 Mar 2, 2026

grunweg added a commit to grunweg/mathlib4 that referenced this pull request Mar 5, 2026

chore: golf using custom elaborators

961959c

The final pieces from leanprover-community#30357.

grunweg mentioned this pull request Mar 5, 2026

[Merged by Bors] - chore: golf using custom elaborators #36235

Closed

mathlib-bors bot pushed a commit that referenced this pull request Mar 6, 2026

chore: golf using custom elaborators (#36235)

1921cda

The final pieces from #30357.

grunweg closed this Mar 7, 2026

grunweg deleted the diffgeo-use-custom-elaborators branch March 7, 2026 12:31

xroblot pushed a commit to xroblot/mathlib4 that referenced this pull request Mar 8, 2026

chore: golf using custom elaborators (leanprover-community#36235)

fcaaa20

The final pieces from leanprover-community#30357.

xroblot pushed a commit to xroblot/mathlib4 that referenced this pull request Mar 9, 2026

chore: golf using custom elaborators (leanprover-community#36235)

ef77f97

The final pieces from leanprover-community#30357.

seewoo5 pushed a commit to seewoo5/mathlib4 that referenced this pull request Mar 9, 2026

chore: golf using custom elaborators (leanprover-community#36235)

358ac49

The final pieces from leanprover-community#30357.

xroblot pushed a commit to xroblot/mathlib4 that referenced this pull request Mar 10, 2026

chore: golf using custom elaborators (leanprover-community#36235)

32ed4c2

The final pieces from leanprover-community#30357.

Conversation

grunweg commented Oct 9, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Oct 9, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 4166dc3b98

Import changes for modified files

Declarations diff

Uh oh!

grunweg commented Oct 10, 2025

Uh oh!

leanprover-bot commented Oct 10, 2025

Uh oh!

github-actions bot commented Oct 10, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Oct 14, 2025

Uh oh!

grunweg commented Oct 27, 2025

Uh oh!

grunweg commented Oct 27, 2025

Uh oh!

leanprover-bot commented Oct 27, 2025

Uh oh!

mathlib4-merge-conflict-bot commented Oct 28, 2025

Uh oh!

grunweg commented Feb 27, 2026

Uh oh!

leanprover-radar commented Feb 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib-merge-conflicts bot commented Mar 2, 2026

Uh oh!

grunweg commented Mar 7, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

grunweg commented Oct 9, 2025 •

edited

Loading

github-actions bot commented Oct 9, 2025 •

edited

Loading

leanprover-radar commented Feb 27, 2026 •

edited

Loading