[Merged by Bors] - perf: remove overspecified fields by mattrobball · Pull Request #6965 · leanprover-community/mathlib4

mattrobball · 2023-09-05T17:29:09Z

This removes redundant field values of the form add := add for smaller terms and less unfolding during unification.

A list of all files containing a structure instance of the form { a1, ... with x1 := val, ... } where some xi is a field of some aj was generated by modifying the structure instance elaboration algorithm to print such overlaps to stdout in a custom toolchain.

Using that toolchain, I went through each file on the list and attempted to remove algebraic fields that overlapped and were redundant, eg add := add and not toFun (though some other ones did creep in). If things broke (which was the case in a couple of cases), I did not push further and reverted.

It is possible that pushing harder and trying to remove all redundant overlaps will yield further improvements.

jcommelin · 2023-09-05T18:27:47Z

You checked in an .olean file. I guess that isn't what you intended.

mattrobball · 2023-09-05T18:35:18Z

No. I wasn’t being careful because none of this really works. It is more for ease of communication at the moment.

Eventually, there will be a real toolchain here with changes that will be benched.

mattrobball · 2023-09-06T08:49:34Z

!bench

leanprover-bot · 2023-09-06T10:32:16Z

Here are the benchmark results for commit 27719fb.
There were significant changes against commit 2f410e1:

  Benchmark                                              Metric         Change
  ============================================================================
+ build                                                  maxrss          -7.7%
- ~Mathlib.Algebra.Category.ModuleCat.EpiMono            instructions     8.6%
- ~Mathlib.Algebra.Category.ModuleCat.Subobject          instructions     5.5%
+ ~Mathlib.Algebra.Category.Ring.Adjunctions             instructions    -7.6%
+ ~Mathlib.Algebra.DirectSum.Ring                        instructions   -24.2%
+ ~Mathlib.Algebra.EuclideanDomain.Instances             instructions   -17.1%
+ ~Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra          instructions   -10.7%
+ ~Mathlib.Algebra.Group.TypeTags                        instructions    -6.8%
+ ~Mathlib.Algebra.GroupRingAction.Subobjects            instructions    -6.0%
+ ~Mathlib.Algebra.Lie.Engel                             instructions    -5.5%
+ ~Mathlib.Algebra.Lie.Matrix                            instructions    -6.6%
+ ~Mathlib.Algebra.Lie.OfAssociative                     instructions   -11.2%
+ ~Mathlib.Algebra.MonoidAlgebra.Basic                   instructions    -9.2%
+ ~Mathlib.Algebra.MonoidAlgebra.Grading                 instructions   -18.9%
+ ~Mathlib.Algebra.Order.Pi                              instructions   -14.6%
+ ~Mathlib.Algebra.Order.Ring.WithTop                    instructions   -19.6%
+ ~Mathlib.Algebra.Ring.Defs                             instructions    -6.0%
+ ~Mathlib.Algebra.Star.Module                           instructions   -14.1%
+ ~Mathlib.Algebra.Symmetrized                           instructions    -5.8%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Point         instructions    -9.1%
+ ~Mathlib.Analysis.Calculus.IteratedDeriv               instructions    -5.0%
+ ~Mathlib.Analysis.NormedSpace.Completion               instructions    -6.6%
+ ~Mathlib.Analysis.NormedSpace.Dual                     instructions   -33.9%
+ ~Mathlib.Analysis.NormedSpace.Multilinear              instructions    -6.0%
+ ~Mathlib.Data.MvPolynomial.Funext                      instructions    -6.1%
+ ~Mathlib.Data.Polynomial.Monomial                      instructions    -8.9%
+ ~Mathlib.FieldTheory.Cardinality                       instructions   -54.6%
+ ~Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure      instructions   -16.6%
+ ~Mathlib.FieldTheory.MvPolynomial                      instructions   -14.2%
+ ~Mathlib.FieldTheory.PolynomialGaloisGroup             instructions    -8.1%
+ ~Mathlib.FieldTheory.SplittingField.Construction       instructions   -22.1%
- ~Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional   instructions     5.6%
- ~Mathlib.LinearAlgebra.AffineSpace.Restrict            instructions     7.3%
+ ~Mathlib.LinearAlgebra.Charpoly.Basic                  instructions    -5.8%
+ ~Mathlib.LinearAlgebra.DirectSum.Finsupp               instructions   -14.0%
- ~Mathlib.LinearAlgebra.DirectSum.TensorProduct         instructions    11.5%
+ ~Mathlib.LinearAlgebra.FiniteDimensional               instructions   -10.4%
+ ~Mathlib.LinearAlgebra.FreeAlgebra                     instructions    -6.7%
- ~Mathlib.LinearAlgebra.FreeModule.Finite.Rank          instructions     6.5%
- ~Mathlib.LinearAlgebra.Isomorphisms                    instructions    40.7%
- ~Mathlib.LinearAlgebra.Matrix.Charpoly.Basic           instructions     5.4%
+ ~Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff           instructions    -6.5%
+ ~Mathlib.NumberTheory.LegendreSymbol.GaussSum          instructions    -7.9%
+ ~Mathlib.NumberTheory.NumberField.Norm                 instructions    -5.7%
+ ~Mathlib.RepresentationTheory.Maschke                  instructions    -6.0%
+ ~Mathlib.RingTheory.FinitePresentation                 instructions   -26.8%
+ ~Mathlib.RingTheory.FreeCommRing                       instructions    -9.5%
- ~Mathlib.RingTheory.MatrixAlgebra                      instructions    12.4%
+ ~Mathlib.RingTheory.MvPolynomial.Homogeneous           instructions    -5.8%
+ ~Mathlib.RingTheory.MvPolynomial.Ideal                 instructions    -6.8%
+ ~Mathlib.RingTheory.Nullstellensatz                    instructions   -22.5%
+ ~Mathlib.RingTheory.Polynomial.Basic                   instructions    -5.9%
+ ~Mathlib.RingTheory.Polynomial.GaussLemma              instructions    -5.9%
- ~Mathlib.RingTheory.Polynomial.Vieta                   instructions     6.3%
+ ~Mathlib.RingTheory.RootsOfUnity.Minpoly               instructions   -35.2%
- ~Mathlib.RingTheory.SimpleModule                       instructions    24.2%
+ ~Mathlib.RingTheory.WittVector.Basic                   instructions    -6.5%
+ ~Mathlib.RingTheory.WittVector.Defs                    instructions    -9.2%
+ ~Mathlib.RingTheory.WittVector.Teichmuller             instructions   -15.1%
+ ~Mathlib.RingTheory.WittVector.WittPolynomial          instructions    -7.3%

jcommelin · 2023-09-07T09:38:18Z

Looks like you checked in an .olean file again.

again

mattrobball · 2023-09-07T15:32:54Z

I am not sure how it keeps happening...

sgouezel

This is clearly a step in the right direction, opening the way to other improvements. Can you maybe explain in the PR description how you found those? (And in particular if you expect to have catched all of them, or if it was just a random selection)?

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

Mathlib/Algebra/GroupRingAction/Basic.lean

Mathlib/Algebra/Module/Submodule/Basic.lean

sgouezel · 2023-09-07T17:16:02Z

Mathlib/FieldTheory/RatFunc.lean

 instance instCommRing : CommRing (RatFunc K) :=
  { instCommMonoid K, instAddCommGroup K with
-    add := (· + ·)
    zero := 0


how come you still need the zero and the sub, while you have instAddCommGroup K above?

This broke and I didn't push it.

mattrobball · 2023-09-07T18:37:44Z

This is clearly a step in the right direction, opening the way to other improvements. Can you maybe explain in the PR description how you found those? (And in particular if you expect to have catched all of them, or if it was just a random selection)?

I expanded. Please let me know how it reads. What I did was kinda hacky. The correct thing to do is to make a Lean.Linter which checks the overlaps for syntactic equality (up to some reasonable differences) and complains if so. Mario had some thoughts on this.

mattrobball · 2023-09-12T01:43:14Z

!bench

leanprover-bot · 2023-09-12T02:16:55Z

Here are the benchmark results for commit e3fe071.
There were significant changes against commit eae0fe5:

  Benchmark                                                           Metric         Change
  =========================================================================================
+ lint                                                                wall-clock      -8.0%
- ~Mathlib.Algebra.Category.ModuleCat.EpiMono                         instructions    13.9%
- ~Mathlib.Algebra.Category.ModuleCat.Images                          instructions     8.9%
- ~Mathlib.Algebra.Category.ModuleCat.Kernels                         instructions     5.6%
- ~Mathlib.Algebra.Category.ModuleCat.Subobject                       instructions    12.7%
+ ~Mathlib.Algebra.Category.Ring.Adjunctions                          instructions    -7.6%
+ ~Mathlib.Algebra.DirectSum.Ring                                     instructions   -24.2%
+ ~Mathlib.Algebra.EuclideanDomain.Instances                          instructions   -18.1%
+ ~Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra                       instructions   -10.8%
+ ~Mathlib.Algebra.Group.TypeTags                                     instructions    -7.0%
+ ~Mathlib.Algebra.GroupRingAction.Subobjects                         instructions    -6.0%
- ~Mathlib.Algebra.Lie.Abelian                                        instructions    17.2%
+ ~Mathlib.Algebra.Lie.Engel                                          instructions    -6.2%
+ ~Mathlib.Algebra.Lie.Free                                           instructions    -5.5%
+ ~Mathlib.Algebra.Lie.Matrix                                         instructions    -6.5%
+ ~Mathlib.Algebra.Lie.OfAssociative                                  instructions   -10.9%
- ~Mathlib.Algebra.Lie.Semisimple                                     instructions    27.6%
- ~Mathlib.Algebra.Lie.Solvable                                       instructions    10.4%
- ~Mathlib.Algebra.Lie.Submodule                                      instructions     8.1%
- ~Mathlib.Algebra.Lie.TensorProduct                                  instructions    12.4%
- ~Mathlib.Algebra.Lie.Weights                                        instructions    20.9%
- ~Mathlib.Algebra.LinearRecurrence                                   instructions     9.2%
- ~Mathlib.Algebra.Module.Zlattice                                    instructions    18.2%
+ ~Mathlib.Algebra.MonoidAlgebra.Basic                                instructions    -9.4%
+ ~Mathlib.Algebra.MonoidAlgebra.Grading                              instructions   -19.6%
+ ~Mathlib.Algebra.Order.Pi                                           instructions   -14.7%
+ ~Mathlib.Algebra.Order.Ring.WithTop                                 instructions   -19.6%
+ ~Mathlib.Algebra.Ring.Defs                                          instructions    -6.6%
+ ~Mathlib.Algebra.Star.Module                                        instructions   -18.6%
+ ~Mathlib.Algebra.Symmetrized                                        instructions    -5.9%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Point                      instructions    -9.1%
+ ~Mathlib.Analysis.Calculus.IteratedDeriv                            instructions    -5.0%
- ~Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho                instructions    11.5%
- ~Mathlib.Analysis.InnerProductSpace.Projection                      instructions    14.2%
+ ~Mathlib.Analysis.NormedSpace.Completion                            instructions    -6.6%
+ ~Mathlib.Analysis.NormedSpace.Dual                                  instructions   -33.9%
- ~Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit   instructions     8.8%
- ~Mathlib.CategoryTheory.Monad.Basic                                 instructions     9.3%
- ~Mathlib.Data.Matrix.Rank                                           instructions    21.9%
+ ~Mathlib.Data.MvPolynomial.Funext                                   instructions    -6.0%
+ ~Mathlib.Data.Polynomial.Laurent                                    instructions    -5.1%
+ ~Mathlib.Data.Polynomial.Monomial                                   instructions    -9.7%
+ ~Mathlib.FieldTheory.Cardinality                                    instructions   -54.6%
+ ~Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure                   instructions   -16.7%
+ ~Mathlib.FieldTheory.MvPolynomial                                   instructions   -14.9%
+ ~Mathlib.FieldTheory.PolynomialGaloisGroup                          instructions    -8.3%
+ ~Mathlib.FieldTheory.SplittingField.Construction                    instructions   -19.5%
- ~Mathlib.Geometry.Euclidean.Circumcenter                            instructions    11.6%
- ~Mathlib.Geometry.Euclidean.Inversion.Calculus                      instructions     9.4%
- ~Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional                instructions    24.1%
- ~Mathlib.LinearAlgebra.AffineSpace.Restrict                         instructions    17.0%
+ ~Mathlib.LinearAlgebra.Charpoly.Basic                               instructions    -5.8%
- ~Mathlib.LinearAlgebra.Dimension                                    instructions     8.4%
+ ~Mathlib.LinearAlgebra.DirectSum.Finsupp                            instructions   -13.9%
- ~Mathlib.LinearAlgebra.DirectSum.TensorProduct                      instructions    11.5%
- ~Mathlib.LinearAlgebra.Eigenspace.Basic                             instructions    20.2%
- ~Mathlib.LinearAlgebra.FiniteDimensional                            instructions     7.4%
- ~Mathlib.LinearAlgebra.Finrank                                      instructions    17.7%
+ ~Mathlib.LinearAlgebra.FreeAlgebra                                  instructions    -6.9%
- ~Mathlib.LinearAlgebra.FreeModule.Finite.Rank                       instructions    33.5%
- ~Mathlib.LinearAlgebra.Isomorphisms                                 instructions    37.2%
- ~Mathlib.LinearAlgebra.Matrix.Charpoly.Basic                        instructions     5.5%
+ ~Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff                        instructions    -6.3%
- ~Mathlib.LinearAlgebra.Matrix.Diagonal                              instructions     8.5%
- ~Mathlib.LinearAlgebra.Projection                                   instructions     6.2%
- ~Mathlib.LinearAlgebra.ProjectiveSpace.Basic                        instructions     8.5%
- ~Mathlib.LinearAlgebra.TensorAlgebra.Grading                        instructions    12.4%
- ~Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2    instructions     5.4%
+ ~Mathlib.NumberTheory.LegendreSymbol.GaussSum                       instructions    -7.9%
+ ~Mathlib.NumberTheory.NumberField.Norm                              instructions    -6.0%
- ~Mathlib.Probability.ConditionalExpectation                         instructions    66.0%
- ~Mathlib.RingTheory.Artinian                                        instructions     7.2%
+ ~Mathlib.RingTheory.FinitePresentation                              instructions   -24.3%
+ ~Mathlib.RingTheory.FreeCommRing                                    instructions   -10.0%
- ~Mathlib.RingTheory.Ideal.Cotangent                                 instructions    17.7%
- ~Mathlib.RingTheory.MatrixAlgebra                                   instructions    12.6%
+ ~Mathlib.RingTheory.MvPolynomial.Homogeneous                        instructions    -5.3%
+ ~Mathlib.RingTheory.MvPolynomial.Ideal                              instructions    -6.8%
+ ~Mathlib.RingTheory.Nullstellensatz                                 instructions   -22.3%
+ ~Mathlib.RingTheory.Polynomial.Basic                                instructions    -5.8%
+ ~Mathlib.RingTheory.Polynomial.GaussLemma                           instructions    -6.1%
+ ~Mathlib.RingTheory.Polynomial.Quotient                             instructions    -5.3%
- ~Mathlib.RingTheory.Polynomial.Vieta                                instructions     6.2%
+ ~Mathlib.RingTheory.RootsOfUnity.Minpoly                            instructions   -35.2%
- ~Mathlib.RingTheory.SimpleModule                                    instructions    31.1%
+ ~Mathlib.RingTheory.WittVector.Basic                                instructions    -7.5%
+ ~Mathlib.RingTheory.WittVector.Defs                                 instructions    -9.4%
+ ~Mathlib.RingTheory.WittVector.Teichmuller                          instructions   -15.9%
+ ~Mathlib.RingTheory.WittVector.WittPolynomial                       instructions    -7.2%
- ~Mathlib.Topology.Algebra.UniformConvergence                        instructions    12.0%

works but out of scope

jcommelin · 2023-09-14T18:23:19Z

!bench

leanprover-bot · 2023-09-14T19:21:04Z

Here are the benchmark results for commit 77b1bfa.
There were significant changes against commit eae0fe5:

  Benchmark                                              Metric         Change
  ============================================================================
+ lint                                                   wall-clock      -9.0%
- ~Mathlib.Algebra.Category.ModuleCat.EpiMono            instructions     8.7%
- ~Mathlib.Algebra.Category.ModuleCat.Subobject          instructions     5.6%
+ ~Mathlib.Algebra.Category.Ring.Adjunctions             instructions    -7.6%
+ ~Mathlib.Algebra.DirectSum.Ring                        instructions   -24.2%
+ ~Mathlib.Algebra.EuclideanDomain.Instances             instructions   -17.8%
+ ~Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra          instructions   -10.9%
+ ~Mathlib.Algebra.Group.TypeTags                        instructions    -6.9%
+ ~Mathlib.Algebra.GroupRingAction.Subobjects            instructions    -6.2%
+ ~Mathlib.Algebra.Lie.Engel                             instructions    -5.5%
+ ~Mathlib.Algebra.Lie.Matrix                            instructions    -6.6%
+ ~Mathlib.Algebra.Lie.OfAssociative                     instructions   -11.2%
+ ~Mathlib.Algebra.MonoidAlgebra.Basic                   instructions    -9.3%
+ ~Mathlib.Algebra.MonoidAlgebra.Grading                 instructions   -18.8%
+ ~Mathlib.Algebra.Order.Pi                              instructions   -14.7%
+ ~Mathlib.Algebra.Order.Ring.WithTop                    instructions   -19.6%
+ ~Mathlib.Algebra.Ring.Defs                             instructions    -6.7%
+ ~Mathlib.Algebra.Star.Module                           instructions   -11.4%
+ ~Mathlib.Algebra.Symmetrized                           instructions    -5.5%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Point         instructions    -9.1%
+ ~Mathlib.Analysis.Calculus.IteratedDeriv               instructions    -5.0%
+ ~Mathlib.Analysis.NormedSpace.Completion               instructions    -6.6%
+ ~Mathlib.Analysis.NormedSpace.Dual                     instructions   -33.8%
+ ~Mathlib.Data.MvPolynomial.Funext                      instructions    -6.3%
+ ~Mathlib.Data.Polynomial.Laurent                       instructions    -5.0%
+ ~Mathlib.Data.Polynomial.Monomial                      instructions    -9.6%
+ ~Mathlib.FieldTheory.Cardinality                       instructions   -54.6%
+ ~Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure      instructions   -16.6%
+ ~Mathlib.FieldTheory.MvPolynomial                      instructions   -14.8%
+ ~Mathlib.FieldTheory.PolynomialGaloisGroup             instructions    -8.3%
+ ~Mathlib.FieldTheory.SplittingField.Construction       instructions   -19.5%
- ~Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional   instructions     5.6%
- ~Mathlib.LinearAlgebra.AffineSpace.Restrict            instructions     7.3%
+ ~Mathlib.LinearAlgebra.Charpoly.Basic                  instructions    -5.8%
+ ~Mathlib.LinearAlgebra.DirectSum.Finsupp               instructions   -13.9%
- ~Mathlib.LinearAlgebra.DirectSum.TensorProduct         instructions    11.5%
+ ~Mathlib.LinearAlgebra.FiniteDimensional               instructions   -10.3%
+ ~Mathlib.LinearAlgebra.FreeAlgebra                     instructions    -6.9%
- ~Mathlib.LinearAlgebra.FreeModule.Finite.Rank          instructions     6.5%
- ~Mathlib.LinearAlgebra.Isomorphisms                    instructions    40.7%
- ~Mathlib.LinearAlgebra.Matrix.Charpoly.Basic           instructions     5.7%
+ ~Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff           instructions    -6.4%
+ ~Mathlib.NumberTheory.LegendreSymbol.GaussSum          instructions    -7.9%
+ ~Mathlib.NumberTheory.NumberField.Norm                 instructions    -5.7%
+ ~Mathlib.RepresentationTheory.Maschke                  instructions    -6.2%
+ ~Mathlib.RingTheory.FinitePresentation                 instructions   -24.2%
+ ~Mathlib.RingTheory.FreeCommRing                       instructions    -9.9%
- ~Mathlib.RingTheory.MatrixAlgebra                      instructions    12.7%
+ ~Mathlib.RingTheory.MvPolynomial.Homogeneous           instructions    -6.0%
+ ~Mathlib.RingTheory.MvPolynomial.Ideal                 instructions    -6.8%
+ ~Mathlib.RingTheory.Nullstellensatz                    instructions   -22.5%
+ ~Mathlib.RingTheory.Polynomial.Basic                   instructions    -5.9%
+ ~Mathlib.RingTheory.Polynomial.GaussLemma              instructions    -6.1%
+ ~Mathlib.RingTheory.Polynomial.Quotient                instructions    -5.2%
- ~Mathlib.RingTheory.Polynomial.Vieta                   instructions     6.3%
+ ~Mathlib.RingTheory.RootsOfUnity.Minpoly               instructions   -35.1%
- ~Mathlib.RingTheory.SimpleModule                       instructions    24.2%
+ ~Mathlib.RingTheory.WittVector.Basic                   instructions    -7.6%
+ ~Mathlib.RingTheory.WittVector.Defs                    instructions    -9.4%
+ ~Mathlib.RingTheory.WittVector.Teichmuller             instructions   -16.0%
+ ~Mathlib.RingTheory.WittVector.WittPolynomial          instructions    -7.1%

jcommelin

bors d+

bors · 2023-09-14T19:25:14Z

✌️ mattrobball can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

mattrobball · 2023-09-14T19:51:32Z

bors merge

This removes redundant field values of the form `add := add` for smaller terms and less unfolding during unification. A list of all files containing a structure instance of the form `{ a1, ... with x1 := val, ... }` where some `xi` is a field of some `aj` was generated by modifying the structure instance elaboration algorithm to print such overlaps to stdout in a custom toolchain. Using that toolchain, I went through each file on the list and attempted to remove algebraic fields that overlapped and were redundant, eg `add := add` and not `toFun` (though some other ones did creep in). If things broke (which was the case in a couple of cases), I did not push further and reverted. It is possible that pushing harder and trying to remove all redundant overlaps will yield further improvements.

bors · 2023-09-14T20:45:07Z

Build failed (retrying...):

Build

This removes redundant field values of the form `add := add` for smaller terms and less unfolding during unification. A list of all files containing a structure instance of the form `{ a1, ... with x1 := val, ... }` where some `xi` is a field of some `aj` was generated by modifying the structure instance elaboration algorithm to print such overlaps to stdout in a custom toolchain. Using that toolchain, I went through each file on the list and attempted to remove algebraic fields that overlapped and were redundant, eg `add := add` and not `toFun` (though some other ones did creep in). If things broke (which was the case in a couple of cases), I did not push further and reverted. It is possible that pushing harder and trying to remove all redundant overlaps will yield further improvements.

bors · 2023-09-14T20:46:11Z

Build failed (retrying...):

Build

This removes redundant field values of the form `add := add` for smaller terms and less unfolding during unification. A list of all files containing a structure instance of the form `{ a1, ... with x1 := val, ... }` where some `xi` is a field of some `aj` was generated by modifying the structure instance elaboration algorithm to print such overlaps to stdout in a custom toolchain. Using that toolchain, I went through each file on the list and attempted to remove algebraic fields that overlapped and were redundant, eg `add := add` and not `toFun` (though some other ones did creep in). If things broke (which was the case in a couple of cases), I did not push further and reverted. It is possible that pushing harder and trying to remove all redundant overlaps will yield further improvements.

bors · 2023-09-14T20:47:50Z

Build failed (retrying...):

Build

mattrobball · 2023-09-15T14:59:11Z

bors merge

This removes redundant field values of the form `add := add` for smaller terms and less unfolding during unification. A list of all files containing a structure instance of the form `{ a1, ... with x1 := val, ... }` where some `xi` is a field of some `aj` was generated by modifying the structure instance elaboration algorithm to print such overlaps to stdout in a custom toolchain. Using that toolchain, I went through each file on the list and attempted to remove algebraic fields that overlapped and were redundant, eg `add := add` and not `toFun` (though some other ones did creep in). If things broke (which was the case in a couple of cases), I did not push further and reverted. It is possible that pushing harder and trying to remove all redundant overlaps will yield further improvements.

bors · 2023-09-15T15:42:24Z

This PR was included in a batch that was canceled, it will be automatically retried

This removes redundant field values of the form `add := add` for smaller terms and less unfolding during unification. A list of all files containing a structure instance of the form `{ a1, ... with x1 := val, ... }` where some `xi` is a field of some `aj` was generated by modifying the structure instance elaboration algorithm to print such overlaps to stdout in a custom toolchain. Using that toolchain, I went through each file on the list and attempted to remove algebraic fields that overlapped and were redundant, eg `add := add` and not `toFun` (though some other ones did creep in). If things broke (which was the case in a couple of cases), I did not push further and reverted. It is possible that pushing harder and trying to remove all redundant overlaps will yield further improvements.

bors · 2023-09-15T17:45:38Z

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

This removes redundant field values of the form `add := add` for smaller terms and less unfolding during unification. A list of all files containing a structure instance of the form `{ a1, ... with x1 := val, ... }` where some `xi` is a field of some `aj` was generated by modifying the structure instance elaboration algorithm to print such overlaps to stdout in a custom toolchain. Using that toolchain, I went through each file on the list and attempted to remove algebraic fields that overlapped and were redundant, eg `add := add` and not `toFun` (though some other ones did creep in). If things broke (which was the case in a couple of cases), I did not push further and reverted. It is possible that pushing harder and trying to remove all redundant overlaps will yield further improvements.

new collisions

d435bc6

mattrobball marked this pull request as draft September 5, 2023 18:34

mattrobball added 8 commits September 5, 2023 14:35

remove olean

5b7c9d4

changes

48b72f1

restore toolchain

c384fdf

remove collisions

fa20c8c

fix one good; fix one bad

e6ef9a4

fixes

18bda7f

fix

a8b1eaf

nolint

27719fb

add pr toolchain

c646fc3

mattrobball marked this pull request as ready for review September 7, 2023 00:29

mattrobball added the awaiting-review label Sep 7, 2023

restore toolchain

ca16678

remove olean

933dd66

again

sgouezel reviewed Sep 7, 2023

View reviewed changes

jcommelin requested a review from sgouezel September 8, 2023 04:30

ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Sep 8, 2023

leanprover-community deleted a comment from leanprover-bot Sep 12, 2023

mattrobball added 7 commits September 12, 2023 15:08

remove changes

ae4b9c1

nolint

e9a6aef

restore

4e92a7f

clean up

9d2fbe2

restore

e999eab

works but out of scope

remove

a143c37

remove

77b1bfa

jcommelin approved these changes Sep 14, 2023

View reviewed changes

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Sep 14, 2023

Merge branch 'master' into mrb/no_bad_add

f4e6926

bors bot changed the title ~~perf: remove overspecified fields~~ [Merged by Bors] - perf: remove overspecified fields Sep 15, 2023

bors bot closed this Sep 15, 2023

bors bot deleted the mrb/no_bad_add branch September 15, 2023 17:45

Conversation

mattrobball commented Sep 5, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jcommelin commented Sep 5, 2023

Uh oh!

mattrobball commented Sep 5, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mattrobball commented Sep 6, 2023

Uh oh!

leanprover-bot commented Sep 6, 2023

Uh oh!

jcommelin commented Sep 7, 2023

Uh oh!

mattrobball commented Sep 7, 2023

Uh oh!

sgouezel left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

sgouezel Sep 7, 2023

Choose a reason for hiding this comment

Uh oh!

mattrobball Sep 7, 2023

Choose a reason for hiding this comment

Uh oh!

mattrobball commented Sep 7, 2023

Uh oh!

mattrobball commented Sep 12, 2023

Uh oh!

leanprover-bot commented Sep 12, 2023

Uh oh!

jcommelin commented Sep 14, 2023

Uh oh!

leanprover-bot commented Sep 14, 2023

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

bors bot commented Sep 14, 2023

Uh oh!

mattrobball commented Sep 14, 2023

Uh oh!

bors bot commented Sep 14, 2023

Uh oh!

bors bot commented Sep 14, 2023

Uh oh!

bors bot commented Sep 14, 2023

Uh oh!

mattrobball commented Sep 15, 2023

Uh oh!

bors bot commented Sep 15, 2023

Uh oh!

bors bot commented Sep 15, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

mattrobball commented Sep 5, 2023 •

edited

Loading

mattrobball commented Sep 5, 2023 •

edited

Loading