chore: lint show (adaptation for leanprover/lean4#7395)#26103
Closed
jcommelin wants to merge 3 commits intoleanprover-community:bump/v4.22.0from
Closed
chore: lint show (adaptation for leanprover/lean4#7395)#26103jcommelin wants to merge 3 commits intoleanprover-community:bump/v4.22.0from
show (adaptation for leanprover/lean4#7395)#26103jcommelin wants to merge 3 commits intoleanprover-community:bump/v4.22.0from
Conversation
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>
kbuzzard
reviewed
Jun 18, 2025
| ⟨fun f g => | ||
| { toFun := fun m => f m * g m, | ||
| map_mul' := fun x y => by | ||
| show f (x * y) * g (x * y) = f x * g x * (f y * g y) |
Member
There was a problem hiding this comment.
Is this randomly needed now? Is what's going on understood?
Collaborator
There was a problem hiding this comment.
I think this was here before but was removed in f076c12. We decided to use show for no-ops so that one has been reverted.
kbuzzard
reviewed
Jun 18, 2025
| PseudoMetricSpace E where | ||
| dist x y := ‖x - y‖ | ||
| dist_self x := by | ||
| show ‖x - x‖ = 0 |
Member
There was a problem hiding this comment.
Similarly these. What's going on?
kbuzzard
reviewed
Jun 18, 2025
| HasSum (fun n : ℕ => x ^ (n + 1) / (n + 1)) (-log (1 - x)) := by | ||
| rw [Summable.hasSum_iff_tendsto_nat] | ||
| · rw [tendsto_iff_norm_sub_tendsto_zero] | ||
| · show Tendsto (fun n : ℕ => ∑ i ∈ range n, x ^ (i + 1) / (i + 1)) atTop (𝓝 (-log (1 - x))) |
Member
There was a problem hiding this comment.
I'm a bit confused about why these are appearing. Maybe I'll stop mentioning them now.
Collaborator
There was a problem hiding this comment.
Again, they were removed in f076c12 and then re-added.
Member
|
OK so there are conflicts and CI is failing, but I have read through the entire diff because I'm procrastinating about doing something else. There are under ten randomly-added I guess the diff would be even easier to understand if |
Member
|
Actually one last thought on this: I am a bit unclear myself about whether |
Collaborator
|
I'm just going to note that #25749 has already been merged into nightly-testing and this is just to make the diff on #26077 more manageable (see https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/.2326077.20adaptations.20for.20nightly-2025-06-18/with/524729820) |
PR summary 5cdffe1590Import 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 |
|---|---|
869 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.Hom.Basic 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
+ H0
+ H0IsoOfIsTrivial
+ H0IsoOfIsTrivial_hom_apply
+ H0IsoOfIsTrivial_hom_hom
+ H0IsoOfIsTrivial_inv_apply
+ H0LequivOfIsTrivial
+ H0LequivOfIsTrivial_apply
+ H0LequivOfIsTrivial_eq_subtype
+ H0LequivOfIsTrivial_symm_apply
+ H1
+ H1IsoOfIsTrivial
+ H1IsoOfIsTrivial_H1π_apply_apply
+ H1IsoOfIsTrivial_inv_apply
+ H1LequivOfIsTrivial
+ H1LequivOfIsTrivial_comp_H1_π_apply_apply
+ H1LequivOfIsTrivial_comp_H1π
+ H1LequivOfIsTrivial_symm_apply
+ H1_induction_on
+ H1π
+ H1π_comp_H1IsoOfIsTrivial_hom
+ H1π_eq_zero_iff
+ H2
+ H2_induction_on
+ H2π
+ H2π_eq_zero_iff
+ 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
Author
That is true! And thanks again for preparing the PR into But just to clarify: anything can be merged into nightly-testing. This doesn't require much (or any!) review. At some point, this code converges towards master, and it needs to pass a review somewhere in that process. The way we've set up the system, this review happens at the moment the code moves from So in that sense, Kevin's review is still very helpful. |
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
4 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.
Adds
showas an exception to the unused tactic linter and adds a separate linter forshows that should be replaced bychange.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