fix: !bench after Lake path changes#24143
Conversation
|
!bench |
PR summary a86c12eb12
|
| Files | Import difference |
|---|---|
Mathlib.Data.UInt |
-483 |
Mathlib.Algebra.Expr |
-40 |
Mathlib.Data.Num.Basic |
-36 |
Mathlib.Data.Tree.Get |
-34 |
Mathlib.Algebra.NeZero |
-29 |
Mathlib.Algebra.Order.ZeroLEOne |
-23 |
Mathlib.Data.PNat.Defs Mathlib.Testing.Plausible.Sampleable |
-20 |
9 filesMathlib.Data.PNat.Equiv Mathlib.Data.Set.Insert Mathlib.Data.Set.Subsingleton Mathlib.Logic.Function.FiberPartition Mathlib.Order.Bounded Mathlib.Order.Filter.Defs Mathlib.Order.Interval.Set.Basic Mathlib.Order.Interval.Set.LinearOrder Mathlib.SetTheory.PGame.Basic |
-16 |
78 filesMathlib.Combinatorics.Quiver.Arborescence Mathlib.Data.Bool.Set Mathlib.Data.Countable.Small Mathlib.Data.Nat.Set Mathlib.Data.Rel Mathlib.Data.Semiquot Mathlib.Data.Set.Accumulate Mathlib.Data.Set.BooleanAlgebra Mathlib.Data.Set.Function Mathlib.Data.Set.Functor Mathlib.Data.Set.Image Mathlib.Data.Set.Lattice.Image Mathlib.Data.Set.Lattice Mathlib.Data.Set.List Mathlib.Data.Set.Monotone Mathlib.Data.Set.NAry Mathlib.Data.Set.Pairwise.Basic Mathlib.Data.Set.Pairwise.Lattice Mathlib.Data.Set.Piecewise Mathlib.Data.Set.Prod Mathlib.Data.Set.Restrict Mathlib.Data.Set.Sigma Mathlib.Data.Set.Subset Mathlib.Data.Set.UnionLift Mathlib.Data.Setoid.Basic Mathlib.Logic.Embedding.Set Mathlib.Logic.Equiv.Embedding Mathlib.Logic.Equiv.PartialEquiv Mathlib.Logic.Equiv.Set Mathlib.Logic.Function.DependsOn Mathlib.Logic.Small.Basic Mathlib.Logic.Small.Set Mathlib.Order.Antichain Mathlib.Order.Bounds.Basic Mathlib.Order.Bounds.Image Mathlib.Order.Bounds.Lattice Mathlib.Order.Bounds.OrderIso Mathlib.Order.Chain Mathlib.Order.Closure Mathlib.Order.Cofinal Mathlib.Order.CompleteBooleanAlgebra Mathlib.Order.CompleteLattice.Basic Mathlib.Order.CompleteLattice.Chain Mathlib.Order.CompleteLattice.Defs Mathlib.Order.CompleteLattice.Lemmas Mathlib.Order.Concept Mathlib.Order.ConditionallyCompleteLattice.Basic Mathlib.Order.ConditionallyCompleteLattice.Defs Mathlib.Order.ConditionallyCompleteLattice.Indexed Mathlib.Order.Copy Mathlib.Order.Directed Mathlib.Order.Extension.Linear Mathlib.Order.GaloisConnection.Basic Mathlib.Order.Heyting.Regular Mathlib.Order.Hom.CompleteLattice Mathlib.Order.Hom.Order Mathlib.Order.Hom.Set Mathlib.Order.Interval.Basic Mathlib.Order.Interval.Set.Disjoint Mathlib.Order.Interval.Set.Image Mathlib.Order.Interval.Set.OrderIso Mathlib.Order.Interval.Set.SurjOn Mathlib.Order.Interval.Set.WithBotTop Mathlib.Order.LatticeIntervals Mathlib.Order.Minimal Mathlib.Order.Monotone.Extension Mathlib.Order.Monotone.Union Mathlib.Order.Nucleus Mathlib.Order.OrdContinuous Mathlib.Order.Preorder.Chain Mathlib.Order.Rel.GaloisConnection Mathlib.Order.RelIso.Set Mathlib.Order.ScottContinuity Mathlib.Order.Set Mathlib.Order.WellFounded Mathlib.Order.Zorn Mathlib.SetTheory.Cardinal.Defs Mathlib.SetTheory.ZFC.PSet |
-15 |
120 filesMathlib.Algebra.Order.Nonneg.Lattice Mathlib.Combinatorics.SetFamily.Intersecting Mathlib.Control.EquivFunctor.Instances Mathlib.Control.Functor.Multivariate Mathlib.Data.Fin.Basic Mathlib.Data.Fin.Fin2 Mathlib.Data.Fin.FlagRange Mathlib.Data.Fin.Rev Mathlib.Data.Fin.SuccPred Mathlib.Data.Fin.Tuple.Basic Mathlib.Data.Fin.Tuple.Curry Mathlib.Data.Fin.Tuple.Take Mathlib.Data.Fin.VecNotation Mathlib.Data.Finite.Set Mathlib.Data.Finset.Attach Mathlib.Data.Finset.Basic Mathlib.Data.Finset.BooleanAlgebra Mathlib.Data.Finset.Card Mathlib.Data.Finset.Dedup Mathlib.Data.Finset.Defs Mathlib.Data.Finset.Disjoint Mathlib.Data.Finset.Empty Mathlib.Data.Finset.Erase Mathlib.Data.Finset.Filter Mathlib.Data.Finset.Fin Mathlib.Data.Finset.Fold Mathlib.Data.Finset.Image Mathlib.Data.Finset.Insert Mathlib.Data.Finset.Lattice.Basic Mathlib.Data.Finset.Lattice.Lemmas Mathlib.Data.Finset.Order Mathlib.Data.Finset.Piecewise Mathlib.Data.Finset.Range Mathlib.Data.Finset.SDiff Mathlib.Data.Finset.SymmDiff Mathlib.Data.Fintype.Basic Mathlib.Data.Fintype.Card Mathlib.Data.Fintype.Defs Mathlib.Data.Fintype.EquivFin Mathlib.Data.Fintype.Inv Mathlib.Data.Fintype.OfMap Mathlib.Data.Fintype.Sets Mathlib.Data.Fintype.Shrink Mathlib.Data.List.ChainOfFn Mathlib.Data.List.FinRange Mathlib.Data.List.Lemmas Mathlib.Data.List.NodupEquivFin Mathlib.Data.List.OfFn Mathlib.Data.List.Permutation Mathlib.Data.List.Sort Mathlib.Data.List.Sublists Mathlib.Data.MLList.BestFirst Mathlib.Data.Multiset.Dedup Mathlib.Data.Multiset.Filter Mathlib.Data.Multiset.FinsetOps Mathlib.Data.Multiset.Fold Mathlib.Data.Multiset.Lattice Mathlib.Data.Multiset.MapFold Mathlib.Data.Multiset.NatAntidiagonal Mathlib.Data.Multiset.Range Mathlib.Data.Multiset.Sort Mathlib.Data.Multiset.UnionInter Mathlib.Data.Prod.TProd Mathlib.Data.Set.Constructions Mathlib.Data.Set.Finite.Basic Mathlib.Data.Set.Finite.Range Mathlib.Data.Set.Pairwise.List Mathlib.Data.TypeVec Mathlib.Data.Vector3 Mathlib.Logic.Equiv.Fin.Basic Mathlib.Logic.Equiv.Fintype Mathlib.Logic.Function.FromTypes Mathlib.Logic.Function.OfArity Mathlib.Order.Atoms Mathlib.Order.CompleteLatticeIntervals Mathlib.Order.Cover Mathlib.Order.DirectedInverseSystem Mathlib.Order.Fin.Basic Mathlib.Order.Fin.Finset Mathlib.Order.Fin.SuccAboveOrderIso Mathlib.Order.Fin.Tuple Mathlib.Order.InitialSeg Mathlib.Order.Interval.Set.Fin Mathlib.Order.Interval.Set.Infinite Mathlib.Order.Interval.Set.InitialSeg Mathlib.Order.Interval.Set.Limit Mathlib.Order.Interval.Set.Monotone Mathlib.Order.Interval.Set.OrdConnectedComponent Mathlib.Order.Interval.Set.OrdConnected Mathlib.Order.Interval.Set.OrderEmbedding Mathlib.Order.Interval.Set.ProjIcc Mathlib.Order.Interval.Set.SuccOrder Mathlib.Order.Interval.Set.SuccPred Mathlib.Order.Interval.Set.Union Mathlib.Order.Interval.Set.UnorderedInterval Mathlib.Order.IsNormal Mathlib.Order.ModularLattice Mathlib.Order.PiLex Mathlib.Order.Radical Mathlib.Order.Shrink Mathlib.Order.SuccPred.Archimedean Mathlib.Order.SuccPred.Basic Mathlib.Order.SuccPred.CompleteLinearOrder Mathlib.Order.SuccPred.InitialSeg Mathlib.Order.SuccPred.IntervalSucc Mathlib.Order.SuccPred.Limit Mathlib.Order.SuccPred.Relation Mathlib.Order.SuccPred.Tree Mathlib.Order.SuccPred.WithBot Mathlib.Order.TransfiniteIteration Mathlib.Order.UpperLower.Basic Mathlib.Order.UpperLower.Closure Mathlib.Order.UpperLower.CompleteLattice Mathlib.Order.UpperLower.Fibration Mathlib.Order.UpperLower.Hom Mathlib.Order.UpperLower.Principal Mathlib.Order.UpperLower.Prod Mathlib.Order.ZornAtoms Mathlib.SetTheory.ZFC.Basic Mathlib.Tactic.FinCases |
-14 |
12 filesMathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations Mathlib.AlgebraicTopology.SimplexCategory.Defs Mathlib.CategoryTheory.FinCategory.AsType Mathlib.CategoryTheory.FinCategory.Basic Mathlib.CategoryTheory.MorphismProperty.Basic Mathlib.CategoryTheory.MorphismProperty.Composition Mathlib.CategoryTheory.MorphismProperty.Factorization Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy Mathlib.CategoryTheory.MorphismProperty.IsSmall Mathlib.CategoryTheory.MorphismProperty.Retract Mathlib.CategoryTheory.PathCategory.MorphismProperty Mathlib.CategoryTheory.Widesubcategory |
-13 |
Mathlib.Algebra.GCDMonoid.Nat |
-10 |
Mathlib.Data.Int.GCD |
-5 |
Mathlib.Tactic.NormNum.GCD |
-2 |
219 filesMathlib.Algebra.Algebra.Spectrum.Basic Mathlib.Algebra.Algebra.Spectrum.Pi Mathlib.Algebra.Algebra.Spectrum.Quasispectrum Mathlib.Algebra.Algebra.Subalgebra.Operations Mathlib.Algebra.CharP.Invertible Mathlib.Algebra.Group.WithOne.Basic Mathlib.Algebra.Group.WithOne.Defs Mathlib.Algebra.MvPolynomial.SchwartzZippel Mathlib.Algebra.Notation.Lemmas Mathlib.Algebra.Polynomial.Laurent Mathlib.Algebra.Polynomial.PartialFractions Mathlib.Algebra.Polynomial.Roots Mathlib.Algebra.Star.Unitary Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant Mathlib.CategoryTheory.Adjunction.Comma Mathlib.CategoryTheory.Adjunction.Evaluation Mathlib.CategoryTheory.Adjunction.FullyFaithful Mathlib.CategoryTheory.Adjunction.Limits Mathlib.CategoryTheory.Adjunction.PartialAdjoint Mathlib.CategoryTheory.Adjunction.Reflective Mathlib.CategoryTheory.Adjunction.Triple Mathlib.CategoryTheory.Bicategory.Kan.Adjunction Mathlib.CategoryTheory.Bicategory.Kan.HasKan Mathlib.CategoryTheory.Bicategory.SingleObj Mathlib.CategoryTheory.Category.Cat.Limit Mathlib.CategoryTheory.Category.Factorisation Mathlib.CategoryTheory.Category.Pairwise Mathlib.CategoryTheory.Category.Quiv Mathlib.CategoryTheory.Category.ReflQuiv Mathlib.CategoryTheory.Category.RelCat Mathlib.CategoryTheory.Closed.Monoidal Mathlib.CategoryTheory.Comma.LocallySmall Mathlib.CategoryTheory.Comma.Over.Pullback Mathlib.CategoryTheory.Comma.StructuredArrow.Small Mathlib.CategoryTheory.Countable Mathlib.CategoryTheory.EffectiveEpi.Basic Mathlib.CategoryTheory.EffectiveEpi.Comp Mathlib.CategoryTheory.EffectiveEpi.Coproduct Mathlib.CategoryTheory.EffectiveEpi.Enough Mathlib.CategoryTheory.EffectiveEpi.Preserves Mathlib.CategoryTheory.EffectiveEpi.RegularEpi Mathlib.CategoryTheory.EssentiallySmall Mathlib.CategoryTheory.Functor.Derived.RightDerived Mathlib.CategoryTheory.Functor.KanExtension.Adjunction Mathlib.CategoryTheory.Functor.KanExtension.Basic Mathlib.CategoryTheory.Functor.KanExtension.Pointwise Mathlib.CategoryTheory.Limits.Bicones Mathlib.CategoryTheory.Limits.ColimitLimit Mathlib.CategoryTheory.Limits.ConeCategory Mathlib.CategoryTheory.Limits.Connected Mathlib.CategoryTheory.Limits.Constructions.Over.Connected Mathlib.CategoryTheory.Limits.Constructions.Pullbacks Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial Mathlib.CategoryTheory.Limits.Creates Mathlib.CategoryTheory.Limits.Elements Mathlib.CategoryTheory.Limits.EssentiallySmall Mathlib.CategoryTheory.Limits.Fubini Mathlib.CategoryTheory.Limits.FullSubcategory Mathlib.CategoryTheory.Limits.FunctorCategory.Basic Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks Mathlib.CategoryTheory.Limits.FunctorToTypes Mathlib.CategoryTheory.Limits.HasLimits Mathlib.CategoryTheory.Limits.Pi Mathlib.CategoryTheory.Limits.Preorder Mathlib.CategoryTheory.Limits.Preserves.Basic Mathlib.CategoryTheory.Limits.Preserves.Grothendieck Mathlib.CategoryTheory.Limits.Preserves.Limits Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal Mathlib.CategoryTheory.Limits.Preserves.Ulift Mathlib.CategoryTheory.Limits.Preserves.Yoneda Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts Mathlib.CategoryTheory.Limits.Shapes.Connected Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct Mathlib.CategoryTheory.Limits.Shapes.End Mathlib.CategoryTheory.Limits.Shapes.Equalizers Mathlib.CategoryTheory.Limits.Shapes.Equivalence Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes Mathlib.CategoryTheory.Limits.Shapes.Grothendieck Mathlib.CategoryTheory.Limits.Shapes.Images Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer Mathlib.CategoryTheory.Limits.Shapes.PiProd Mathlib.CategoryTheory.Limits.Shapes.Preorder.Basic Mathlib.CategoryTheory.Limits.Shapes.Preorder.Fin Mathlib.CategoryTheory.Limits.Shapes.Preorder.PrincipalSeg Mathlib.CategoryTheory.Limits.Shapes.Products Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone Mathlib.CategoryTheory.Limits.Shapes.RegularMono Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer Mathlib.CategoryTheory.Limits.Shapes.StrictInitial Mathlib.CategoryTheory.Limits.Shapes.Terminal Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects Mathlib.CategoryTheory.Limits.Types.Colimits Mathlib.CategoryTheory.Limits.Types.Images Mathlib.CategoryTheory.Limits.Types.Limits Mathlib.CategoryTheory.Limits.Types.Shapes Mathlib.CategoryTheory.Limits.Types.Yoneda Mathlib.CategoryTheory.Limits.Unit Mathlib.CategoryTheory.Limits.Yoneda Mathlib.CategoryTheory.Localization.Adjunction Mathlib.CategoryTheory.Localization.Bifunctor Mathlib.CategoryTheory.Localization.Bousfield Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions Mathlib.CategoryTheory.Localization.CalculusOfFractions Mathlib.CategoryTheory.Localization.Composition Mathlib.CategoryTheory.Localization.Construction Mathlib.CategoryTheory.Localization.Equivalence Mathlib.CategoryTheory.Localization.HasLocalization Mathlib.CategoryTheory.Localization.HomEquiv Mathlib.CategoryTheory.Localization.LocalizerMorphism Mathlib.CategoryTheory.Localization.LocallySmall Mathlib.CategoryTheory.Localization.Monoidal Mathlib.CategoryTheory.Localization.Opposite Mathlib.CategoryTheory.Localization.Predicate Mathlib.CategoryTheory.Localization.Prod Mathlib.CategoryTheory.Localization.Resolution Mathlib.CategoryTheory.Localization.SmallHom Mathlib.CategoryTheory.Localization.StructuredArrow Mathlib.CategoryTheory.Localization.Trifunctor Mathlib.CategoryTheory.Monad.Adjunction Mathlib.CategoryTheory.Monad.Limits Mathlib.CategoryTheory.Monad.Products Mathlib.CategoryTheory.Monoidal.End Mathlib.CategoryTheory.Monoidal.Free.Basic Mathlib.CategoryTheory.Monoidal.Free.Coherence Mathlib.CategoryTheory.Monoidal.Functor Mathlib.CategoryTheory.Monoidal.NaturalTransformation Mathlib.CategoryTheory.Monoidal.OfChosenFiniteProducts.Basic Mathlib.CategoryTheory.Monoidal.Rigid.Basic Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence Mathlib.CategoryTheory.Monoidal.Transport Mathlib.CategoryTheory.MorphismProperty.Comma Mathlib.CategoryTheory.MorphismProperty.Concrete Mathlib.CategoryTheory.Sites.Closed Mathlib.CategoryTheory.Sites.EffectiveEpimorphic Mathlib.CategoryTheory.Sites.EqualizerSheafCondition Mathlib.CategoryTheory.Sites.Grothendieck Mathlib.CategoryTheory.Sites.IsSheafFor Mathlib.CategoryTheory.Sites.Pretopology Mathlib.CategoryTheory.Sites.SheafOfTypes Mathlib.CategoryTheory.Sites.Sieves Mathlib.CategoryTheory.SmallObject.WellOrderInductionData Mathlib.CategoryTheory.Subpresheaf.Basic Mathlib.CategoryTheory.Subpresheaf.Sieves Mathlib.CategoryTheory.WithTerminal.Basic Mathlib.Combinatorics.Nullstellensatz Mathlib.Combinatorics.Quiver.ReflQuiver Mathlib.Data.Int.Sqrt Mathlib.Data.Nat.Factorial.NatCast Mathlib.Data.Rat.Defs Mathlib.Dynamics.PeriodicPts.Lemmas Mathlib.LinearAlgebra.AffineSpace.MidpointZero Mathlib.LinearAlgebra.AffineSpace.Ordered Mathlib.Order.Category.BddDistLat Mathlib.Order.Category.BddLat Mathlib.Order.Category.BddOrd Mathlib.Order.Category.BoolAlg Mathlib.Order.Category.CompleteLat Mathlib.Order.Category.DistLat Mathlib.Order.Category.Frm Mathlib.Order.Category.HeytAlg Mathlib.Order.Category.Lat Mathlib.Order.Category.LinOrd Mathlib.Order.Category.PartOrd Mathlib.Order.Category.Preord Mathlib.Order.Category.Semilat Mathlib.RingTheory.Algebraic.Cardinality Mathlib.RingTheory.Coprime.Ideal Mathlib.RingTheory.Coprime.Lemmas Mathlib.RingTheory.DividedPowers.Basic Mathlib.RingTheory.DividedPowers.DPMorphism Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal Mathlib.RingTheory.GradedAlgebra.Radical Mathlib.RingTheory.HahnSeries.HEval Mathlib.RingTheory.HahnSeries.PowerSeries Mathlib.RingTheory.HahnSeries.Valuation Mathlib.RingTheory.Ideal.Colon Mathlib.RingTheory.Ideal.Maps Mathlib.RingTheory.Ideal.Operations Mathlib.RingTheory.Ideal.Pointwise Mathlib.RingTheory.Ideal.Prod Mathlib.RingTheory.Localization.Away.Basic Mathlib.RingTheory.MvPolynomial.EulerIdentity Mathlib.RingTheory.MvPolynomial.Groebner Mathlib.RingTheory.MvPolynomial.Homogeneous Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex Mathlib.RingTheory.MvPolynomial.MonomialOrder Mathlib.RingTheory.Polynomial.HilbertPoly Mathlib.RingTheory.Polynomial.Ideal Mathlib.RingTheory.PowerSeries.Basic Mathlib.RingTheory.PowerSeries.Order Mathlib.RingTheory.PowerSeries.Trunc Mathlib.RingTheory.PowerSeries.WellKnown Mathlib.RingTheory.UniqueFactorizationDomain.Ideal Mathlib.RingTheory.Valuation.Basic Mathlib.RingTheory.Valuation.Discrete.Basic Mathlib.RingTheory.Valuation.ExtendToLocalization Mathlib.RingTheory.Valuation.Integers Mathlib.RingTheory.Valuation.PrimeMultiplicity Mathlib.RingTheory.Valuation.RankOne Mathlib.RingTheory.Valuation.ValExtension Mathlib.Tactic.CategoryTheory.Coherence Mathlib.Tactic.NormNum.IsCoprime Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology |
-1 |
Mathlib.Control.Traversable.Basic Mathlib.Data.Option.Defs |
1 |
Declarations diff
+ CommRing.toGrindCommRing
+ CommRing.toGrindCommRing_ofNat
+ _root_.Lean.SearchPath.relativize
+ instance (X : Type u) [TopologicalSpace X] [Small.{v} X] :
+ instance (α : Type*) [CommRing α] (n : ℕ) [CharP α n] : Lean.Grind.IsCharP α n
+ instance [NormedField 𝕜] [NormedCommRing R] [NormedAlgebra 𝕜 R] :
+ merge_isAssociative
+ merge_isCommutative
+ merge_isId
+ merge_isIdempotent
++-- toAffine
+-+--+ of_surjective
- One
- add_eq_left
- add_eq_max_iff
- add_eq_min_iff
- add_eq_one_iff
- add_eq_right
- add_eq_three_iff
- add_eq_two_iff
- add_eq_zero
- add_le_iff_le_sub
- add_le_mul
- add_le_zero_iff_le_neg
- add_le_zero_iff_le_neg'
- add_left_inj
- add_mod_eq_add_mod_left
- add_mod_eq_add_mod_right
- add_mod_eq_ite
- add_nonnneg_iff_neg_le
- add_nonnneg_iff_neg_le'
- add_pos_iff_pos_or_pos
- add_right_inj
- add_sub_one_le_mul
- add_sub_sub_cancel
- add_succ_lt_add
- add_succ_sub_one
- cast_id
- decidableEqNone
- decidableExistsMem
- decidableForallMem
- default_eq_zero
- div_add_mod'
- div_div_div_eq_div
- div_div_self
- div_dvd_of_dvd
- div_eq_iff_eq_of_dvd_dvd
- div_eq_self
- div_eq_sub_mod_div
- div_eq_zero_iff
- div_le_div
- div_le_div_of_mul_le_mul
- div_le_div_right
- div_le_iff_le_mul_add_pred
- div_le_iff_le_mul_of_dvd
- div_left_inj
- div_lt_div_left
- div_lt_div_of_lt_of_dvd
- div_lt_div_right
- div_lt_one_iff
- div_mod_unique
- div_mul_div_comm
- div_mul_div_le
- div_mul_div_le_div
- div_mul_right_comm
- div_ne_zero_iff
- div_ne_zero_iff_of_dvd
- div_pos_iff
- div_pow
- drop_sum_flatten'
- drop_sum_join'
- drop_take_succ_flatten_eq_getElem'
- drop_take_succ_join_eq_getElem'
- dvd_add_left
- dvd_add_right
- dvd_div_iff_mul_dvd
- dvd_div_of_mul_dvd
- dvd_gcd
- dvd_iff_div_mul_eq
- dvd_iff_dvd_dvd
- dvd_iff_le_div_mul
- dvd_of_mul_dvd_mul_left
- dvd_of_mul_dvd_mul_right
- dvd_sub_mod
- ediv_dvd_ediv
- ediv_dvd_of_dvd
- eq_div_iff_mul_eq_left
- eq_div_of_mul_eq_left
- eq_div_of_mul_eq_right
- eq_mul_of_div_eq_left
- eq_none_iff_forall_some_ne
- eq_none_or_eq_some
- eq_of_dvd_of_div_eq_one
- eq_of_dvd_of_lt_two_mul
- eq_one_of_mul_eq_one_left
- eq_one_of_mul_eq_one_right
- eq_sub_of_add_eq
- eq_sub_of_add_eq'
- eq_zero_of_dvd_of_div_eq_zero
- eq_zero_of_dvd_of_lt
- eq_zero_of_le_div
- eq_zero_of_mul_le
- exists_ne_none
- gcd_assoc
- gcd_comm
- gcd_dvd_gcd_mul_left_right
- gcd_dvd_gcd_mul_right_right
- gcd_dvd_gcd_of_dvd_left
- gcd_dvd_gcd_of_dvd_right
- gcd_eq_left
- gcd_eq_right
- gcd_eq_zero_iff
- gcd_mul_lcm
- gcd_mul_left
- gcd_mul_right
- gcd_natCast_natCast
- gcd_pos_iff
- gcd_pos_of_ne_zero_left
- gcd_pos_of_ne_zero_right
- gcd_self
- gcd_zero_left
- gcd_zero_right
- ge_of_eq
- getLast_cons_cons
- instance (X : Type u) [TopologicalSpace X] [Small.{v} X] : TopologicalSpace (Shrink.{v} X)
- instance (priority := 200) One.ofOfNat1 {α} [OfNat α (nat_lit 1)] : One α
- instance (priority := 300) One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1)
- instance : Pow (BitVec w) ℕ := ⟨fun x n => ofFin <| x.toFin ^ n⟩
- instance [NormedField 𝕜] [NormedCommRing R] [NormedAlgebra 𝕜 R] : NormedSpace 𝕜 C(α, R)₀
- isNone_eq_false_iff
- lcm_assoc
- lcm_comm
- lcm_dvd
- lcm_dvd_iff
- lcm_dvd_mul
- lcm_one_left
- lcm_one_right
- lcm_pos
- lcm_zero_left
- lcm_zero_right
- le_add_iff_sub_le
- le_add_pred_of_pos
- le_and_le_add_one_iff
- le_antisymm_iff
- le_iff_eq_or_lt
- le_iff_lt_or_eq
- le_iff_ne_zero_of_dvd
- le_mul_self
- le_of_eq
- le_of_lt_add_of_dvd
- le_of_pred_lt
- le_one_iff_eq_zero_or_eq_one
- le_or_le_of_add_eq_add_pred
- le_or_lt
- le_rfl
- le_self_pow
- le_sub_one_iff
- le_succ_iff
- lt_asymm
- lt_div_iff_mul_lt'
- lt_div_iff_mul_lt_of_dvd
- lt_div_mul_add
- lt_iff_add_one_le
- lt_iff_le_pred
- lt_iff_lt_of_mul_eq_mul
- lt_mul_div_succ
- lt_mul_iff_one_lt_left
- lt_mul_iff_one_lt_right
- lt_mul_of_div_lt
- lt_mul_self_iff
- lt_of_div_lt_div
- lt_of_lt_pred
- lt_of_pow_dvd_right
- lt_of_toNat_lt
- lt_one_add_iff
- lt_or_le
- lt_or_lt_of_ne
- lt_pred_iff
- lt_sub_iff_add_lt
- lt_sub_iff_add_lt'
- lt_toNat
- max_eq_zero_iff
- max_left_comm
- max_right_comm
- mem_some_iff
- min_eq_zero_iff
- min_left_comm
- min_right_comm
- mod_add_div'
- mod_eq_iff_lt
- mod_succ
- mod_succ_eq_iff_lt
- mod_two_ne_one
- mod_two_ne_zero
- mod_two_not_eq_one
- mod_two_not_eq_zero
- mul_add_mod'
- mul_add_mod_of_lt
- mul_add_mul_div_of_dvd
- mul_div_cancel_left'
- mul_div_eq_iff_dvd
- mul_div_le_mul_div_assoc
- mul_div_lt_iff_not_dvd
- mul_div_mul_comm
- mul_div_right_comm
- mul_dvd_mul
- mul_dvd_mul_iff_left
- mul_dvd_mul_iff_right
- mul_dvd_mul_left
- mul_dvd_mul_right
- mul_dvd_of_dvd_div
- mul_eq_left
- mul_eq_right
- mul_le_mul_iff_of_pos_right
- mul_le_mul_left
- mul_le_mul_left_of_neg
- mul_le_mul_right
- mul_le_mul_right_of_neg
- mul_le_of_le_div
- mul_left_inj
- mul_lt_mul''
- mul_lt_mul_left
- mul_lt_mul_left_of_neg
- mul_lt_mul_pow_succ
- mul_lt_mul_right
- mul_lt_mul_right_of_neg
- mul_ne_mul_left
- mul_ne_mul_right
- mul_nonneg_iff_of_pos_right
- mul_right_inj
- mul_self_inj
- mul_self_le_mul_self
- mul_self_le_mul_self_iff
- mul_self_lt_mul_self
- mul_self_lt_mul_self_iff
- mul_sub_div_of_dvd
- mul_sub_mul_div_of_dvd
- natAbs_add_of_nonneg
- natAbs_add_of_nonpos
- natAbs_cast
- natAbs_ediv_of_dvd
- natAbs_eq_of_dvd_dvd
- natAbs_ofNat'
- natAbs_pow
- natAbs_pow_two
- natCast_ediv
- natCast_eq_zero
- natCast_inj
- natCast_ne_zero
- natCast_ne_zero_iff_pos
- natCast_nonneg
- natCast_nonpos_iff
- natCast_pos
- natCast_sub
- natCast_succ_pos
- neg_emod_two
- neg_neg_iff_pos
- neg_nonneg
- neg_pos
- not_dvd_of_pos_of_lt
- not_succ_lt_self
- ofNat_add_one_out
- ofNat_add_out
- ofNat_eq_natCast
- ofNat_mul_out
- one_add_le_iff
- one_le_div_iff
- one_le_iff_ne_zero
- one_le_of_lt
- one_le_pow
- one_lt_iff_ne_zero_and_ne_one
- one_lt_mul_iff
- one_lt_pow
- one_lt_pow'
- one_lt_pow_iff
- one_lt_succ_succ
- one_lt_two_pow'
- one_mod
- one_mod_eq_one
- one_ne_zero
- one_nonneg
- one_pos
- pbind_eq_bind
- pbind_eq_some
- pbind_map
- pow_dvd_pow_iff
- pow_eq_one
- pow_eq_self_iff
- pow_eq_zero
- pow_le_one_iff
- pow_le_pow_iff_left
- pow_lt_pow_iff_left
- pow_lt_pow_right
- pow_mod
- pow_pos_iff
- pow_right_inj
- pow_self_mul_pow_self_le
- pow_self_pos
- pow_two_sub_pow_two
- pred_add_self
- pred_eq_of_eq_succ
- pred_eq_self_iff
- pred_eq_succ_iff
- pred_le_iff
- pred_one_add
- pred_sub
- self_add_pred
- self_add_sub_one
- sign_natCast_add_one
- sign_natCast_of_ne_zero
- sub_add_sub_cancel
- sub_eq_of_eq_add'
- sub_lt_iff_lt_add
- sub_lt_iff_lt_add'
- sub_lt_sub_iff_right
- sub_mod_eq_zero_of_mod_eq
- sub_nonneg
- sub_one_add_self
- sub_one_lt_iff
- sub_pos
- sub_sub_sub_cancel_right
- sub_succ'
- succ_add_sub_one
- succ_inj
- succ_le_iff
- succ_mul_pos
- succ_ne_succ
- succ_succ_ne_one
- take_sum_flatten'
- take_sum_join'
- toNat_natCast
- toNat_natCast_add_one
- toNat_sub_of_le
- two_mul
- two_pow_succ
- zero_eq_mul
-+- div_dvd_iff_dvd_mul
-+-+ iic
-+-+-+-+ colimitCoconeIsColimit
-- lcm_mul_left
-- lcm_mul_right
-- le_add_one_iff
--+ dvd_mul_of_div_dvd
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 script/declarations_diff.sh contains some details about this script.
Decrease in tech debt: (relative, absolute) = (0.83, 0.02)
| Current number | Change | Type |
|---|---|---|
| 125 | 3 | adaptation notes |
| 71 | -3 | disabled deprecation lints |
Current commit a86c12eb12
Reference commit 446b459fb1
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
|
Here are the benchmark results for commit 502149c. |
|
!bench |
|
Here are the benchmark results for commit 33a8018.Found no runs to compare against. |
|
!bench |
|
Here are the benchmark results for commit a86c12e.Found no runs to compare against. |
* Trigger CI for leanprover/lean4#7971 * WIP * WIP * WIP * Trigger CI for leanprover/lean4#7971 * Update lean-toolchain for testing leanprover/lean4#7975 * Fix * Trigger CI for leanprover/lean4#7971 * remove adaptation notes * Fix * Fix * chore: bump to nightly-2025-04-16 * revert some stuff * Update lean-toolchain for testing leanprover/lean4#7983 * WIP * Part one * Part two * lake update and fix * Fix * Trigger CI for leanprover/lean4#7983 * Shake * chore: bump to nightly-2025-04-17 * lake update * . * chore: bump to nightly-2025-04-18 * Update lean-toolchain for testing leanprover/lean4#8021 * fix * fix: !bench after Lake path changes (#24143) * fix * fix * chore: bump to nightly-2025-04-19 * Merge master into nightly-testing * temporarirly disable sythorder checking for Grind.IsCharP instance * shake * chore: bump to nightly-2025-04-20 * fix * chore: bump to nightly-2025-04-21 * make fix more robust * fix test * chore: bump to nightly-2025-04-22 * . * sorries * sorries * chore: bump to nightly-2025-04-23 * chore: bump to nightly-2025-04-24 * fix * not there yet * comment out * comment out * chore: bump to nightly-2025-04-25 * bump batteries * more * hacky fix? * add comment * fix lint-style * Fix shake: Parser.parseHeader returns TSyntax instead of Syntax after the new module system * Clean up * Update lean-toolchain for testing leanprover/lean4#8000 * Lake update * Fix * Fix * Fix * Fix * fix to Mathlib/Algebra/Homology/Embedding/Connect.lean * Fix * chore: bump to nightly-2025-04-26 * fix MinImports * Update lean-toolchain for testing leanprover/lean4#8114 * lake update * fix * fixes * fix * fix deprecations * remove accidental files * chore: bump to nightly-2025-04-26 * chore: bump to nightly-2025-04-27 * fixes * cleanup adaptation note * shake --fix * cleanup * . * cleanup * cleanup * cleanup * comments * cleanuo * move batteries back to nightly-testing * fix * fix build hopefully? * fix build hopefully? * chore: bump to nightly-2025-04-28 * Update lean-toolchain for testing leanprover/lean4#8144 * lake update * Fix * fix grind instances * shake * Cleanup * shake * chore: bump to nightly-2025-04-29 * fix * deprecation * Update lean-toolchain for testing leanprover/lean4#8161 * shake * fix GrindInstances * basic test for grind +ring * fixes for leanprover/lean4#8161 * fixes * chore: adaptations for nightly-2025-04-29 * Merge master into nightly-testing * chore: bump to nightly-2025-04-30 * lake update * fix * fix merge * fix merge * Drop a few unnecessary changes * fix test * chore: bump to nightly-2025-05-01 * fix --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Markus Himmel <markus@lean-fro.org> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net>
* chore: bump to nightly-2025-04-16 * revert some stuff * Update lean-toolchain for testing leanprover/lean4#7983 * WIP * Part one * Part two * lake update and fix * Fix * Trigger CI for leanprover/lean4#7983 * Shake * chore: bump to nightly-2025-04-17 * lake update * . * chore: bump to nightly-2025-04-18 * Update lean-toolchain for testing leanprover/lean4#8021 * fix * fix: !bench after Lake path changes (#24143) * fix * fix * chore: bump to nightly-2025-04-19 * Merge master into nightly-testing * temporarirly disable sythorder checking for Grind.IsCharP instance * shake * chore: bump to nightly-2025-04-20 * fix * chore: bump to nightly-2025-04-21 * make fix more robust * fix test * chore: bump to nightly-2025-04-22 * . * sorries * sorries * chore: bump to nightly-2025-04-23 * chore: bump to nightly-2025-04-24 * fix * not there yet * comment out * comment out * chore: bump to nightly-2025-04-25 * bump batteries * more * hacky fix? * add comment * fix lint-style * Fix shake: Parser.parseHeader returns TSyntax instead of Syntax after the new module system * Clean up * Update lean-toolchain for testing leanprover/lean4#8000 * Lake update * Fix * Fix * Fix * Fix * fix to Mathlib/Algebra/Homology/Embedding/Connect.lean * Fix * chore: bump to nightly-2025-04-26 * fix MinImports * Update lean-toolchain for testing leanprover/lean4#8114 * lake update * fix * fixes * fix * fix deprecations * remove accidental files * chore: bump to nightly-2025-04-26 * chore: bump to nightly-2025-04-27 * fixes * cleanup adaptation note * shake --fix * cleanup * . * cleanup * cleanup * cleanup * comments * cleanuo * move batteries back to nightly-testing * fix * fix build hopefully? * fix build hopefully? * chore: bump to nightly-2025-04-28 * Update lean-toolchain for testing leanprover/lean4#8144 * lake update * Fix * fix grind instances * shake * Cleanup * shake * chore: bump to nightly-2025-04-29 * fix * deprecation * Update lean-toolchain for testing leanprover/lean4#8161 * shake * fix GrindInstances * basic test for grind +ring * fixes for leanprover/lean4#8161 * fixes * chore: adaptations for nightly-2025-04-29 * Merge master into nightly-testing * chore: bump to nightly-2025-04-30 * lake update * fix * fix merge * fix merge * Drop a few unnecessary changes * fix test * chore: bump to nightly-2025-05-01 * fix * Merge master into nightly-testing * chore: bump to nightly-2025-05-02 * chore: bump to nightly-2025-05-03 * chore: adaptations for nightly-2025-05-03 --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Markus Himmel <markus@lean-fro.org> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
No description provided.