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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - chore: bump toolchain to v4.2.0-rc2 #7703

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - chore: bump toolchain to v4.2.0-rc2 #7703

wants to merge 1 commit into from

Conversation

semorrison
Copy link
Contributor

This includes all the changes from #7606.

Open in Gitpod

@semorrison semorrison added awaiting-review The author would like community review of the PR awaiting-CI labels Oct 16, 2023
@semorrison semorrison mentioned this pull request Oct 16, 2023
Closed
@PatrickMassot
Copy link
Member

bors d+

@bors
Copy link

bors bot commented Oct 16, 2023

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

@github-actions github-actions bot added delegated and removed awaiting-review The author would like community review of the PR labels Oct 16, 2023
@semorrison
Copy link
Contributor Author

!bench

@semorrison semorrison added the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label Oct 16, 2023
@leanprover-community-mathlib4-bot
Copy link
Collaborator

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

bors bot pushed a commit that referenced this pull request Oct 16, 2023
@semorrison
chore: bump toolchain to v4.2.0-rc2 (#7703)
26eb2b0 
This includes all the changes from #7606.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit d8f5691.
There were significant changes against commit 7f121a4:

  Benchmark                                                          Metric             Change
  ============================================================================================
+ build                                                              elaboration        -19.5%
+ build                                                              instructions       -11.3%
+ build                                                              interpretation      -7.9%
+ build                                                              simp                -6.9%
+ build                                                              tactic execution   -31.4%
+ build                                                              task-clock          -8.1%
+ build                                                              wall-clock         -14.4%
+ lint                                                               instructions        -7.0%
+ lint                                                               wall-clock         -10.9%
+ ~Mathlib.Algebra.Category.AlgebraCat.Limits                        instructions       -39.4%
+ ~Mathlib.Algebra.Category.AlgebraCat.Monoidal                      instructions       -29.6%
+ ~Mathlib.Algebra.Category.FGModuleCat.Basic                        instructions       -88.6%
+ ~Mathlib.Algebra.Category.ModuleCat.Adjunctions                    instructions       -17.1%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings                  instructions        -2.6%
+ ~Mathlib.Algebra.Category.ModuleCat.Colimits                       instructions       -45.5%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic                 instructions       -31.5%
+ ~Mathlib.Algebra.Category.Ring.Limits                              instructions       -33.1%
+ ~Mathlib.Algebra.DirectLimit                                       instructions       -20.5%
+ ~Mathlib.Algebra.Homology.Augment                                  instructions       -16.3%
+ ~Mathlib.Algebra.Homology.DifferentialObject                       instructions        -5.5%
+ ~Mathlib.Algebra.Homology.LocalCohomology                          instructions       -77.7%
+ ~Mathlib.Algebra.Homology.ModuleCat                                instructions       -23.7%
+ ~Mathlib.Algebra.Jordan.Basic                                      instructions        -7.1%
+ ~Mathlib.Algebra.Lie.Matrix                                        instructions       -34.6%
+ ~Mathlib.Algebra.Lie.TensorProduct                                 instructions       -35.4%
+ ~Mathlib.Algebra.Lie.UniversalEnveloping                           instructions       -52.0%
+ ~Mathlib.Algebra.Lie.Weights.Cartan                                instructions       -25.3%
+ ~Mathlib.Algebra.Module.GradedModule                               instructions        -7.4%
+ ~Mathlib.Algebra.Module.PID                                        instructions       -38.5%
+ ~Mathlib.Algebra.Module.Torsion                                    instructions       -13.2%
+ ~Mathlib.Algebra.MonoidAlgebra.Grading                             instructions       -24.7%
+ ~Mathlib.AlgebraicGeometry.AffineScheme                            instructions       -47.1%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Point                     instructions       -17.6%
+ ~Mathlib.AlgebraicGeometry.FunctionField                           instructions       -26.4%
+ ~Mathlib.AlgebraicGeometry.GammaSpecAdjunction                     instructions       -73.2%
+ ~Mathlib.AlgebraicGeometry.Gluing                                  instructions       -11.8%
+ ~Mathlib.AlgebraicGeometry.Morphisms.Basic                         instructions       -22.4%
+ ~Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated                instructions        -6.9%
+ ~Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties             instructions       -16.9%
+ ~Mathlib.AlgebraicGeometry.OpenImmersion                           instructions        -9.8%
+ ~Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf       instructions       -13.2%
+ ~Mathlib.AlgebraicGeometry.Pullbacks                               instructions       -18.6%
+ ~Mathlib.AlgebraicGeometry.Scheme                                  instructions       -50.2%
+ ~Mathlib.AlgebraicGeometry.Spec                                    instructions       -56.1%
+ ~Mathlib.AlgebraicGeometry.StructureSheaf                          instructions       -13.9%
+ ~Mathlib.Analysis.Analytic.Basic                                   instructions       -12.8%
+ ~Mathlib.Analysis.Analytic.Composition                             instructions       -17.8%
+ ~Mathlib.Analysis.Analytic.Inverse                                 instructions       -31.2%
+ ~Mathlib.Analysis.BoxIntegral.Partition.Split                      instructions       -47.5%
+ ~Mathlib.Analysis.Calculus.ContDiff                                instructions       -24.1%
+ ~Mathlib.Analysis.Calculus.ContDiffDef                             instructions       -44.7%
+ ~Mathlib.Analysis.Calculus.Deriv.Mul                               instructions        -9.1%
+ ~Mathlib.Analysis.Calculus.FDeriv.Analytic                         instructions       -41.0%
+ ~Mathlib.Analysis.Calculus.Series                                  instructions       -51.1%
+ ~Mathlib.Analysis.Complex.PhragmenLindelof                         instructions       -20.2%
+ ~Mathlib.Analysis.Complex.RealDeriv                                instructions       -19.1%
+ ~Mathlib.Analysis.Complex.UpperHalfPlane.Basic                     instructions       -53.7%
+ ~Mathlib.Analysis.Complex.UpperHalfPlane.Metric                    instructions       -12.9%
+ ~Mathlib.Analysis.Convolution                                      instructions       -17.2%
+ ~Mathlib.Analysis.Distribution.SchwartzSpace                       instructions        -7.0%
+ ~Mathlib.Analysis.Fourier.AddCircle                                instructions       -35.1%
+ ~Mathlib.Analysis.Fourier.PoissonSummation                         instructions       -50.5%
+ ~Mathlib.Analysis.Fourier.RiemannLebesgueLemma                     instructions       -48.5%
+ ~Mathlib.Analysis.InnerProductSpace.Adjoint                        instructions        -9.5%
+ ~Mathlib.Analysis.InnerProductSpace.Basic                          instructions        -9.6%
+ ~Mathlib.Analysis.InnerProductSpace.Dual                           instructions       -22.9%
+ ~Mathlib.Analysis.InnerProductSpace.PiL2                           instructions        -5.5%
+ ~Mathlib.Analysis.InnerProductSpace.Projection                     instructions        -5.1%
+ ~Mathlib.Analysis.InnerProductSpace.TwoDim                         instructions        -8.9%
+ ~Mathlib.Analysis.MeanInequalities                                 instructions       -43.8%
+ ~Mathlib.Analysis.NormedSpace.LpEquiv                              instructions       -23.3%
+ ~Mathlib.Analysis.NormedSpace.Multilinear                          instructions       -33.1%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm                         instructions       -23.4%
+ ~Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus    instructions       -42.6%
+ ~Mathlib.Analysis.NormedSpace.Star.GelfandDuality                  instructions       -21.2%
+ ~Mathlib.Analysis.NormedSpace.Star.Multiplier                      instructions        -4.9%
+ ~Mathlib.Analysis.SpecialFunctions.Complex.Arg                     instructions       -22.8%
+ ~Mathlib.Analysis.SpecialFunctions.Gamma.Basic                     instructions       -23.2%
+ ~Mathlib.Analysis.SpecialFunctions.Gaussian                        instructions       -52.1%
+ ~Mathlib.Analysis.SpecialFunctions.Pow.Deriv                       instructions       -13.1%
+ ~Mathlib.Analysis.SpecialFunctions.Pow.Real                        instructions       -27.8%
+ ~Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic             instructions       -73.4%
+ ~Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds            instructions       -42.6%
+ ~Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv             instructions       -22.4%
+ ~Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd     instructions       -33.7%
- ~Mathlib.CategoryTheory.Abelian.InjectiveResolution                instructions         3.4%
+ ~Mathlib.CategoryTheory.Abelian.LeftDerived                        instructions       -40.3%
+ ~Mathlib.CategoryTheory.Abelian.RightDerived                       instructions       -45.7%
- ~Mathlib.CategoryTheory.Abelian.Transfer                           instructions         5.9%
+ ~Mathlib.CategoryTheory.Monoidal.Bimod                             instructions       -22.6%
+ ~Mathlib.CategoryTheory.Monoidal.Free.Coherence                    instructions       -25.6%
+ ~Mathlib.Combinatorics.Additive.Behrend                            instructions       -38.4%
+ ~Mathlib.Data.Matrix.Rank                                          instructions       -20.2%
+ ~Mathlib.Data.Nat.Basic                                            instructions       -53.8%
+ ~Mathlib.Data.Real.ENNReal                                         instructions        -9.9%
+ ~Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber          instructions        -5.6%
+ ~Mathlib.FieldTheory.AbelRuffini                                   instructions       -19.3%
+ ~Mathlib.FieldTheory.Adjoin                                        instructions       -19.7%
+ ~Mathlib.FieldTheory.Cardinality                                   instructions       -70.5%
+ ~Mathlib.FieldTheory.Fixed                                         instructions       -22.1%
+ ~Mathlib.FieldTheory.Galois                                        instructions       -28.0%
+ ~Mathlib.FieldTheory.IntermediateField                             instructions       -21.3%
+ ~Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure                  instructions       -57.3%
+ ~Mathlib.FieldTheory.IsAlgClosed.Basic                             instructions       -13.0%
+ ~Mathlib.FieldTheory.Normal                                        instructions       -12.2%
+ ~Mathlib.FieldTheory.NormalClosure                                 instructions       -23.4%
+ ~Mathlib.FieldTheory.PolynomialGaloisGroup                         instructions       -19.7%
+ ~Mathlib.FieldTheory.PrimitiveElement                              instructions       -22.0%
+ ~Mathlib.FieldTheory.RatFunc                                       instructions       -11.0%
+ ~Mathlib.FieldTheory.SplittingField.Construction                   instructions       -51.7%
+ ~Mathlib.Geometry.Euclidean.Angle.Oriented.Basic                   instructions       -60.3%
+ ~Mathlib.Geometry.Euclidean.Angle.Sphere                           instructions       -50.7%
+ ~Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle            instructions       -46.2%
+ ~Mathlib.Geometry.Euclidean.Basic                                  instructions       -12.9%
+ ~Mathlib.Geometry.Euclidean.Circumcenter                           instructions       -10.2%
+ ~Mathlib.Geometry.Euclidean.MongePoint                             instructions        -9.8%
+ ~Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation         instructions       -30.9%
+ ~Mathlib.Geometry.Manifold.ContMDiff                               instructions       -23.5%
+ ~Mathlib.Geometry.Manifold.DerivationBundle                        instructions       -17.0%
+ ~Mathlib.Geometry.Manifold.Instances.Sphere                        instructions       -16.8%
+ ~Mathlib.Geometry.RingedSpace.OpenImmersion                        instructions        -5.2%
+ ~Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing               instructions        -5.8%
+ ~Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits          instructions       -28.9%
+ ~Mathlib.GroupTheory.FiniteAbelian                                 instructions       -53.3%
+ ~Mathlib.GroupTheory.Solvable                                      instructions       -83.4%
+ ~Mathlib.GroupTheory.SpecificGroups.Alternating                    instructions       -47.7%
+ ~Mathlib.LinearAlgebra.AffineSpace.AffineSubspace                  instructions       -17.8%
+ ~Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional               instructions       -23.8%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange                  instructions       -49.2%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Basic                       instructions       -31.6%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation                 instructions       -28.7%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Contraction                 instructions       -48.4%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Even                        instructions       -21.1%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv                   instructions       -33.0%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Fold                        instructions       -29.7%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Grading                     instructions       -35.3%
+ ~Mathlib.LinearAlgebra.Dual                                        instructions       -26.7%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.Grading                     instructions       -38.4%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating               instructions       -24.8%
+ ~Mathlib.LinearAlgebra.FiniteDimensional                           instructions        -7.2%
+ ~Mathlib.LinearAlgebra.FinsuppVectorSpace                          instructions        -2.9%
+ ~Mathlib.LinearAlgebra.FreeModule.Norm                             instructions       -84.2%
+ ~Mathlib.LinearAlgebra.FreeModule.StrongRankCondition              instructions       -64.9%
+ ~Mathlib.LinearAlgebra.Isomorphisms                                instructions       -25.4%
+ ~Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup                   instructions       -27.3%
+ ~Mathlib.LinearAlgebra.Orientation                                 instructions       -24.4%
+ ~Mathlib.LinearAlgebra.TensorPower                                 instructions       -35.9%
+ ~Mathlib.LinearAlgebra.TensorProduct.Opposite                      instructions       -33.2%
+ ~Mathlib.LinearAlgebra.Trace                                       instructions       -11.2%
+ ~Mathlib.MeasureTheory.Decomposition.Lebesgue                      instructions        -9.9%
+ ~Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2   instructions       -10.3%
+ ~Mathlib.MeasureTheory.Function.Jacobian                           instructions       -18.4%
+ ~Mathlib.MeasureTheory.Function.LpSpace                            instructions       -11.8%
+ ~Mathlib.MeasureTheory.Function.UniformIntegrable                  instructions       -34.6%
+ ~Mathlib.MeasureTheory.Integral.Bochner                            instructions        -5.4%
+ ~Mathlib.MeasureTheory.Integral.CircleTransform                    instructions       -46.1%
+ ~Mathlib.MeasureTheory.Integral.SetIntegral                        instructions       -13.6%
+ ~Mathlib.MeasureTheory.Integral.SetToL1                            instructions        -7.5%
+ ~Mathlib.MeasureTheory.MeasurableSpace.Card                        instructions       -73.7%
+ ~Mathlib.MeasureTheory.Measure.Hausdorff                           instructions       -15.2%
+ ~Mathlib.MeasureTheory.Measure.MeasureSpace                        instructions        -6.7%
+ ~Mathlib.MeasureTheory.Measure.ProbabilityMeasure                  instructions       -22.6%
+ ~Mathlib.MeasureTheory.Measure.WithDensityVectorMeasure            instructions       -73.3%
+ ~Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots                    instructions       -12.7%
+ ~Mathlib.NumberTheory.Cyclotomic.Rat                               instructions       -12.0%
+ ~Mathlib.NumberTheory.KummerDedekind                               instructions       -28.6%
+ ~Mathlib.NumberTheory.LegendreSymbol.GaussSum                      instructions       -43.5%
+ ~Mathlib.NumberTheory.LegendreSymbol.ZModChar                      instructions       -90.6%
+ ~Mathlib.NumberTheory.LucasLehmer                                  instructions       -38.7%
+ ~Mathlib.NumberTheory.Modular                                      instructions       -32.2%
+ ~Mathlib.NumberTheory.ModularForms.Basic                           instructions       -72.7%
+ ~Mathlib.NumberTheory.ModularForms.CongruenceSubgroups             instructions       -68.9%
+ ~Mathlib.NumberTheory.ModularForms.SlashActions                    instructions       -65.1%
+ ~Mathlib.NumberTheory.NumberField.Basic                            instructions       -16.7%
+ ~Mathlib.NumberTheory.NumberField.CanonicalEmbedding               instructions        -9.2%
+ ~Mathlib.NumberTheory.NumberField.Norm                             instructions       -19.0%
+ ~Mathlib.NumberTheory.NumberField.Units                            instructions       -14.7%
+ ~Mathlib.NumberTheory.Padics.PadicIntegers                         instructions       -22.8%
+ ~Mathlib.NumberTheory.RamificationInertia                          instructions        -4.1%
+ ~Mathlib.NumberTheory.SumFourSquares                               instructions       -38.8%
+ ~Mathlib.NumberTheory.ZetaFunction                                 instructions       -29.5%
+ ~Mathlib.NumberTheory.ZetaValues                                   instructions       -25.9%
+ ~Mathlib.Probability.Variance                                      instructions       -21.8%
+ ~Mathlib.RepresentationTheory.Character                            instructions       -15.9%
+ ~Mathlib.RepresentationTheory.FdRep                                instructions       -54.9%
+ ~Mathlib.RepresentationTheory.GroupCohomology.Basic                instructions       -90.5%
+ ~Mathlib.RepresentationTheory.GroupCohomology.Resolution           instructions       -34.4%
+ ~Mathlib.RepresentationTheory.Rep                                  instructions       -33.2%
+ ~Mathlib.RingTheory.Adjoin.Field                                   instructions       -47.4%
+ ~Mathlib.RingTheory.AdjoinRoot                                     instructions       -12.1%
+ ~Mathlib.RingTheory.AlgebraicIndependent                           instructions       -12.6%
+ ~Mathlib.RingTheory.ClassGroup                                     instructions        -9.3%
+ ~Mathlib.RingTheory.DedekindDomain.AdicValuation                   instructions       -18.8%
+ ~Mathlib.RingTheory.DedekindDomain.IntegralClosure                 instructions       -19.8%
+ ~Mathlib.RingTheory.FinitePresentation                             instructions       -20.2%
+ ~Mathlib.RingTheory.Finiteness                                     instructions       -49.7%
+ ~Mathlib.RingTheory.GradedAlgebra.Basic                            instructions       -13.0%
+ ~Mathlib.RingTheory.Ideal.Norm                                     instructions       -33.0%
+ ~Mathlib.RingTheory.IntegralClosure                                instructions       -15.2%
+ ~Mathlib.RingTheory.Jacobson                                       instructions       -61.1%
+ ~Mathlib.RingTheory.JacobsonIdeal                                  instructions       -40.7%
+ ~Mathlib.RingTheory.Kaehler                                        instructions       -36.7%
+ ~Mathlib.RingTheory.LocalProperties                                instructions       -42.9%
+ ~Mathlib.RingTheory.MatrixAlgebra                                  instructions       -40.7%
+ ~Mathlib.RingTheory.Norm                                           instructions        -9.2%
+ ~Mathlib.RingTheory.Nullstellensatz                                instructions       -29.7%
+ ~Mathlib.RingTheory.Polynomial.Hermite.Basic                       instructions       -37.2%
+ ~Mathlib.RingTheory.Polynomial.Quotient                            instructions       -16.7%
+ ~Mathlib.RingTheory.TensorProduct                                  instructions        -9.5%
+ ~Mathlib.RingTheory.Trace                                          instructions       -10.5%
+ ~Mathlib.RingTheory.Valuation.ValuationSubring                     instructions       -10.1%
+ ~Mathlib.RingTheory.WittVector.InitTail                            instructions       -85.8%
+ ~Mathlib.RingTheory.WittVector.IsPoly                              instructions       -52.8%
+ ~Mathlib.SetTheory.Game.Birthday                                   instructions       -31.6%
+ ~Mathlib.SetTheory.Ordinal.NaturalOps                              instructions       -47.0%
+ ~Mathlib.SetTheory.ZFC.Basic                                       instructions       -42.8%
+ ~Mathlib.Topology.ContinuousFunction.Ideals                        instructions       -22.2%
+ ~Mathlib.Topology.ContinuousFunction.StoneWeierstrass              instructions       -15.6%
+ ~Mathlib.Topology.EMetricSpace.Basic                               instructions       -18.4%
+ ~Mathlib.Topology.Instances.ENNReal                                instructions       -14.0%
+ ~Mathlib.Topology.MetricSpace.GromovHausdorff                      instructions        -7.3%
+ ~Mathlib.Topology.Sheaves.Stalks                                   instructions       -11.3%
+ ~Mathlib.Topology.TietzeExtension                                  instructions       -34.7%

@bors
Copy link

bors bot commented Oct 16, 2023

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.

@bors bors bot changed the title chore: bump toolchain to v4.2.0-rc2 [Merged by Bors] - chore: bump toolchain to v4.2.0-rc2 Oct 16, 2023
@bors bors bot closed this Oct 16, 2023
@bors bors bot deleted the bump-v4.2.0-rc2 branch October 16, 2023 04:42
mattrobball added a commit that referenced this pull request Oct 16, 2023
@mattrobball
Revert "chore: bump toolchain to v4.2.0-rc2 (#7703)"
87e1348 
This reverts commit 26eb2b0.
bors bot pushed a commit that referenced this pull request Oct 16, 2023
@mattrobball
chore: revert #7703 (#7710)
f3695eb 
This reverts commit 26eb2b0.
@semorrison semorrison mentioned this pull request Oct 16, 2023
Merged
semorrison added a commit that referenced this pull request Oct 17, 2023
@semorrison
Revert "chore: revert #7703 (#7710)"
ab56fa2 
This reverts commit f3695eb.
@urkud urkud mentioned this pull request May 5, 2024
Closed
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
auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. delegated
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@semorrison @PatrickMassot @leanprover-community-mathlib4-bot @leanprover-bot