Skip to content

Commit 1b97255

Browse files
nomeataclaude
nomeata
and
claude
committed
chore: update nolints.json after merge
Lost in the merge of nightly-testing-2026-05-06; regenerated via `lake exe runLinter --update Mathlib`. Net -49 lines: stale entries pruned, the simpNF regressions exposed by the recent `useBackward` removals folded back in. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 4a4a28a commit 1b97255

1 file changed

Lines changed: 86 additions & 135 deletions

File tree

‎scripts/nolints.json‎

Lines changed: 86 additions & 135 deletions
Original file line numberDiff line numberDiff line change
@@ -1,40 +1,29 @@
1-
[["docBlame", "Affine.Simplex.points"],
2-
["docBlame", "AlgebraicGeometry.PresheafedSpace.Hom.base"],
3-
["docBlame", "AlgebraicGeometry.PresheafedSpace.Hom.c"],
4-
["docBlame", "AlgebraicGeometry.PresheafedSpace.carrier"],
5-
["docBlame", "AlgebraicGeometry.PresheafedSpace.presheaf"],
6-
["docBlame", "AlgebraicTopology.DoldKan.MorphComponents.a"],
7-
["docBlame", "AlgebraicTopology.DoldKan.MorphComponents.b"],
8-
["docBlame", "Array.cyclicPermute!.cyclicPermuteAux"],
1+
[["docBlame", "CongrMetaM"],
2+
["docBlame", "CongrState"],
3+
["docBlame", "Cont"],
4+
["docBlame", "ContT"],
5+
["docBlame", "LawfulMonadCont"],
6+
["docBlame", "MonadCont"],
7+
["docBlame", "MonadWriter"],
8+
["docBlame", "Writer"],
9+
["docBlame", "eqns"],
10+
["docBlame", "eqnsAttribute"],
911
["docBlame", "Bifunctor.bimap"],
1012
["docBlame", "Bitraversable.bitraverse"],
11-
["docBlame", "Bundle.TotalSpace.mk'"],
12-
["docBlame", "Bundle.TotalSpace.snd"],
1313
["docBlame", "CFilter.f"],
1414
["docBlame", "CFilter.inf"],
1515
["docBlame", "CFilter.pt"],
16-
["docBlame", "CliffordAlgebra.EvenHom.bilin"],
1716
["docBlame", "Congr!.elabConfig"],
18-
["docBlame", "CongrMetaM"],
19-
["docBlame", "CongrState"],
20-
["docBlame", "Cont"],
21-
["docBlame", "ContT"],
2217
["docBlame", "ContT.map"],
2318
["docBlame", "ContT.withContT"],
24-
["docBlame", "Ctop.Realizer.F"],
25-
["docBlame", "Ctop.Realizer.σ"],
2619
["docBlame", "Ctop.f"],
2720
["docBlame", "Ctop.inter"],
2821
["docBlame", "Ctop.top"],
2922
["docBlame", "DilationEquiv.toDilation"],
30-
["docBlame", "DirectSum.Decomposition.decompose'"],
31-
["docBlame", "DirectSum.GAlgebra.toFun"],
3223
["docBlame", "EsakiaHom.toPseudoEpimorphism"],
3324
["docBlame", "EuclideanDomain.wellFoundedRelation"],
3425
["docBlame", "ExceptT.callCC"],
3526
["docBlame", "ExceptT.mkLabel"],
36-
["docBlame", "FBinopElab.SRec.args"],
37-
["docBlame", "FBinopElab.SRec.name"],
3827
["docBlame", "FBinopElab.elabBinOp"],
3928
["docBlame", "FiberBundle.trivializationAt'"],
4029
["docBlame", "FiberBundle.trivializationAtlas'"],
@@ -43,142 +32,37 @@
4332
["docBlame", "FiberBundleCore.indexAt"],
4433
["docBlame", "FiberPrebundle.pretrivializationAt"],
4534
["docBlame", "FiberPrebundle.pretrivializationAtlas"],
46-
["docBlame", "Filter.Realizer.F"],
47-
["docBlame", "Filter.Realizer.σ"],
48-
["docBlame", "GenContFract.IntFractPair.b"],
49-
["docBlame", "GenContFract.IntFractPair.fr"],
50-
["docBlame", "GromovHausdorff.AuxGluingStruct.Space"],
51-
["docBlame", "GromovHausdorff.AuxGluingStruct.embed"],
52-
["docBlame", "GromovHausdorff.AuxGluingStruct.metric"],
5335
["docBlame", "HSpace.e"],
5436
["docBlame", "HSpace.eHmul"],
5537
["docBlame", "HSpace.hmul"],
5638
["docBlame", "HSpace.hmulE"],
57-
["docBlame", "HomogeneousLocalization.NumDenSameDeg.deg"],
58-
["docBlame", "HomogeneousLocalization.NumDenSameDeg.den"],
59-
["docBlame", "HomogeneousLocalization.NumDenSameDeg.num"],
60-
["docBlame", "HomologicalComplex.Hom.f"],
6139
["docBlame", "HomologicalComplex.X"],
6240
["docBlame", "HomologicalComplex.d"],
6341
["docBlame", "Homotopy.hom"],
64-
["docBlame", "Ideal.Filtration.N"],
6542
["docBlame", "IntermediateField.delabAdjoinNotation"],
6643
["docBlame", "IsAdjoinRoot.map"],
67-
["docBlame", "IsDedekindDomain.HeightOneSpectrum.asIdeal"],
6844
["docBlame", "JordanHolderLattice.IsMaximal"],
6945
["docBlame", "JordanHolderLattice.Iso"],
70-
["docBlame", "LawfulMonadCont"],
71-
["docBlame", "Lean.Elab.Command.irredDefLemma"],
72-
["docBlame", "Lean.Export.Alloc"],
73-
["docBlame", "Lean.Export.Alloc.map"],
74-
["docBlame", "Lean.Export.Alloc.next"],
75-
["docBlame", "Lean.Export.Entry"],
76-
["docBlame", "Lean.Export.OfState"],
77-
["docBlame", "Lean.Export.OfState.get"],
78-
["docBlame", "Lean.Export.OfState.modify"],
79-
["docBlame", "Lean.Export.State"],
80-
["docBlame", "Lean.Export.State.defs"],
81-
["docBlame", "Lean.Export.State.exprs"],
82-
["docBlame", "Lean.Export.State.levels"],
83-
["docBlame", "Lean.Export.State.names"],
84-
["docBlame", "Lean.Export.State.stk"],
85-
["docBlame", "Lean.Export.alloc"],
86-
["docBlame", "Lean.Export.biStr"],
87-
["docBlame", "Lean.Export.exportDef"],
88-
["docBlame", "Lean.Export.exportExpr"],
89-
["docBlame", "Lean.Export.exportLevel"],
90-
["docBlame", "Lean.Export.exportName"],
91-
["docBlame", "Lean.Export.runExportM"],
9246
["docBlame", "Lean.ExportM"],
93-
["docBlame", "Lean.Expr.bvarIdx?"],
94-
["docBlame", "Lean.Expr.getRevArg?"],
95-
["docBlame", "Lean.Expr.modifyAppArgM"],
96-
["docBlame", "Lean.Expr.modifyRevArg"],
97-
["docBlame", "Lean.MVarId.casesType"],
98-
["docBlame", "Lean.MVarId.congrCore!"],
99-
["docBlame", "Lean.Meta.RefinedDiscrTree.instInhabitedPartialMatch.default"],
100-
["docBlame", "Lean.Name.isBlackListed"],
101-
["docBlame", "Lean.PHashSet.toList"],
102-
["docBlame", "Lean.Parser.Attr.higherOrder"],
103-
["docBlame", "Lean.Parser.Tactic.applyCongr"],
104-
["docBlame", "Lists.Equiv.decidable"],
105-
["docBlame", "Lists.Subset.decidable"],
106-
["docBlame", "Lists.mem.decidable"],
107-
["docBlame", "LocallyFinite.Realizer.bas"],
108-
["docBlame", "LocallyFinite.Realizer.sets"],
109-
["docBlame", "Mathlib.Command.Variable.completeBinders"],
110-
["docBlame", "Mathlib.Command.Variable.variable?.checkRedundant"],
111-
["docBlame", "Mathlib.Command.Variable.variable?.maxSteps"],
112-
["docBlame", "Mathlib.Deriving.Fintype.mkFintype"],
113-
["docBlame", "Mathlib.Deriving.Fintype.mkFintypeInstanceHandler"],
114-
["docBlame", "Mathlib.Linter.Flexible.instInhabitedStained.default"],
115-
["docBlame", "Mathlib.Linter.TextBased.instInhabitedStyleError.default"],
116-
["docBlame", "Mathlib.Linter.instInhabitedFormatError.default"],
117-
["docBlame", "Mathlib.Linter.instInhabitedImportState.default"],
118-
["docBlame", "Mathlib.Meta.NormNum.proveNatFibAux"],
119-
["docBlame", "Mathlib.Notation3.expandFoldl"],
120-
["docBlame", "Mathlib.Notation3.expandFoldr"],
121-
["docBlame", "Mathlib.Notation3.prettyPrintOpt"],
122-
["docBlame", "Mathlib.Tactic.Coherence.LiftHom.lift"],
123-
["docBlame", "Mathlib.Tactic.Coherence.LiftObj.lift"],
124-
["docBlame", "Mathlib.Tactic.Conv.convRun_conv_"],
125-
["docBlame", "Mathlib.Tactic.ElimApp.evalNames"],
126-
["docBlame", "Mathlib.Tactic.Find.findDeclsPerHead"],
127-
["docBlame", "Mathlib.Tactic.Find.findType"],
128-
["docBlame", "Mathlib.Tactic.GCongr.ForwardExt.eval"],
129-
["docBlame", "Mathlib.Tactic.GCongr.exact"],
130-
["docBlame", "Mathlib.Tactic.Monotonicity.mono.side"],
131-
["docBlame", "Mathlib.Tactic.Sat.buildReify.mkPS"],
132-
["docBlame", "Mathlib.Tactic.evalIntrov"],
133-
["docBlame", "Mathlib.Tactic.setArgsRest"],
134-
["docBlame", "Mathlib.Tactic.usingArg"],
135-
["docBlame", "Mathlib.Tactic.withArgs"],
136-
["docBlame", "Mathlib.WhatsNew.diffExtension"],
137-
["docBlame", "Mathlib.WhatsNew.whatsNew"],
138-
["docBlame", "Matrix.TransvectionStruct.c"],
139-
["docBlame", "Matrix.TransvectionStruct.i"],
140-
["docBlame", "Matrix.TransvectionStruct.j"],
14147
["docBlame", "MaximalSpectrum.asIdeal"],
14248
["docBlame", "ModularForm.«term_∣[_]_»"],
143-
["docBlame", "Module.Baer.supExtensionOfMaxSingleton"],
144-
["docBlame", "Module.End.Eigenvalues.val"],
145-
["docBlame", "MonadCont"],
14649
["docBlame", "MonadCont.Label"],
147-
["docBlame", "MonadCont.Label.apply"],
14850
["docBlame", "MonadCont.callCC"],
14951
["docBlame", "MonadCont.goto"],
150-
["docBlame", "MonadWriter"],
15152
["docBlame", "MonadWriterAdapter.adaptWriter"],
152-
["docBlame", "Monoid.Foldl.get"],
153-
["docBlame", "Monoid.Foldl.mk"],
154-
["docBlame", "Monoid.Foldl.ofFreeMonoid"],
15553
["docBlame", "Monoid.Foldr"],
156-
["docBlame", "Monoid.Foldr.get"],
157-
["docBlame", "Monoid.Foldr.mk"],
158-
["docBlame", "Monoid.Foldr.ofFreeMonoid"],
15954
["docBlame", "Monoid.foldlM"],
160-
["docBlame", "Monoid.foldlM.get"],
161-
["docBlame", "Monoid.foldlM.mk"],
162-
["docBlame", "Monoid.foldlM.ofFreeMonoid"],
16355
["docBlame", "Monoid.foldrM"],
164-
["docBlame", "Monoid.foldrM.get"],
165-
["docBlame", "Monoid.foldrM.mk"],
166-
["docBlame", "Monoid.foldrM.ofFreeMonoid"],
16756
["docBlame", "MvPFunctor.wpRec"],
16857
["docBlame", "MvQPF.P"],
16958
["docBlame", "MvQPF.abs"],
17059
["docBlame", "MvQPF.repr"],
17160
["docBlame", "OptionT.callCC"],
17261
["docBlame", "OptionT.mkLabel"],
173-
["docBlame", "Order.Ideal.PrimePair.F"],
174-
["docBlame", "Order.Ideal.PrimePair.I"],
175-
["docBlame", "Order.PFilter.dual"],
176-
["docBlame", "PProd.mk.injArrow"],
17762
["docBlame", "PowerBasis.basis"],
17863
["docBlame", "PowerBasis.dim"],
17964
["docBlame", "PowerBasis.gen"],
18065
["docBlame", "PrimeSpectrum.asIdeal"],
181-
["docBlame", "Prod.mk.injArrow"],
18266
["docBlame", "ProjectiveSpectrum.asHomogeneousIdeal"],
18367
["docBlame", "QPF.P"],
18468
["docBlame", "QPF.abs"],
@@ -195,8 +79,6 @@
19579
["docBlame", "StateT.callCC"],
19680
["docBlame", "StateT.mkLabel"],
19781
["docBlame", "Stream'.unfolds"],
198-
["docBlame", "Submodule.quotientPi_aux.invFun"],
199-
["docBlame", "Submodule.quotientPi_aux.toFun"],
20082
["docBlame", "Submodule.«term_∙_»"],
20183
["docBlame", "Traversable.foldMap"],
20284
["docBlame", "Traversable.foldl"],
@@ -215,8 +97,6 @@
21597
["docBlame", "VectorPrebundle.pretrivializationAt"],
21698
["docBlame", "VectorPrebundle.pretrivializationAtlas"],
21799
["docBlame", "WithIdeal.i"],
218-
["docBlame", "WittVector.Isocrystal.frob"],
219-
["docBlame", "Writer"],
220100
["docBlame", "WriterT.adapt"],
221101
["docBlame", "WriterT.callCC"],
222102
["docBlame", "WriterT.callCC'"],
@@ -324,6 +204,8 @@
324204
["docBlame", "Mathlib.Command.Variable.completeBinders"],
325205
["docBlame", "Mathlib.Deriving.Fintype.mkFintype"],
326206
["docBlame", "Mathlib.Deriving.Fintype.mkFintypeInstanceHandler"],
207+
["docBlame", "Mathlib.Linter.instInhabitedFormatError.default"],
208+
["docBlame", "Mathlib.Linter.instInhabitedImportState.default"],
327209
["docBlame", "Mathlib.Meta.NormNum.proveNatFibAux"],
328210
["docBlame", "Mathlib.Tactic.Conv.convRun_conv_"],
329211
["docBlame", "Mathlib.Tactic.ElimApp.evalNames"],
@@ -333,15 +215,84 @@
333215
["docBlame", "Module.End.Eigenvalues.val"],
334216
["docBlame", "Order.Ideal.PrimePair.F"],
335217
["docBlame", "Order.Ideal.PrimePair.I"],
218+
["docBlame", "Lean.Meta.RefinedDiscrTree.instInhabitedPartialMatch.default"],
336219
["docBlame", "Mathlib.Command.Variable.variable?.checkRedundant"],
337220
["docBlame", "Mathlib.Command.Variable.variable?.maxSteps"],
221+
["docBlame", "Mathlib.Linter.Flexible.instInhabitedStained.default"],
222+
["docBlame", "Mathlib.Linter.TextBased.instInhabitedStyleError.default"],
338223
["docBlame", "Mathlib.Tactic.Coherence.LiftHom.lift"],
339224
["docBlame", "Mathlib.Tactic.Coherence.LiftObj.lift"],
340225
["docBlame", "Mathlib.Tactic.GCongr.ForwardExt.eval"],
341226
["docBlame", "Mathlib.Tactic.Monotonicity.mono.side"],
342227
["docBlame", "Mathlib.Tactic.Sat.buildReify.mkPS"],
343-
["docBlame", "Lean.Meta.RefinedDiscrTree.instInhabitedPartialMatch.default"],
344-
["docBlame", "Mathlib.Linter.Flexible.instInhabitedStained.default"],
345-
["docBlame", "Mathlib.Linter.instInhabitedImportState.default"],
346-
["docBlame", "Mathlib.Linter.TextBased.instInhabitedStyleError.default"],
347-
["docBlame", "Mathlib.Linter.instInhabitedFormatError.default"]]
228+
["simpNF",
229+
"lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_hom_app_hom_apply_apply"],
230+
["simpNF",
231+
"lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_hom_app_hom_apply_hom_hom"],
232+
["simpNF", "AddEquiv.coe_toAddHom"],
233+
["simpNF", "AlgEquiv.coe_ringEquiv"],
234+
["simpNF", "AlgHom.toFun_eq_coe"],
235+
["simpNF", "CategoryTheory.η_naturality"],
236+
["simpNF", "CategoryTheory.η_naturality_assoc"],
237+
["simpNF", "CommGrpTypeEquivalenceCommGrp.inverse_obj_one"],
238+
["simpNF", "LinearMap.comp_id_fgModuleCat"],
239+
["simpNF", "LinearMap.id_fgModuleCat_comp"],
240+
["simpNF", "ModuleCat.restrictScalarsIsoOfEquiv_hom_apply"],
241+
["simpNF", "ModuleCat.restrictScalarsIsoOfEquiv_inv_apply"],
242+
["simpNF", "MulEquiv.coe_toMulHom"],
243+
["simpNF", "NonUnitalAlgHom.toFun_eq_coe"],
244+
["simpNF", "OpenPartialHomeomorph.lift_openEmbedding_symm_target"],
245+
["simpNF", "Polynomial.toFinsupp_algebraMap"],
246+
["simpNF", "SSet.leftUnitor_hom_app_apply"],
247+
["simpNF", "SSet.leftUnitor_inv_app_apply"],
248+
["simpNF", "SSet.rightUnitor_hom_app_apply"],
249+
["simpNF", "SSet.rightUnitor_inv_app_apply"],
250+
["simpNF", "SSet.tensorHom_app_apply"],
251+
["simpNF", "Set.mem_sep_iff"],
252+
["simpNF", "SimplexCategory.toPartOrd_map_apply"],
253+
["simpNF", "TopCat.presheafToType_map"],
254+
["simpNF", "TopCat.presheafToTypes_map"],
255+
["simpNF", "CategoryTheory.CostructuredArrow.map₂_map_right"],
256+
["simpNF",
257+
"CategoryTheory.FunctorToTypes.inl_comp_binaryCoproductIso_inv_apply"],
258+
["simpNF",
259+
"CategoryTheory.FunctorToTypes.inr_comp_binaryCoproductIso_inv_apply"],
260+
["simpNF",
261+
"CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_symm_app_apply"],
262+
["simpNF", "CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_app_apply"],
263+
["simpNF", "CategoryTheory.StructuredArrow.map₂_map_left"],
264+
["simpNF", "Filter.Germ.const_max"],
265+
["simpNF", "Filter.Germ.const_min"],
266+
["simpNF", "ProbabilityTheory.Kernel.integral_const"],
267+
["simpNF", "ProbabilityTheory.Kernel.lintegral_const"],
268+
["simpNF", "ProbabilityTheory.Kernel.setIntegral_const"],
269+
["simpNF", "ProbabilityTheory.Kernel.setLIntegral_const"],
270+
["simpNF", "SSet.Subcomplex.homOfLE_app_val"],
271+
["simpNF", "SSet.Subcomplex.lift_app_coe"],
272+
["simpNF", "SSet.Subcomplex.toRange_app_val"],
273+
["simpNF", "SSet.Truncated.tensor_map_apply_fst"],
274+
["simpNF", "SSet.Truncated.tensor_map_apply_snd"],
275+
["simpNF", "SSet.stdSimplex.isoNerve_hom_app_apply"],
276+
["simpNF", "SSet.stdSimplex.isoNerve_inv_app_apply"],
277+
["simpNF", "TopologicalSpace.OpenNhds.map_id_obj_unop"],
278+
["simpNF", "CategoryTheory.Cat.Hom.id_obj"],
279+
["simpNF", "CategoryTheory.Cat.Hom₂.id_app"],
280+
["simpNF", "CategoryTheory.Enriched.Functor.associator_hom_apply"],
281+
["simpNF", "CategoryTheory.Enriched.Functor.associator_inv_apply"],
282+
["simpNF",
283+
"CategoryTheory.Enriched.Functor.functorHom_whiskerLeft_natTransEquiv_symm_app"],
284+
["simpNF", "CategoryTheory.Enriched.Functor.natTransEquiv_symm_app_app_apply"],
285+
["simpNF",
286+
"CategoryTheory.Enriched.Functor.natTransEquiv_symm_whiskerRight_functorHom_app"],
287+
["simpNF", "CategoryTheory.Enriched.Functor.whiskerLeft_app_apply"],
288+
["simpNF", "CategoryTheory.Enriched.Functor.whiskerRight_app_apply"],
289+
["simpNF", "CategoryTheory.Functor.LeftExtension.postcompose₂_map_left"],
290+
["simpNF", "CategoryTheory.Functor.LeftExtension.postcomp₁_map_left"],
291+
["simpNF", "CategoryTheory.Functor.LeftExtension.precomp_map_left"],
292+
["simpNF", "CategoryTheory.Functor.Monoidal.associator_hom_app"],
293+
["simpNF", "CategoryTheory.Functor.Monoidal.associator_inv_app"],
294+
["simpNF", "CategoryTheory.Functor.Monoidal.leftUnitor_inv_app"],
295+
["simpNF", "CategoryTheory.Functor.Monoidal.rightUnitor_inv_app"],
296+
["simpNF", "CategoryTheory.Functor.RightExtension.postcompose₂_map_right"],
297+
["simpNF", "CategoryTheory.Functor.RightExtension.postcomp₁_map_right"],
298+
["simpNF", "CategoryTheory.Functor.RightExtension.precomp_map_right"]]

0 commit comments

Comments
 (0)