chore: adaptations for nightly-2025-06-18#26077
Merged
jcommelin merged 8775 commits intobump/v4.22.0from Jun 19, 2025
Merged
Conversation
This reverts commit 34f1f7f.
Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net>
PR summary bb38781a57Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Tactic.Linter.Style | 7 | 8 | +1 (+14.29%) |
| Mathlib.Init | 29 | 30 | +1 (+3.45%) |
| Mathlib.Tactic.CongrExclamation | 90 | 91 | +1 (+1.11%) |
| Mathlib.Algebra.Group.Hom.Basic | 128 | 129 | +1 (+0.78%) |
| Mathlib.Data.Erased | 134 | 135 | +1 (+0.75%) |
| Mathlib.Algebra.Ring.GrindInstances | 141 | 142 | +1 (+0.71%) |
| Mathlib.Order.Monotone.Basic | 179 | 180 | +1 (+0.56%) |
| Mathlib.Algebra.GroupWithZero.Action.Defs | 195 | 196 | +1 (+0.51%) |
| Mathlib.Algebra.Group.Action.Basic | 221 | 222 | +1 (+0.45%) |
| Mathlib.Data.Setoid.Basic | 259 | 260 | +1 (+0.39%) |
| Mathlib.Order.ConditionallyCompleteLattice.Basic | 273 | 274 | +1 (+0.37%) |
| Mathlib.Data.PFun | 288 | 289 | +1 (+0.35%) |
| Mathlib.Data.Nat.Pairing | 291 | 292 | +1 (+0.34%) |
| Mathlib.GroupTheory.Submonoid.Center | 338 | 339 | +1 (+0.30%) |
Import changes for all files
| Files | Import difference |
|---|---|
868 filesMathlib.Algebra.AddTorsor.Defs Mathlib.Algebra.BigOperators.Group.List.Defs Mathlib.Algebra.CharZero.Defs Mathlib.Algebra.EuclideanDomain.Defs Mathlib.Algebra.EuclideanDomain.Field Mathlib.Algebra.EuclideanDomain.Int Mathlib.Algebra.Expr Mathlib.Algebra.Field.Basic Mathlib.Algebra.Field.Defs Mathlib.Algebra.Field.MinimalAxioms Mathlib.Algebra.Field.ULift Mathlib.Algebra.Free Mathlib.Algebra.Group.Action.Basic Mathlib.Algebra.Group.Action.Defs Mathlib.Algebra.Group.Action.Faithful Mathlib.Algebra.Group.Action.Hom Mathlib.Algebra.Group.Action.Opposite Mathlib.Algebra.Group.Action.Option Mathlib.Algebra.Group.Action.Pi Mathlib.Algebra.Group.Action.Pointwise.Set.Basic Mathlib.Algebra.Group.Action.Pretransitive Mathlib.Algebra.Group.Action.Prod Mathlib.Algebra.Group.Action.Sigma Mathlib.Algebra.Group.Action.Sum Mathlib.Algebra.Group.Action.TypeTags Mathlib.Algebra.Group.Action.Units Mathlib.Algebra.Group.Basic Mathlib.Algebra.Group.Center Mathlib.Algebra.Group.Commutator Mathlib.Algebra.Group.Commute.Basic Mathlib.Algebra.Group.Commute.Defs Mathlib.Algebra.Group.Commute.Hom Mathlib.Algebra.Group.Commute.Units Mathlib.Algebra.Group.Defs Mathlib.Algebra.Group.Embedding Mathlib.Algebra.Group.Equiv.Basic Mathlib.Algebra.Group.Equiv.Defs Mathlib.Algebra.Group.Equiv.Opposite Mathlib.Algebra.Group.Equiv.TypeTags Mathlib.Algebra.Group.Even Mathlib.Algebra.Group.Ext Mathlib.Algebra.Group.Hom.Basic Mathlib.Algebra.Group.Hom.CompTypeclasses Mathlib.Algebra.Group.Hom.Defs Mathlib.Algebra.Group.Hom.End Mathlib.Algebra.Group.Hom.Instances Mathlib.Algebra.Group.Idempotent Mathlib.Algebra.Group.Indicator Mathlib.Algebra.Group.InjSurj Mathlib.Algebra.Group.Int.Defs Mathlib.Algebra.Group.Int.TypeTags Mathlib.Algebra.Group.Int.Units Mathlib.Algebra.Group.Invertible.Basic Mathlib.Algebra.Group.Invertible.Defs Mathlib.Algebra.Group.Irreducible.Defs Mathlib.Algebra.Group.Irreducible.Lemmas Mathlib.Algebra.Group.MinimalAxioms Mathlib.Algebra.Group.Nat.Defs Mathlib.Algebra.Group.Nat.Even Mathlib.Algebra.Group.Nat.Hom Mathlib.Algebra.Group.Nat.TypeTags Mathlib.Algebra.Group.Nat.Units Mathlib.Algebra.Group.Opposite Mathlib.Algebra.Group.PUnit Mathlib.Algebra.Group.Pi.Basic Mathlib.Algebra.Group.Pi.Lemmas Mathlib.Algebra.Group.Pi.Units Mathlib.Algebra.Group.Pointwise.Set.Basic Mathlib.Algebra.Group.Pointwise.Set.Lattice Mathlib.Algebra.Group.Pointwise.Set.Scalar Mathlib.Algebra.Group.Prod Mathlib.Algebra.Group.Semiconj.Basic Mathlib.Algebra.Group.Semiconj.Defs Mathlib.Algebra.Group.Semiconj.Units Mathlib.Algebra.Group.Submonoid.Basic Mathlib.Algebra.Group.Submonoid.Defs Mathlib.Algebra.Group.Submonoid.DistribMulAction Mathlib.Algebra.Group.Submonoid.MulAction Mathlib.Algebra.Group.Submonoid.MulOpposite Mathlib.Algebra.Group.Submonoid.Operations Mathlib.Algebra.Group.Subsemigroup.Basic Mathlib.Algebra.Group.Subsemigroup.Defs Mathlib.Algebra.Group.Subsemigroup.Membership Mathlib.Algebra.Group.Subsemigroup.Operations Mathlib.Algebra.Group.Support Mathlib.Algebra.Group.Torsion Mathlib.Algebra.Group.TypeTags.Basic Mathlib.Algebra.Group.TypeTags.Hom Mathlib.Algebra.Group.ULift Mathlib.Algebra.Group.Units.Basic Mathlib.Algebra.Group.Units.Defs Mathlib.Algebra.Group.Units.Equiv Mathlib.Algebra.Group.Units.Hom Mathlib.Algebra.Group.Units.Opposite Mathlib.Algebra.GroupWithZero.Action.Defs Mathlib.Algebra.GroupWithZero.Action.End Mathlib.Algebra.GroupWithZero.Action.Faithful Mathlib.Algebra.GroupWithZero.Action.Opposite Mathlib.Algebra.GroupWithZero.Action.Prod Mathlib.Algebra.GroupWithZero.Action.Units Mathlib.Algebra.GroupWithZero.Basic Mathlib.Algebra.GroupWithZero.Center Mathlib.Algebra.GroupWithZero.Commute Mathlib.Algebra.GroupWithZero.Defs Mathlib.Algebra.GroupWithZero.Equiv Mathlib.Algebra.GroupWithZero.Hom Mathlib.Algebra.GroupWithZero.Idempotent Mathlib.Algebra.GroupWithZero.Indicator Mathlib.Algebra.GroupWithZero.InjSurj Mathlib.Algebra.GroupWithZero.Invertible Mathlib.Algebra.GroupWithZero.Nat Mathlib.Algebra.GroupWithZero.NeZero Mathlib.Algebra.GroupWithZero.Opposite Mathlib.Algebra.GroupWithZero.Pi Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic Mathlib.Algebra.GroupWithZero.Semiconj Mathlib.Algebra.GroupWithZero.ULift Mathlib.Algebra.GroupWithZero.Units.Basic Mathlib.Algebra.GroupWithZero.Units.Equiv Mathlib.Algebra.GroupWithZero.Units.Lemmas Mathlib.Algebra.HierarchyDesign Mathlib.Algebra.Homology.ComplexShape Mathlib.Algebra.Homology.Embedding.Basic Mathlib.Algebra.Homology.HasNoLoop Mathlib.Algebra.Module.Defs Mathlib.Algebra.Module.MinimalAxioms Mathlib.Algebra.Module.Opposite Mathlib.Algebra.Module.PUnit Mathlib.Algebra.Module.PointwisePi Mathlib.Algebra.Module.Prod Mathlib.Algebra.Module.RingHom Mathlib.Algebra.NeZero Mathlib.Algebra.NoZeroSMulDivisors.Defs Mathlib.Algebra.NoZeroSMulDivisors.Pi Mathlib.Algebra.NoZeroSMulDivisors.Prod Mathlib.Algebra.Notation.Defs Mathlib.Algebra.Notation.Lemmas Mathlib.Algebra.Notation.Pi Mathlib.Algebra.Notation.Prod Mathlib.Algebra.Notation Mathlib.Algebra.Opposites Mathlib.Algebra.Order.AddGroupWithTop Mathlib.Algebra.Order.AddTorsor Mathlib.Algebra.Order.BigOperators.GroupWithZero.List Mathlib.Algebra.Order.Field.Defs Mathlib.Algebra.Order.Field.InjSurj Mathlib.Algebra.Order.Field.Pointwise Mathlib.Algebra.Order.Group.Abs Mathlib.Algebra.Order.Group.Action.End Mathlib.Algebra.Order.Group.Action.Flag Mathlib.Algebra.Order.Group.Action.Synonym Mathlib.Algebra.Order.Group.Action Mathlib.Algebra.Order.Group.Basic Mathlib.Algebra.Order.Group.Bounds Mathlib.Algebra.Order.Group.CompleteLattice Mathlib.Algebra.Order.Group.Cone Mathlib.Algebra.Order.Group.Defs Mathlib.Algebra.Order.Group.DenselyOrdered Mathlib.Algebra.Order.Group.End Mathlib.Algebra.Order.Group.Indicator Mathlib.Algebra.Order.Group.InjSurj Mathlib.Algebra.Order.Group.Instances Mathlib.Algebra.Order.Group.Int Mathlib.Algebra.Order.Group.Lattice Mathlib.Algebra.Order.Group.MinMax Mathlib.Algebra.Order.Group.Nat Mathlib.Algebra.Order.Group.Opposite Mathlib.Algebra.Order.Group.OrderIso Mathlib.Algebra.Order.Group.Pointwise.Bounds Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice Mathlib.Algebra.Order.Group.PosPart Mathlib.Algebra.Order.Group.Prod Mathlib.Algebra.Order.Group.Synonym Mathlib.Algebra.Order.Group.TypeTags Mathlib.Algebra.Order.Group.Unbundled.Abs Mathlib.Algebra.Order.Group.Unbundled.Basic Mathlib.Algebra.Order.Group.Unbundled.Int Mathlib.Algebra.Order.Group.Units Mathlib.Algebra.Order.GroupWithZero.Bounds Mathlib.Algebra.Order.GroupWithZero.Submonoid Mathlib.Algebra.Order.GroupWithZero.Synonym Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs Mathlib.Algebra.Order.GroupWithZero.Unbundled.Lemmas Mathlib.Algebra.Order.GroupWithZero.Unbundled.OrderIso Mathlib.Algebra.Order.GroupWithZero.Unbundled Mathlib.Algebra.Order.Interval.Set.Group Mathlib.Algebra.Order.Interval.Set.Instances Mathlib.Algebra.Order.Interval.Set.Monoid Mathlib.Algebra.Order.Monoid.Basic Mathlib.Algebra.Order.Monoid.Canonical.Defs Mathlib.Algebra.Order.Monoid.Defs Mathlib.Algebra.Order.Monoid.NatCast Mathlib.Algebra.Order.Monoid.OrderDual Mathlib.Algebra.Order.Monoid.Prod Mathlib.Algebra.Order.Monoid.Submonoid Mathlib.Algebra.Order.Monoid.TypeTags Mathlib.Algebra.Order.Monoid.Unbundled.Basic Mathlib.Algebra.Order.Monoid.Unbundled.Defs Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE Mathlib.Algebra.Order.Monoid.Unbundled.MinMax Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual Mathlib.Algebra.Order.Monoid.Unbundled.Pow Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags Mathlib.Algebra.Order.Monoid.Unbundled.WithTop Mathlib.Algebra.Order.Monoid.Units Mathlib.Algebra.Order.Monoid.WithTop Mathlib.Algebra.Order.PUnit Mathlib.Algebra.Order.Pi Mathlib.Algebra.Order.Positive.Field Mathlib.Algebra.Order.Positive.Ring Mathlib.Algebra.Order.Quantale Mathlib.Algebra.Order.Ring.Cone Mathlib.Algebra.Order.Ring.Defs Mathlib.Algebra.Order.Ring.Idempotent Mathlib.Algebra.Order.Ring.InjSurj Mathlib.Algebra.Order.Ring.Opposite Mathlib.Algebra.Order.Ring.Synonym Mathlib.Algebra.Order.Ring.Unbundled.Basic Mathlib.Algebra.Order.Sub.Basic Mathlib.Algebra.Order.Sub.Defs Mathlib.Algebra.Order.Sub.Prod Mathlib.Algebra.Order.Sub.Unbundled.Basic Mathlib.Algebra.Order.Sub.Unbundled.Hom Mathlib.Algebra.Order.Sub.WithTop Mathlib.Algebra.Order.Sum Mathlib.Algebra.Order.ZeroLEOne Mathlib.Algebra.PEmptyInstances Mathlib.Algebra.Regular.Basic Mathlib.Algebra.Regular.Opposite Mathlib.Algebra.Regular.Pi Mathlib.Algebra.Regular.Prod Mathlib.Algebra.Regular.SMul Mathlib.Algebra.Regular.ULift Mathlib.Algebra.Ring.Action.Basic Mathlib.Algebra.Ring.Action.Field Mathlib.Algebra.Ring.Action.Pointwise.Set Mathlib.Algebra.Ring.Action.Rat Mathlib.Algebra.Ring.Basic Mathlib.Algebra.Ring.Centralizer Mathlib.Algebra.Ring.Commute Mathlib.Algebra.Ring.CompTypeclasses Mathlib.Algebra.Ring.Defs Mathlib.Algebra.Ring.Equiv Mathlib.Algebra.Ring.Ext Mathlib.Algebra.Ring.GrindInstances Mathlib.Algebra.Ring.Hom.Basic Mathlib.Algebra.Ring.Hom.Defs Mathlib.Algebra.Ring.Hom.InjSurj Mathlib.Algebra.Ring.Idempotent Mathlib.Algebra.Ring.InjSurj Mathlib.Algebra.Ring.Int.Defs Mathlib.Algebra.Ring.Int.Units Mathlib.Algebra.Ring.Invertible Mathlib.Algebra.Ring.MinimalAxioms Mathlib.Algebra.Ring.Nat Mathlib.Algebra.Ring.Opposite Mathlib.Algebra.Ring.PUnit Mathlib.Algebra.Ring.Pi Mathlib.Algebra.Ring.Pointwise.Set Mathlib.Algebra.Ring.Regular Mathlib.Algebra.Ring.Semiconj Mathlib.Algebra.Ring.Submonoid.Basic Mathlib.Algebra.Ring.Submonoid Mathlib.Algebra.Ring.Subsemiring.Defs Mathlib.Algebra.Ring.Subsemiring.Order Mathlib.Algebra.Ring.ULift Mathlib.Algebra.Ring.Units Mathlib.Algebra.Tropical.Basic Mathlib.Algebra.Tropical.Lattice Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Note Mathlib.CategoryTheory.Category.Init Mathlib.CategoryTheory.ConcreteCategory.Bundled Mathlib.Combinatorics.Quiver.Arborescence Mathlib.Combinatorics.Quiver.Basic Mathlib.Combinatorics.Quiver.Cast Mathlib.Combinatorics.Quiver.ConnectedComponent Mathlib.Combinatorics.Quiver.Path Mathlib.Combinatorics.Quiver.Prefunctor Mathlib.Combinatorics.Quiver.Push Mathlib.Combinatorics.Quiver.SingleObj Mathlib.Combinatorics.Quiver.Subquiver Mathlib.Combinatorics.Quiver.Symmetric Mathlib.Combinatorics.SimpleGraph.Init Mathlib.Control.Applicative Mathlib.Control.Basic Mathlib.Control.Combinators Mathlib.Control.EquivFunctor Mathlib.Control.Functor Mathlib.Control.Lawful Mathlib.Control.Monad.Basic Mathlib.Control.Monad.Cont Mathlib.Control.Monad.Writer Mathlib.Control.Traversable.Basic Mathlib.Control.Traversable.Equiv Mathlib.Control.Traversable.Lemmas Mathlib.Control.ULift Mathlib.Data.Array.Defs Mathlib.Data.Array.Extract Mathlib.Data.Bool.AllAny Mathlib.Data.Bool.Basic Mathlib.Data.Bool.Set Mathlib.Data.Bracket Mathlib.Data.Bundle Mathlib.Data.Char Mathlib.Data.Countable.Defs Mathlib.Data.Countable.Small Mathlib.Data.ENat.Defs Mathlib.Data.Erased Mathlib.Data.FP.Basic Mathlib.Data.Finite.Defs Mathlib.Data.Finset.Attr Mathlib.Data.FunLike.Basic Mathlib.Data.FunLike.Embedding Mathlib.Data.FunLike.Equiv Mathlib.Data.Ineq Mathlib.Data.Int.Basic Mathlib.Data.Int.Cast.Basic Mathlib.Data.Int.Cast.Defs Mathlib.Data.Int.Cast.Field Mathlib.Data.Int.Cast.Pi Mathlib.Data.Int.Cast.Prod Mathlib.Data.Int.ConditionallyCompleteOrder Mathlib.Data.Int.DivMod Mathlib.Data.Int.Init Mathlib.Data.Int.LeastGreatest Mathlib.Data.Int.Notation Mathlib.Data.Int.Order.Basic Mathlib.Data.List.Defs Mathlib.Data.List.EditDistance.Defs Mathlib.Data.List.Flatten Mathlib.Data.List.GetD Mathlib.Data.List.Iterate Mathlib.Data.List.Lookmap Mathlib.Data.List.ModifyLast Mathlib.Data.List.Monad Mathlib.Data.List.Pairwise Mathlib.Data.List.Scan Mathlib.Data.List.SplitLengths Mathlib.Data.List.TFAE Mathlib.Data.List.TakeWhile Mathlib.Data.List.Triplewise Mathlib.Data.Matrix.DMatrix Mathlib.Data.Matroid.Init Mathlib.Data.Nat.Basic Mathlib.Data.Nat.BinaryRec Mathlib.Data.Nat.Bits Mathlib.Data.Nat.Cast.Commute Mathlib.Data.Nat.Cast.Defs Mathlib.Data.Nat.Cast.NeZero Mathlib.Data.Nat.Cast.Prod Mathlib.Data.Nat.Cast.Synonym Mathlib.Data.Nat.Cast.WithTop Mathlib.Data.Nat.Find Mathlib.Data.Nat.Init Mathlib.Data.Nat.Log Mathlib.Data.Nat.Notation Mathlib.Data.Nat.Order.Lemmas Mathlib.Data.Nat.PSub Mathlib.Data.Nat.Pairing Mathlib.Data.Nat.Set Mathlib.Data.Nat.Size Mathlib.Data.Nat.Sqrt Mathlib.Data.Nat.Upto Mathlib.Data.Num.Basic Mathlib.Data.Opposite Mathlib.Data.Option.Basic Mathlib.Data.Option.Defs Mathlib.Data.Option.NAry Mathlib.Data.Ordering.Basic Mathlib.Data.Ordering.Lemmas Mathlib.Data.Ordmap.Ordnode Mathlib.Data.PEquiv Mathlib.Data.PFun Mathlib.Data.PNat.Defs Mathlib.Data.PNat.Equiv Mathlib.Data.PNat.Notation Mathlib.Data.PSigma.Order Mathlib.Data.Part Mathlib.Data.Prod.Basic Mathlib.Data.Prod.Lex Mathlib.Data.Prod.PProd Mathlib.Data.Quot Mathlib.Data.Rat.Init Mathlib.Data.Rel Mathlib.Data.SProd Mathlib.Data.Semiquot Mathlib.Data.Set.Accumulate Mathlib.Data.Set.Basic Mathlib.Data.Set.BoolIndicator Mathlib.Data.Set.BooleanAlgebra Mathlib.Data.Set.CoeSort Mathlib.Data.Set.Defs Mathlib.Data.Set.Disjoint Mathlib.Data.Set.Function Mathlib.Data.Set.Functor Mathlib.Data.Set.Image Mathlib.Data.Set.Inclusion Mathlib.Data.Set.Insert Mathlib.Data.Set.Lattice.Image Mathlib.Data.Set.Lattice Mathlib.Data.Set.List Mathlib.Data.Set.Monotone Mathlib.Data.Set.NAry Mathlib.Data.Set.Notation Mathlib.Data.Set.Operations Mathlib.Data.Set.Opposite Mathlib.Data.Set.Order 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.Subsingleton Mathlib.Data.Set.SymmDiff Mathlib.Data.Set.UnionLift Mathlib.Data.SetLike.Basic Mathlib.Data.Setoid.Basic Mathlib.Data.Sigma.Basic Mathlib.Data.Sigma.Lex Mathlib.Data.Sigma.Order Mathlib.Data.Stream.Defs Mathlib.Data.String.Defs Mathlib.Data.String.Lemmas Mathlib.Data.Subtype Mathlib.Data.Sum.Basic Mathlib.Data.Sum.Lattice Mathlib.Data.Sum.Order Mathlib.Data.Sym.Sym2.Init Mathlib.Data.Tree.Basic Mathlib.Data.Tree.Get Mathlib.Data.Tree.RBMap Mathlib.Data.Tree.Traversable Mathlib.Data.TwoPointing Mathlib.Data.UInt Mathlib.Data.ULift Mathlib.Deprecated.Aliases Mathlib.Deprecated.Order Mathlib.GroupTheory.Congruence.Basic Mathlib.GroupTheory.Congruence.Defs Mathlib.GroupTheory.Congruence.Hom Mathlib.GroupTheory.Congruence.Opposite Mathlib.GroupTheory.EckmannHilton Mathlib.GroupTheory.GroupAction.DomAct.ActionHom Mathlib.GroupTheory.GroupAction.DomAct.Basic Mathlib.GroupTheory.GroupAction.Embedding Mathlib.GroupTheory.GroupAction.Hom Mathlib.GroupTheory.GroupAction.IterateAct Mathlib.GroupTheory.GroupAction.Pointwise Mathlib.GroupTheory.GroupAction.Ring Mathlib.GroupTheory.GroupAction.Support Mathlib.GroupTheory.OreLocalization.OreSet Mathlib.GroupTheory.Submonoid.Center Mathlib.GroupTheory.Submonoid.Centralizer Mathlib.GroupTheory.Subsemigroup.Center Mathlib.GroupTheory.Subsemigroup.Centralizer Mathlib.Init Mathlib.Lean.CoreM Mathlib.Lean.Elab.Tactic.Basic Mathlib.Lean.Elab.Term Mathlib.Lean.EnvExtension Mathlib.Lean.Exception Mathlib.Lean.Expr.Basic Mathlib.Lean.Expr.ExtraRecognizers Mathlib.Lean.Expr.Rat Mathlib.Lean.Expr.ReplaceRec Mathlib.Lean.Expr Mathlib.Lean.GoalsLocation Mathlib.Lean.Json Mathlib.Lean.LocalContext Mathlib.Lean.Message Mathlib.Lean.Meta.Basic Mathlib.Lean.Meta.CongrTheorems Mathlib.Lean.Meta.DiscrTree Mathlib.Lean.Meta.KAbstractPositions Mathlib.Lean.Meta.RefinedDiscrTree.Basic Mathlib.Lean.Meta.RefinedDiscrTree.Encode Mathlib.Lean.Meta.RefinedDiscrTree.Initialize Mathlib.Lean.Meta.RefinedDiscrTree.Lookup Mathlib.Lean.Meta.RefinedDiscrTree Mathlib.Lean.Meta.Simp Mathlib.Lean.Meta Mathlib.Lean.Name Mathlib.Lean.PrettyPrinter.Delaborator Mathlib.Lean.Thunk Mathlib.LinearAlgebra.AffineSpace.Defs Mathlib.Logic.Basic Mathlib.Logic.Embedding.Basic Mathlib.Logic.Embedding.Set Mathlib.Logic.Equiv.Basic Mathlib.Logic.Equiv.Defs Mathlib.Logic.Equiv.Embedding Mathlib.Logic.Equiv.Nat Mathlib.Logic.Equiv.Option Mathlib.Logic.Equiv.Pairwise Mathlib.Logic.Equiv.PartialEquiv Mathlib.Logic.Equiv.Prod Mathlib.Logic.Equiv.Set Mathlib.Logic.Equiv.Sum Mathlib.Logic.ExistsUnique Mathlib.Logic.Function.Basic Mathlib.Logic.Function.Coequalizer Mathlib.Logic.Function.CompTypeclasses Mathlib.Logic.Function.Conjugate Mathlib.Logic.Function.Defs Mathlib.Logic.Function.DependsOn Mathlib.Logic.Function.FiberPartition Mathlib.Logic.Function.Iterate Mathlib.Logic.Function.ULift Mathlib.Logic.IsEmpty Mathlib.Logic.Lemmas Mathlib.Logic.Nonempty Mathlib.Logic.Nontrivial.Basic Mathlib.Logic.Nontrivial.Defs Mathlib.Logic.OpClass Mathlib.Logic.Pairwise Mathlib.Logic.Relation Mathlib.Logic.Relator Mathlib.Logic.Small.Basic Mathlib.Logic.Small.Defs Mathlib.Logic.Small.Set Mathlib.Logic.Unique Mathlib.Logic.UnivLE Mathlib.Order.Antichain Mathlib.Order.Antisymmetrization Mathlib.Order.Basic Mathlib.Order.BooleanAlgebra Mathlib.Order.Booleanisation Mathlib.Order.BoundedOrder.Basic Mathlib.Order.BoundedOrder.Lattice Mathlib.Order.BoundedOrder.Monotone Mathlib.Order.Bounded Mathlib.Order.Bounds.Basic Mathlib.Order.Bounds.Defs Mathlib.Order.Bounds.Image Mathlib.Order.Bounds.Lattice Mathlib.Order.Bounds.OrderIso Mathlib.Order.Chain Mathlib.Order.Circular Mathlib.Order.Closure Mathlib.Order.Cofinal Mathlib.Order.Comparable Mathlib.Order.Compare Mathlib.Order.CompleteBooleanAlgebra Mathlib.Order.CompleteLattice.Basic Mathlib.Order.CompleteLattice.Chain Mathlib.Order.CompleteLattice.Defs Mathlib.Order.CompleteLattice.Group Mathlib.Order.CompleteLattice.Lemmas Mathlib.Order.Concept Mathlib.Order.ConditionallyCompleteLattice.Basic Mathlib.Order.ConditionallyCompleteLattice.Defs Mathlib.Order.ConditionallyCompleteLattice.Group Mathlib.Order.ConditionallyCompleteLattice.Indexed Mathlib.Order.Copy Mathlib.Order.Defs.LinearOrder Mathlib.Order.Defs.PartialOrder Mathlib.Order.Defs.Unbundled Mathlib.Order.Directed Mathlib.Order.Disjoint Mathlib.Order.Estimator Mathlib.Order.Extension.Linear Mathlib.Order.Filter.AtTopBot.Basic Mathlib.Order.Filter.AtTopBot.CompleteLattice Mathlib.Order.Filter.AtTopBot.Defs Mathlib.Order.Filter.AtTopBot.Disjoint Mathlib.Order.Filter.AtTopBot.Field Mathlib.Order.Filter.AtTopBot.Group Mathlib.Order.Filter.AtTopBot.Map Mathlib.Order.Filter.AtTopBot.Monoid Mathlib.Order.Filter.AtTopBot.Ring Mathlib.Order.Filter.AtTopBot.Tendsto Mathlib.Order.Filter.Bases.Basic Mathlib.Order.Filter.Basic Mathlib.Order.Filter.Curry Mathlib.Order.Filter.Defs Mathlib.Order.Filter.Ker Mathlib.Order.Filter.Map Mathlib.Order.Filter.NAry Mathlib.Order.Filter.Partial Mathlib.Order.Filter.Prod Mathlib.Order.Filter.Tendsto Mathlib.Order.GaloisConnection.Basic Mathlib.Order.GaloisConnection.Defs Mathlib.Order.Heyting.Basic Mathlib.Order.Heyting.Hom Mathlib.Order.Heyting.Regular Mathlib.Order.Hom.Basic Mathlib.Order.Hom.BoundedLattice Mathlib.Order.Hom.Bounded Mathlib.Order.Hom.CompleteLattice Mathlib.Order.Hom.Lattice Mathlib.Order.Hom.Order Mathlib.Order.Hom.Set Mathlib.Order.Hom.WithTopBot Mathlib.Order.Interval.Basic Mathlib.Order.Interval.Set.Basic Mathlib.Order.Interval.Set.Defs Mathlib.Order.Interval.Set.Disjoint Mathlib.Order.Interval.Set.Image Mathlib.Order.Interval.Set.LinearOrder Mathlib.Order.Interval.Set.OrderIso Mathlib.Order.Interval.Set.SurjOn Mathlib.Order.Interval.Set.WithBotTop Mathlib.Order.Iterate Mathlib.Order.LatticeIntervals Mathlib.Order.Lattice Mathlib.Order.Max Mathlib.Order.MinMax Mathlib.Order.Minimal Mathlib.Order.Monotone.Basic Mathlib.Order.Monotone.Defs Mathlib.Order.Monotone.Extension Mathlib.Order.Monotone.Monovary Mathlib.Order.Monotone.Odd Mathlib.Order.Monotone.Union Mathlib.Order.Nat Mathlib.Order.Notation Mathlib.Order.Nucleus Mathlib.Order.OrdContinuous Mathlib.Order.Preorder.Chain Mathlib.Order.Prod.Lex.Hom Mathlib.Order.PropInstances Mathlib.Order.Rel.GaloisConnection Mathlib.Order.RelClasses Mathlib.Order.RelIso.Basic Mathlib.Order.RelIso.Set Mathlib.Order.ScottContinuity Mathlib.Order.SemiconjSup Mathlib.Order.SetIsMax Mathlib.Order.SetNotation Mathlib.Order.Set Mathlib.Order.SymmDiff Mathlib.Order.Synonym Mathlib.Order.TypeTags Mathlib.Order.ULift Mathlib.Order.UpperLower.Relative Mathlib.Order.WellFounded Mathlib.Order.WithBot Mathlib.Order.Zorn Mathlib.RingTheory.Congruence.Basic Mathlib.RingTheory.Congruence.Defs Mathlib.RingTheory.Congruence.Opposite Mathlib.RingTheory.LocalRing.Defs Mathlib.RingTheory.NonUnitalSubsemiring.Defs Mathlib.RingTheory.OreLocalization.OreSet Mathlib.RingTheory.RingInvo Mathlib.SetTheory.Cardinal.Defs Mathlib.SetTheory.PGame.Basic Mathlib.SetTheory.ZFC.PSet Mathlib.Std.Data.HashMap Mathlib.Tactic.AdaptationNote Mathlib.Tactic.ApplyAt Mathlib.Tactic.ApplyCongr Mathlib.Tactic.ApplyFun Mathlib.Tactic.ApplyWith Mathlib.Tactic.ArithMult.Init Mathlib.Tactic.ArithMult Mathlib.Tactic.Attr.Core Mathlib.Tactic.Attr.Register Mathlib.Tactic.Basic Mathlib.Tactic.Bound.Attribute Mathlib.Tactic.Bound.Init Mathlib.Tactic.ByContra Mathlib.Tactic.CC.Addition Mathlib.Tactic.CC.Datatypes Mathlib.Tactic.CC.Lemmas Mathlib.Tactic.CC.MkProof Mathlib.Tactic.CC Mathlib.Tactic.CancelDenoms.Core Mathlib.Tactic.CasesM Mathlib.Tactic.Cases Mathlib.Tactic.CategoryTheory.Coherence.Datatypes Mathlib.Tactic.CategoryTheory.Coherence.Normalize Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence Mathlib.Tactic.Change Mathlib.Tactic.Check Mathlib.Tactic.Choose Mathlib.Tactic.Clean Mathlib.Tactic.ClearExcept Mathlib.Tactic.ClearExclamation Mathlib.Tactic.Clear_ Mathlib.Tactic.Coe Mathlib.Tactic.CongrExclamation Mathlib.Tactic.CongrM Mathlib.Tactic.Constructor Mathlib.Tactic.Continuity.Init Mathlib.Tactic.Continuity Mathlib.Tactic.ContinuousFunctionalCalculus Mathlib.Tactic.Contrapose Mathlib.Tactic.Conv Mathlib.Tactic.Convert Mathlib.Tactic.Core Mathlib.Tactic.DefEqTransformations Mathlib.Tactic.DeprecateTo Mathlib.Tactic.DeriveCountable Mathlib.Tactic.DeriveTraversable Mathlib.Tactic.Eqns Mathlib.Tactic.ErwQuestion Mathlib.Tactic.Eval Mathlib.Tactic.ExistsI Mathlib.Tactic.Explode.Datatypes Mathlib.Tactic.Explode.Pretty Mathlib.Tactic.Explode Mathlib.Tactic.ExtendDoc Mathlib.Tactic.ExtractGoal Mathlib.Tactic.ExtractLets Mathlib.Tactic.FBinop Mathlib.Tactic.FailIfNoProgress Mathlib.Tactic.FastInstance Mathlib.Tactic.FindSyntax Mathlib.Tactic.Find Mathlib.Tactic.Finiteness.Attr Mathlib.Tactic.FunProp.Attr Mathlib.Tactic.FunProp.Core Mathlib.Tactic.FunProp.Decl Mathlib.Tactic.FunProp.Elab Mathlib.Tactic.FunProp.FunctionData Mathlib.Tactic.FunProp.Mor Mathlib.Tactic.FunProp.Theorems Mathlib.Tactic.FunProp.ToBatteries Mathlib.Tactic.FunProp.Types Mathlib.Tactic.FunProp Mathlib.Tactic.GCongr.CoreAttrs Mathlib.Tactic.GCongr.Core Mathlib.Tactic.GCongr.ForwardAttr Mathlib.Tactic.GCongr Mathlib.Tactic.GRewrite.Core Mathlib.Tactic.GRewrite.Elab Mathlib.Tactic.GRewrite Mathlib.Tactic.GeneralizeProofs Mathlib.Tactic.Generalize Mathlib.Tactic.GuardGoalNums Mathlib.Tactic.GuardHypNums Mathlib.Tactic.HaveI Mathlib.Tactic.Have Mathlib.Tactic.HigherOrder Mathlib.Tactic.ITauto Mathlib.Tactic.InferParam Mathlib.Tactic.Inhabit Mathlib.Tactic.IrreducibleDef Mathlib.Tactic.Lemma Mathlib.Tactic.LiftLets Mathlib.Tactic.Lift Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Gauss Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.PositiveVector Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm Mathlib.Tactic.Linter.DeprecatedModule Mathlib.Tactic.Linter.PPRoundtrip Mathlib.Tactic.Linter.Style Mathlib.Tactic.Linter.TextBased Mathlib.Tactic.Linter.UpstreamableDecl Mathlib.Tactic.Measurability.Init Mathlib.Tactic.Measurability Mathlib.Tactic.MkIffOfInductiveProp Mathlib.Tactic.Monotonicity.Attr Mathlib.Tactic.Monotonicity.Basic Mathlib.Tactic.Monotonicity.Lemmas Mathlib.Tactic.Monotonicity Mathlib.Tactic.MoveAdd Mathlib.Tactic.Nontriviality.Core Mathlib.Tactic.Nontriviality Mathlib.Tactic.NormNum.Core Mathlib.Tactic.NormNum.Result Mathlib.Tactic.NthRewrite Mathlib.Tactic.Observe Mathlib.Tactic.OfNat Mathlib.Tactic.Order.CollectFacts Mathlib.Tactic.Order.Graph.Basic Mathlib.Tactic.Order.Graph.Tarjan Mathlib.Tactic.Order.Preprocessing Mathlib.Tactic.Order Mathlib.Tactic.PPWithUniv Mathlib.Tactic.Peel Mathlib.Tactic.ProdAssoc Mathlib.Tactic.Propose Mathlib.Tactic.ProxyType Mathlib.Tactic.Push Mathlib.Tactic.RSuffices Mathlib.Tactic.Recall Mathlib.Tactic.Recover Mathlib.Tactic.ReduceModChar.Ext Mathlib.Tactic.Relation.Rfl Mathlib.Tactic.Relation.Symm Mathlib.Tactic.RenameBVar Mathlib.Tactic.Rename Mathlib.Tactic.Replace Mathlib.Tactic.Sat.FromLRAT Mathlib.Tactic.Says Mathlib.Tactic.ScopedNS Mathlib.Tactic.SetLike Mathlib.Tactic.Set Mathlib.Tactic.SimpIntro Mathlib.Tactic.SimpRw Mathlib.Tactic.Simproc.ExistsAndEq Mathlib.Tactic.Simps.Basic Mathlib.Tactic.Simps.NotationClass Mathlib.Tactic.SplitIfs Mathlib.Tactic.Spread Mathlib.Tactic.StacksAttribute Mathlib.Tactic.Subsingleton Mathlib.Tactic.Substs Mathlib.Tactic.SuccessIfFailWithMsg Mathlib.Tactic.SudoSetOption Mathlib.Tactic.SuppressCompilation Mathlib.Tactic.SwapVar Mathlib.Tactic.TFAE Mathlib.Tactic.TautoSet Mathlib.Tactic.Tauto Mathlib.Tactic.TermCongr Mathlib.Tactic.ToAdditive.Frontend Mathlib.Tactic.ToAdditive Mathlib.Tactic.ToExpr Mathlib.Tactic.ToLevel Mathlib.Tactic.Trace Mathlib.Tactic.TryThis Mathlib.Tactic.TypeCheck Mathlib.Tactic.TypeStar Mathlib.Tactic.UnsetOption Mathlib.Tactic.Use Mathlib.Tactic.Variable Mathlib.Tactic.WLOG Mathlib.Tactic.Widget.Calc Mathlib.Tactic.Widget.CongrM Mathlib.Tactic.Widget.Conv Mathlib.Tactic.Widget.GCongr Mathlib.Tactic.Widget.InteractiveUnfold Mathlib.Tactic.Widget.SelectInsertParamsClass Mathlib.Tactic.Widget.SelectPanelUtils Mathlib.Tactic.WithoutCDot Mathlib.Tactic.Zify Mathlib.Testing.Plausible.Sampleable Mathlib.Testing.Plausible.Testable Mathlib.Topology.ContinuousMap.Defs Mathlib.Topology.Defs.Basic Mathlib.Topology.Defs.Filter Mathlib.Topology.Defs.Sequences Mathlib.Topology.Sheaves.Init Mathlib.Util.AddRelatedDecl Mathlib.Util.AssertExistsExt Mathlib.Util.AssertExists Mathlib.Util.AssertNoSorry Mathlib.Util.AtomM Mathlib.Util.CompileInductive Mathlib.Util.CountHeartbeats Mathlib.Util.Delaborators Mathlib.Util.DischargerAsTactic Mathlib.Util.Export Mathlib.Util.FormatTable Mathlib.Util.GetAllModules Mathlib.Util.LongNames Mathlib.Util.MemoFix Mathlib.Util.Notation3 Mathlib.Util.PPOptions Mathlib.Util.ParseCommand Mathlib.Util.Qq Mathlib.Util.Simp Mathlib.Util.SleepHeartbeats Mathlib.Util.Superscript Mathlib.Util.SynthesizeUsing Mathlib.Util.Tactic Mathlib.Util.TermReduce Mathlib.Util.TransImports Mathlib.Util.WhatsNew Mathlib.Util.WithWeakNamespace |
1 |
Declarations diff
+ S1
+ doubleUnderscore
+ eraseIdx_insertIdx_self
+ insertIdx_eraseIdx_self
+ nodup_append'
+ showLinter
- doubleUnderscore:
- idxOf_le_length
- idxOf_lt_length_iff
- insertIdx_eraseIdx
- nodup_append
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.
No changes to technical debt.
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).
Member
|
If I compute a diff between this PR and #26103 on the command line, then the diff is quite large. So I don't know what is going on. But I would really like to split this into two pieces. One about the show linter, and the other about the rest. |
Collaborator
|
The main
The result should be something like diff.txt Note: This diff still contains |
Member
|
Thanks for posting those instructions! |
kim-em
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jul 3, 2025
* fix * fixes * chore: adaptations for nightly-2025-06-16 (leanprover-community#25994) * chore: bump to nightly-2025-06-03 * fix * fix * Update lean-toolchain for testing leanprover/lean4#8610 * fix * revert change in `Mathlib.Data.ZMOD.Basic` * fix Mathlib/Data/List/EditDistance/Estimator.lean * give specialized simp lemmas higher prio * simp can prove these * simp can prove these * chore: bump to nightly-2025-06-04 * bump toolchain * Adapt eqns * Revert "Adapt eqns" This reverts commit 34f1f7f. * Simply remove check for now * fix a bunch * fixes? * chore: adaptations for nightly-2025-06-04 * add `simp low` lemma `injOn_of_eq_iff_eq` * wip * wip * wip * fix * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <johan@commelin.net> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes --------- 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: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com> * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 (leanprover-community#26043) * revert change in `Mathlib.Data.ZMOD.Basic` * fix Mathlib/Data/List/EditDistance/Estimator.lean * give specialized simp lemmas higher prio * simp can prove these * simp can prove these * chore: bump to nightly-2025-06-04 * bump toolchain * Adapt eqns * Revert "Adapt eqns" This reverts commit 34f1f7f. * Simply remove check for now * fix a bunch * fixes? * chore: adaptations for nightly-2025-06-04 * add `simp low` lemma `injOn_of_eq_iff_eq` * wip * wip * wip * fix * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <johan@commelin.net> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 --------- Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> * Update lean-toolchain for testing leanprover/lean4#8577 * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8804 * Update lean-toolchain for testing leanprover/lean4#8699 * bump Qq and batteries * meta adaptations * bump aesop * fix * fix (adaptation note) * Update lean-toolchain for leanprover/lean4#8699 * shake * chore: adaptations for nightly-2025-06-18 (leanprover-community#26077) * bump toolchain * Adapt eqns * Revert "Adapt eqns" This reverts commit 34f1f7f. * Simply remove check for now * fix a bunch * fixes? * chore: adaptations for nightly-2025-06-04 * add `simp low` lemma `injOn_of_eq_iff_eq` * wip * wip * wip * fix * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <johan@commelin.net> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Rob23oba <101damnations@github.com> Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> * chore: bump to nightly-2025-06-19 * feat: add algebra shims for Grind.Nat/IntModule (leanprover-community#26133) This PR adds shims so `grind` will understand Mathlib's `AddCommMonoid` and `AddCommGroup`. (Subsequent shims will connect up the order structures for modules and rings.) * fix * Update lean-toolchain for leanprover/lean4#8699 * fix: correct memoFix's use of unsafe code * fix: adjust noncomputable annotations for new compiler * fix: replace use of `open private _ in` with `open private _ from` The implementation of `open private _ from` relies on specific internals of the old compiler and will no longer work. * remove mul_hmul * chore: adjust one maxHeartbeats for the new compiler * linter * feat: generalize grind algebra shims (leanprover-community#26131) This PR extends the shims converting from Mathlib to `Lean.Grind` typeclasses, now that `grind` knows about (non-commutative)-(semi)-rings. * chore: bump to nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 (leanprover-community#26209) * Trigger CI for leanprover-community/batteries#1220 * Merge master into nightly-testing * chore: bump to nightly-2025-06-05 * Kick CI * Bump lean4-cli * Bump import-graph * Kick CI * update lakefile * chore: use more robust syntax quotation in Shake * Trigger CI for leanprover/lean4#8419 * Revert "chore: use more robust syntax quotation in Shake" This reverts commit cd87328. * fix(Shake): fix import syntax @Kha this is deliberately using this approach because syntax quotations are also not robust but for a different reason: they fail to parse the new versions of the syntax (and do so at run time). And using all the optional doohickeys will not be future proof. The current setup is explicitly meant to ping me when there is a syntax change so I can evaluate the right way to handle it. In this case we want all the module options to be ignored (treated the same as a regular import for the purpose of dependency tracking), we don't want to fail. * cleanup lakefile * chore: bump to nightly-2025-06-06 * Update lean-toolchain for testing leanprover/lean4#8653 * fix * how did this get dropped?!?! * chore: bump to nightly-2025-06-07 * chore: bump to nightly-2025-06-08 * chore: bump to nightly-2025-06-09 * fix lakefile * fix lint-style for new Lean.Options API * chore: bump to nightly-2025-06-10 * chore: bump to nightly-2025-06-09 * merge lean-pr-testing-4 * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <johan@commelin.net> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 * Merge master into nightly-testing * chore: bump to nightly-2025-06-19 * fix * remove mul_hmul * linter * chore: bump to nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 --------- 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: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Rob23oba <101damnations@github.com> Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> * Update lean-toolchain for testing leanprover/lean4#8914 * chore: bump to nightly-2025-06-21 * fix * fixes * fixes * fixes * updated lake manifest * comment out tests * chore: fix for nightly-testing (leanprover-community#26246) * fix * fix * fix grind typeclasses * chore: adaptations for nightly-2025-06-20 * lake update * Update lean-toolchain for leanprover/lean4#8914 * fix grind instance * chore: bump to nightly-2025-06-22 * chore: bump to nightly-2025-06-23 * chore: rm unused `Lean.Util.Paths` import & use updated batteries * Ensure we checkout mathlib4 master, not nightly-testing master (which does not exist) * merge lean-pr-testing-8804 * Bump dependencies and silence linter. * Fixes (Now `elabSimpArgs` already handles `*`, so we can delete the associated code.) * lake update; disable unusedSimpArgs in Batteries * lkae update aesop * disable unusedSimpArgs in MathlibTest * fix grind instance priorities * comment out MathlibTest/zmod with adaptation note * touch for CI * chore: bump to nightly-2025-06-24 * Kick CI * Bump batteries * Guessing adaption for leanprover/lean4#8929 * chore: bump to nightly-2025-06-25 * fix: workflow merging master into nightly-testing * fix * chore: cache get uses tracking remote * touch for new CI * restart CI * chore: bump to nightly-2025-06-26 * Update lean-toolchain for testing leanprover/lean4#8928 * Teach Mathlib about `mrefine` * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8980 * chore: update linter warning test outputs * chore: remove excess line break in deprecation lint now that notes add their own line breaks * chore: more test cleanup * . * cleanup adaptation notes * fix * fix * chore: bump to nightly-2025-06-27 * chore: adaptations for nightly-2025-06-26 (#2) * Merge master into nightly-testing * Merge master into nightly-testing * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * chore: adaptations for nightly-2025-06-27 (#3) * fix tests * chore: bump to nightly-2025-06-28 * Merge master into nightly-testing * lintining * Merge master into nightly-testing * unused simp args * chore: bump to nightly-2025-06-29 * chore: adaptations for nightly-2025-06-29 * chore: adaptations for nightly-2025-06-28 (#5) * chore: bump to nightly-2025-06-11 * chore: adaptations for nightly-2025-06-11 * Update Shake/Main.lean Co-authored-by: Johan Commelin <johan@commelin.net> * Apply suggestions from code review * revert * chore: adaptations for nightly-2025-06-11 * cleanup grind tests * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8419 * chore: bump to nightly-2025-06-12 * merge lean-pr-testing-8653 * adaptation note * oops * chore: adaptations for nightly-2025-06-12 * remove nolint simpNF * remove spurious file * Update lean-toolchain for testing leanprover/lean4#8751 * fix * chore: bump to nightly-2025-06-13 * Merge master into nightly-testing * fix * remove upstreamed * drop no-op `show` * chore: bump to nightly-2025-06-14 * chore: bump to nightly-2025-06-15 * intentionally left blank * fix tests * chore: bump to nightly-2025-06-16 * fix upstream * fix * fix * fixes * chore: adaptations for nightly-2025-06-16 * chore: bump to nightly-2025-06-17 * fixes * more fixes * fixes! * more fixes! * hmm * chore: adaptations for nightly-2025-06-17 * chore: adaptations for nightly-2025-06-17 * chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749) Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`. Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633 Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> * Update lean-toolchain for testing leanprover/lean4#8577 * chore: bump to nightly-2025-06-18 * chore: adaptations for nightly-2025-06-18 * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8804 * Update lean-toolchain for testing leanprover/lean4#8699 * bump Qq and batteries * meta adaptations * bump aesop * fix * fix (adaptation note) * Update lean-toolchain for leanprover/lean4#8699 * shake * chore: bump to nightly-2025-06-19 * fix * Update lean-toolchain for leanprover/lean4#8699 * fix: correct memoFix's use of unsafe code * fix: adjust noncomputable annotations for new compiler * fix: replace use of `open private _ in` with `open private _ from` The implementation of `open private _ from` relies on specific internals of the old compiler and will no longer work. * remove mul_hmul * chore: adjust one maxHeartbeats for the new compiler * linter * chore: bump to nightly-2025-06-20 * chore: adaptations for nightly-2025-06-20 * Update lean-toolchain for testing leanprover/lean4#8914 * chore: bump to nightly-2025-06-21 * fix * fixes * fixes * fixes * updated lake manifest * comment out tests * chore: fix for nightly-testing (leanprover-community#26246) * fix * fix * fix grind typeclasses * chore: adaptations for nightly-2025-06-20 * lake update * Update lean-toolchain for leanprover/lean4#8914 * fix grind instance * chore: bump to nightly-2025-06-22 * chore: bump to nightly-2025-06-23 * chore: rm unused `Lean.Util.Paths` import & use updated batteries * Ensure we checkout mathlib4 master, not nightly-testing master (which does not exist) * merge lean-pr-testing-8804 * Bump dependencies and silence linter. * Fixes (Now `elabSimpArgs` already handles `*`, so we can delete the associated code.) * lake update; disable unusedSimpArgs in Batteries * lkae update aesop * disable unusedSimpArgs in MathlibTest * fix grind instance priorities * comment out MathlibTest/zmod with adaptation note * touch for CI * chore: bump to nightly-2025-06-24 * Kick CI * Bump batteries * Guessing adaption for leanprover/lean4#8929 * chore: bump to nightly-2025-06-25 * fix: workflow merging master into nightly-testing * fix * chore: cache get uses tracking remote * touch for new CI * restart CI * chore: bump to nightly-2025-06-26 * Update lean-toolchain for testing leanprover/lean4#8928 * Teach Mathlib about `mrefine` * Merge master into nightly-testing * Update lean-toolchain for testing leanprover/lean4#8980 * chore: update linter warning test outputs * chore: remove excess line break in deprecation lint now that notes add their own line breaks * chore: more test cleanup * . * cleanup adaptation notes * fix * fix * chore: bump to nightly-2025-06-27 * Merge master into nightly-testing * Merge master into nightly-testing * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * re-enable unusedSimpArgs * fix tests * chore: bump to nightly-2025-06-28 * Merge master into nightly-testing * lintining * lint --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Rob23oba <101damnations@github.com> Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Cameron Zwarich <cameron@lean-fro.org> Co-authored-by: Mac Malone <mac@lean-fro.org> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Sebastian Graf <sg@lean-fro.org> Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com> * Merge master into nightly-testing * chore: robustify `open Mathlib` benchmark * deprecations * Update lean-toolchain for testing leanprover/lean4#9086 * Merge master into nightly-testing * fixes * chore: bump to nightly-2025-06-30 * lake update * lake update * lake update * lake update * lake update * . * Merge master into nightly-testing * Merge master into nightly-testing * Merge master into nightly-testing * Merge master into nightly-testing * cleanup * unusedSimpArgs * bump toolchain * lake update * Merge master into nightly-testing * Merge master into nightly-testing * chore: adaptations for nightly-2025-07-01 * add adaptation note * add adaptation note * chore: bump to nightly-2025-07-02 * fixes * Merge master into nightly-testing * fixes * update test output * Merge master into nightly-testing * Merge master into nightly-testing * chore: bump to nightly-2025-07-03 * chore: adaptations for nightly-2025-07-03 --------- Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: leanprover-community-mathlib4-bot <129911861+leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: Rob23oba <101damnations@github.com> Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Kenny Lau <kc_kennylau@yahoo.com.hk> Co-authored-by: Fabrizio Barroero <fbarroero@gmail.com> Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> Co-authored-by: Cameron Zwarich <cameron@lean-fro.org> Co-authored-by: Mac Malone <mac@lean-fro.org> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Sebastian Graf <sg@lean-fro.org> Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
9 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.