From 38266dacbb81b23e4968525e9e7e51b8d81d31aa Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Thu, 26 Mar 2026 16:21:23 -0400 Subject: [PATCH 01/10] chore: testlinter --- Mathlib.lean | 38 +++++++++++++++++++ Mathlib/Init.lean | 1 + Mathlib/Tactic.lean | 1 + .../Tactic/Linter/DirectoryDependency.lean | 1 + Mathlib/Tactic/Linter/TestLinter.lean | 20 ++++++++++ 5 files changed, 61 insertions(+) create mode 100644 Mathlib/Tactic/Linter/TestLinter.lean diff --git a/Mathlib.lean b/Mathlib.lean index afbd14b2167acd..57d6cfb36cbc77 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2,6 +2,43 @@ module -- shake: keep-all public import Std public import Batteries +public import Mathlib.A_Foo.ArrowNatTrans +public import Mathlib.A_Foo.BiCoe +public import Mathlib.A_Foo.DelabAnonConstructor +public import Mathlib.A_Foo.LinterCopies +public import Mathlib.A_Foo.LinterCopiesTest +public import Mathlib.A_Foo.LinterTest +public import Mathlib.A_Foo.MetaUtils +public import Mathlib.A_Foo.NewCat +public import Mathlib.A_Foo.PresheafCopy +public import Mathlib.A_Foo.PrivBar +public import Mathlib.A_Foo.PrivBarImport +public import Mathlib.A_Foo.Santi +public import Mathlib.A_Foo.StrictEquivalence +public import Mathlib.A_Foo.StrictEquivalenceEqToHom +public import Mathlib.A_Foo.StrictEquivalenceTemplate +public import Mathlib.A_Foo.Test.Bar +public import Mathlib.A_Foo.Test.Baz +public import Mathlib.A_Foo.Test.Foo +public import Mathlib.A_Foo.UnusedDecidable +public import Mathlib.A_Foo.UnusedInstancesInTypeCopy +public import Mathlib.A_Foo.fltTest +public import Mathlib.A_Foo.fltTest' +public import Mathlib.A_Foo.getBinders +public import Mathlib.A_Foo.importedModule +public import Mathlib.A_Foo.importingModule +public import Mathlib.A_Foo.loopbug +public import Mathlib.A_Foo.nonunital +public import Mathlib.A_Foo.printAxiomsCheck +public import Mathlib.A_Foo.privmodtest +public import Mathlib.A_Foo.showTasks +public import Mathlib.A_Foo.test +public import Mathlib.A_Foo.test2 +public import Mathlib.A_Foo.testForUIIT +public import Mathlib.A_Foo.traceclassnames +public import Mathlib.A_Foo.vi +public import Mathlib.A_Foo.where +public import Mathlib.A_Foo.«test2 copy» public import Mathlib.Algebra.AddConstMap.Basic public import Mathlib.Algebra.AddConstMap.Equiv public import Mathlib.Algebra.AddTorsor.Basic @@ -7028,6 +7065,7 @@ public import Mathlib.Tactic.Linter.PPRoundtrip public import Mathlib.Tactic.Linter.PrivateModule public import Mathlib.Tactic.Linter.Style public import Mathlib.Tactic.Linter.TacticDocumentation +public import Mathlib.Tactic.Linter.TestLinter public import Mathlib.Tactic.Linter.TextBased public import Mathlib.Tactic.Linter.TextBased.UnicodeLinter public import Mathlib.Tactic.Linter.UnusedInstancesInType diff --git a/Mathlib/Init.lean b/Mathlib/Init.lean index 5b971ae06c2bca..8785ce6743fb0a 100644 --- a/Mathlib/Init.lean +++ b/Mathlib/Init.lean @@ -16,6 +16,7 @@ public import Mathlib.Tactic.Linter.Multigoal public import Mathlib.Tactic.Linter.OldObtain public import Mathlib.Tactic.Linter.PrivateModule public import Mathlib.Tactic.Linter.TacticDocumentation +public import Mathlib.Tactic.Linter.TestLinter -- The following import contains the environment extension for the unused tactic linter. public import Mathlib.Tactic.Linter.UnusedTacticExtension public import Mathlib.Tactic.Linter.UnusedTactic diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean index 50bc51f48c5beb..43c132802ba458 100644 --- a/Mathlib/Tactic.lean +++ b/Mathlib/Tactic.lean @@ -177,6 +177,7 @@ public import Mathlib.Tactic.Linter.PPRoundtrip public import Mathlib.Tactic.Linter.PrivateModule public import Mathlib.Tactic.Linter.Style public import Mathlib.Tactic.Linter.TacticDocumentation +public import Mathlib.Tactic.Linter.TestLinter public import Mathlib.Tactic.Linter.TextBased public import Mathlib.Tactic.Linter.TextBased.UnicodeLinter public import Mathlib.Tactic.Linter.UnusedInstancesInType diff --git a/Mathlib/Tactic/Linter/DirectoryDependency.lean b/Mathlib/Tactic/Linter/DirectoryDependency.lean index 5b16685c5332e0..e2c20a79864272 100644 --- a/Mathlib/Tactic/Linter/DirectoryDependency.lean +++ b/Mathlib/Tactic/Linter/DirectoryDependency.lean @@ -228,6 +228,7 @@ def allowedImportDirs : NamePrefixRel := .ofArray #[ (`Mathlib.Tactic.Linter.UnusedInstancesInType, `Mathlib.Lean.Expr.Basic), (`Mathlib.Tactic.Linter.UnusedInstancesInType, `Mathlib.Lean.Environment), (`Mathlib.Tactic.Linter.UnusedInstancesInType, `Mathlib.Lean.Elab.InfoTree), + (`Mathlib.Tactic.Linter.TestLinter, `Mathlib.Lean.Elab.InfoTree), (`Mathlib.Logic, `Batteries), -- TODO: should the next import direction be flipped? diff --git a/Mathlib/Tactic/Linter/TestLinter.lean b/Mathlib/Tactic/Linter/TestLinter.lean new file mode 100644 index 00000000000000..2db78bb6cf7bc1 --- /dev/null +++ b/Mathlib/Tactic/Linter/TestLinter.lean @@ -0,0 +1,20 @@ +/- +Copyright (c) 2026 Thomas R. Murrills. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Thomas R. Murrills +-/ +module + +public import Lean.Elab.Command +import Mathlib.Lean.Elab.InfoTree + +open Lean Elab + +namespace Mathlib.Tactic + +def workLinter : Linter where + run _ := do + for t in ← getInfoTrees do + let _ := t.getDeclsByBody + +initialize addLinter workLinter From 825f85e483feedfd1a718a897bfcc2905c4d30d8 Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Thu, 26 Mar 2026 16:26:27 -0400 Subject: [PATCH 02/10] chore: docstring --- Mathlib/Tactic/Linter/TestLinter.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/Tactic/Linter/TestLinter.lean b/Mathlib/Tactic/Linter/TestLinter.lean index 2db78bb6cf7bc1..6cdd42e5a21f24 100644 --- a/Mathlib/Tactic/Linter/TestLinter.lean +++ b/Mathlib/Tactic/Linter/TestLinter.lean @@ -12,6 +12,7 @@ open Lean Elab namespace Mathlib.Tactic +/-- Does work. -/ def workLinter : Linter where run _ := do for t in ← getInfoTrees do From 679904569070878edf48c2afdf3f996062a1ac89 Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Thu, 26 Mar 2026 16:41:47 -0400 Subject: [PATCH 03/10] chore: cleanup --- Mathlib/Tactic/Linter/DirectoryDependency.lean | 1 + Mathlib/Tactic/Linter/TestLinter.lean | 2 ++ 2 files changed, 3 insertions(+) diff --git a/Mathlib/Tactic/Linter/DirectoryDependency.lean b/Mathlib/Tactic/Linter/DirectoryDependency.lean index e2c20a79864272..6bf7955d3a8840 100644 --- a/Mathlib/Tactic/Linter/DirectoryDependency.lean +++ b/Mathlib/Tactic/Linter/DirectoryDependency.lean @@ -228,6 +228,7 @@ def allowedImportDirs : NamePrefixRel := .ofArray #[ (`Mathlib.Tactic.Linter.UnusedInstancesInType, `Mathlib.Lean.Expr.Basic), (`Mathlib.Tactic.Linter.UnusedInstancesInType, `Mathlib.Lean.Environment), (`Mathlib.Tactic.Linter.UnusedInstancesInType, `Mathlib.Lean.Elab.InfoTree), + (`Mathlib.Tactic.Linter.TestLinter, `Mathlib.Lean.Environment), (`Mathlib.Tactic.Linter.TestLinter, `Mathlib.Lean.Elab.InfoTree), (`Mathlib.Logic, `Batteries), diff --git a/Mathlib/Tactic/Linter/TestLinter.lean b/Mathlib/Tactic/Linter/TestLinter.lean index 6cdd42e5a21f24..8714112a26c54e 100644 --- a/Mathlib/Tactic/Linter/TestLinter.lean +++ b/Mathlib/Tactic/Linter/TestLinter.lean @@ -8,6 +8,8 @@ module public import Lean.Elab.Command import Mathlib.Lean.Elab.InfoTree +/-! For benching. -/ + open Lean Elab namespace Mathlib.Tactic From b47745c5c24ba8d9cb26a57726ee566d7aa11241 Mon Sep 17 00:00:00 2001 From: thorimur <68410468+thorimur@users.noreply.github.com> Date: Thu, 26 Mar 2026 16:55:45 -0400 Subject: [PATCH 04/10] chore: clean up after mk_all --- Mathlib.lean | 37 ------------------------------------- 1 file changed, 37 deletions(-) diff --git a/Mathlib.lean b/Mathlib.lean index 57d6cfb36cbc77..01e6b903d43b3c 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2,43 +2,6 @@ module -- shake: keep-all public import Std public import Batteries -public import Mathlib.A_Foo.ArrowNatTrans -public import Mathlib.A_Foo.BiCoe -public import Mathlib.A_Foo.DelabAnonConstructor -public import Mathlib.A_Foo.LinterCopies -public import Mathlib.A_Foo.LinterCopiesTest -public import Mathlib.A_Foo.LinterTest -public import Mathlib.A_Foo.MetaUtils -public import Mathlib.A_Foo.NewCat -public import Mathlib.A_Foo.PresheafCopy -public import Mathlib.A_Foo.PrivBar -public import Mathlib.A_Foo.PrivBarImport -public import Mathlib.A_Foo.Santi -public import Mathlib.A_Foo.StrictEquivalence -public import Mathlib.A_Foo.StrictEquivalenceEqToHom -public import Mathlib.A_Foo.StrictEquivalenceTemplate -public import Mathlib.A_Foo.Test.Bar -public import Mathlib.A_Foo.Test.Baz -public import Mathlib.A_Foo.Test.Foo -public import Mathlib.A_Foo.UnusedDecidable -public import Mathlib.A_Foo.UnusedInstancesInTypeCopy -public import Mathlib.A_Foo.fltTest -public import Mathlib.A_Foo.fltTest' -public import Mathlib.A_Foo.getBinders -public import Mathlib.A_Foo.importedModule -public import Mathlib.A_Foo.importingModule -public import Mathlib.A_Foo.loopbug -public import Mathlib.A_Foo.nonunital -public import Mathlib.A_Foo.printAxiomsCheck -public import Mathlib.A_Foo.privmodtest -public import Mathlib.A_Foo.showTasks -public import Mathlib.A_Foo.test -public import Mathlib.A_Foo.test2 -public import Mathlib.A_Foo.testForUIIT -public import Mathlib.A_Foo.traceclassnames -public import Mathlib.A_Foo.vi -public import Mathlib.A_Foo.where -public import Mathlib.A_Foo.«test2 copy» public import Mathlib.Algebra.AddConstMap.Basic public import Mathlib.Algebra.AddConstMap.Equiv public import Mathlib.Algebra.AddTorsor.Basic From 9d7d27597a0d878784f40442a5d66d6455c1acc9 Mon Sep 17 00:00:00 2001 From: thorimur Date: Fri, 27 Mar 2026 17:46:04 -0400 Subject: [PATCH 05/10] chore: bench testing unused --- Mathlib/Tactic/Linter/TestLinter.lean | 42 +++++++++++++++++++++++++-- 1 file changed, 40 insertions(+), 2 deletions(-) diff --git a/Mathlib/Tactic/Linter/TestLinter.lean b/Mathlib/Tactic/Linter/TestLinter.lean index 8714112a26c54e..41ee8087794d62 100644 --- a/Mathlib/Tactic/Linter/TestLinter.lean +++ b/Mathlib/Tactic/Linter/TestLinter.lean @@ -10,14 +10,52 @@ import Mathlib.Lean.Elab.InfoTree /-! For benching. -/ -open Lean Elab +open Lean Elab Command namespace Mathlib.Tactic +/-- +Gets the indices `i` (in ascending order) of the binders of a nested `.forallE`, +`(x₀ : A₀) → (x₁ : A₁) → ⋯ → X`, such that +- `p Aᵢ bi` is `true`, with `bi` the `biinderInfo` +- The rest of the type `(xᵢ₊₁ : Aᵢ₊₁) → ⋯ → X` does not depend on `xᵢ`. (It's in this sense that + `xᵢ : Aᵢ` is "unused".) + +Note that the argument to `p` may have loose bvars. This is a performance optimization. + +This function runs `cleanupAnnotations` on each expression before examining it. + +We see through `let`s, and do not increment the index when doing so. This behavior is compatible +with `forallBoundedTelescope`. +-/ +@[specialize p] +partial def _root_.Lean.Expr.getUnusedForallBinderIdxsWhere + (p : BinderInfo → Expr → Bool) (e : Expr) : Array Nat := + go e 0 #[] +where + /-- Inspects `body`, and if it is a `.forallE` of an instance with type `type` such that `p type` + is `true` and the remainder of the type does not depend on it, pushes the `current` index onto + the accumulated array. -/ + go (body : Expr) (current : Nat) (acc : Array Nat) : Array Nat := + match body.cleanupAnnotations with + | .forallE _ type body bi => go body (current+1) <| + if p bi type && !(body.hasLooseBVar 0) then + acc.push current + else + acc + /- See through `letE`, and just as in the interpretation of a bound provided to + `forallBoundedTelescope`, do not increment the number of binders we've counted. -/ + | .letE _ _ _ body _ => go body current acc + | _ => acc + /-- Does work. -/ def workLinter : Linter where run _ := do for t in ← getInfoTrees do - let _ := t.getDeclsByBody + for n in t.getDeclsByBody do + unless ← liftCoreM <| Meta.isInstance n do continue + let some info := (← getEnv).find? n | continue + let impossibleIdxs := info.type.getUnusedForallBinderIdxsWhere fun bi _ => + !bi.isInstImplicit initialize addLinter workLinter From 2fdc17593fb98a74512f8c4d9a485e20ab949f03 Mon Sep 17 00:00:00 2001 From: thorimur Date: Fri, 27 Mar 2026 19:47:05 -0400 Subject: [PATCH 06/10] chore: bench `has` instead of `get` --- Mathlib/Tactic/Linter/TestLinter.lean | 29 +++++++++------------------ 1 file changed, 10 insertions(+), 19 deletions(-) diff --git a/Mathlib/Tactic/Linter/TestLinter.lean b/Mathlib/Tactic/Linter/TestLinter.lean index 41ee8087794d62..b7e8b210d99500 100644 --- a/Mathlib/Tactic/Linter/TestLinter.lean +++ b/Mathlib/Tactic/Linter/TestLinter.lean @@ -29,24 +29,15 @@ We see through `let`s, and do not increment the index when doing so. This behavi with `forallBoundedTelescope`. -/ @[specialize p] -partial def _root_.Lean.Expr.getUnusedForallBinderIdxsWhere - (p : BinderInfo → Expr → Bool) (e : Expr) : Array Nat := - go e 0 #[] -where - /-- Inspects `body`, and if it is a `.forallE` of an instance with type `type` such that `p type` - is `true` and the remainder of the type does not depend on it, pushes the `current` index onto - the accumulated array. -/ - go (body : Expr) (current : Nat) (acc : Array Nat) : Array Nat := - match body.cleanupAnnotations with - | .forallE _ type body bi => go body (current+1) <| - if p bi type && !(body.hasLooseBVar 0) then - acc.push current - else - acc - /- See through `letE`, and just as in the interpretation of a bound provided to - `forallBoundedTelescope`, do not increment the number of binders we've counted. -/ - | .letE _ _ _ body _ => go body current acc - | _ => acc +partial def _root_.Lean.Expr.hasUnusedForallBinderIdxsWhere + (p : BinderInfo → Expr → Bool) (e : Expr) : Bool := + match e.cleanupAnnotations with + | .forallE _ type body bi => + p bi type && !(body.hasLooseBVar 0) || body.hasUnusedForallBinderIdxsWhere p + /- See through `letE`, and just as in the interpretation of a bound provided to + `forallBoundedTelescope`, do not increment the number of binders we've counted. -/ + | .letE _ _ _ body _ => body.hasUnusedForallBinderIdxsWhere p + | _ => false /-- Does work. -/ def workLinter : Linter where @@ -55,7 +46,7 @@ def workLinter : Linter where for n in t.getDeclsByBody do unless ← liftCoreM <| Meta.isInstance n do continue let some info := (← getEnv).find? n | continue - let impossibleIdxs := info.type.getUnusedForallBinderIdxsWhere fun bi _ => + let impossibleIdxs := info.type.hasUnusedForallBinderIdxsWhere fun bi _ => !bi.isInstImplicit initialize addLinter workLinter From dcca00bd2a8074fb0d807a8ee39f77ff6fb66d55 Mon Sep 17 00:00:00 2001 From: thorimur Date: Fri, 27 Mar 2026 20:11:37 -0400 Subject: [PATCH 07/10] . --- Mathlib/Tactic/Linter/TestLinter.lean | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) diff --git a/Mathlib/Tactic/Linter/TestLinter.lean b/Mathlib/Tactic/Linter/TestLinter.lean index b7e8b210d99500..4f7049e7568192 100644 --- a/Mathlib/Tactic/Linter/TestLinter.lean +++ b/Mathlib/Tactic/Linter/TestLinter.lean @@ -15,18 +15,13 @@ open Lean Elab Command namespace Mathlib.Tactic /-- -Gets the indices `i` (in ascending order) of the binders of a nested `.forallE`, -`(x₀ : A₀) → (x₁ : A₁) → ⋯ → X`, such that -- `p Aᵢ bi` is `true`, with `bi` the `biinderInfo` -- The rest of the type `(xᵢ₊₁ : Aᵢ₊₁) → ⋯ → X` does not depend on `xᵢ`. (It's in this sense that - `xᵢ : Aᵢ` is "unused".) +Tests if any of the binders of `(x₀ : A₀) → (x₁ : A₁) → ⋯ → X` which satisfy `p Aᵢ bi` (with `bi` the `binderInfo`) are unused in the renainder of the type (i.e. in `(xᵢ₊₁ : Aᵢ₊₁) → ⋯ → X`). Note that the argument to `p` may have loose bvars. This is a performance optimization. -This function runs `cleanupAnnotations` on each expression before examining it. +This function runs `cleanupAnnotations` on each type suffix `(xᵢ₊₁ : Aᵢ₊₁) → ⋯ → X` before examining it. -We see through `let`s, and do not increment the index when doing so. This behavior is compatible -with `forallBoundedTelescope`. +We see through `let`s, and do not report if any of them are unused. -/ @[specialize p] partial def _root_.Lean.Expr.hasUnusedForallBinderIdxsWhere @@ -34,8 +29,7 @@ partial def _root_.Lean.Expr.hasUnusedForallBinderIdxsWhere match e.cleanupAnnotations with | .forallE _ type body bi => p bi type && !(body.hasLooseBVar 0) || body.hasUnusedForallBinderIdxsWhere p - /- See through `letE`, and just as in the interpretation of a bound provided to - `forallBoundedTelescope`, do not increment the number of binders we've counted. -/ + /- See through `letE` -/ | .letE _ _ _ body _ => body.hasUnusedForallBinderIdxsWhere p | _ => false From 0b84245581dd6a813d159bab221f6c3cb28501b7 Mon Sep 17 00:00:00 2001 From: thorimur Date: Fri, 27 Mar 2026 20:17:45 -0400 Subject: [PATCH 08/10] chore: try decl ranges --- Mathlib/Tactic/Linter/TestLinter.lean | 35 +++++++++++++++++++++------ 1 file changed, 28 insertions(+), 7 deletions(-) diff --git a/Mathlib/Tactic/Linter/TestLinter.lean b/Mathlib/Tactic/Linter/TestLinter.lean index 4f7049e7568192..25c0e8070a05b7 100644 --- a/Mathlib/Tactic/Linter/TestLinter.lean +++ b/Mathlib/Tactic/Linter/TestLinter.lean @@ -33,14 +33,35 @@ partial def _root_.Lean.Expr.hasUnusedForallBinderIdxsWhere | .letE _ _ _ body _ => body.hasUnusedForallBinderIdxsWhere p | _ => false +#check Nat.lt + +@[inline] protected def _root_.Lean.Position.qlt : Position → Position → Bool + | ⟨l₁, c₁⟩, ⟨l₂, c₂⟩ => l₁.blt l₂ || l₁.beq l₂ && c₁.blt c₂ + +/-- +If `pos` is a `String.Pos`, then `getNamesFrom pos` returns the array of identifiers +for the names of the declarations whose syntax begins in position at least `pos`. +-/ +def getNamesAndRanges {m} [Monad m] [MonadEnv m] [MonadFileMap m] (pos : String.Pos.Raw) : + m (Array Name) := do + -- declarations from parallelism branches should not be interesting here, so use `local` + let drs := declRangeExt.getState (asyncMode := .local) (← getEnv) + let fm ← getFileMap + let pos := fm.toPosition pos + let mut nms := #[] + for (name, { range .. }) in drs do + unless range.pos.qlt pos do + nms := nms.push name + return nms + /-- Does work. -/ def workLinter : Linter where - run _ := do - for t in ← getInfoTrees do - for n in t.getDeclsByBody do - unless ← liftCoreM <| Meta.isInstance n do continue - let some info := (← getEnv).find? n | continue - let impossibleIdxs := info.type.hasUnusedForallBinderIdxsWhere fun bi _ => - !bi.isInstImplicit + run cmd := do + let some pos := cmd.getPos? | return + for n in ← getNamesAndRanges pos do + unless ← liftCoreM <| Meta.isInstance n do continue + let some info := (← getEnv).find? n | continue + let impossibleIdxs := info.type.hasUnusedForallBinderIdxsWhere fun bi _ => + !bi.isInstImplicit initialize addLinter workLinter From cd6c1db02203dfa9872c9bdda3906e4de639658f Mon Sep 17 00:00:00 2001 From: thorimur Date: Fri, 27 Mar 2026 22:06:40 -0400 Subject: [PATCH 09/10] chore: perf? --- Mathlib/Tactic/Linter/TestLinter.lean | 19 ++++++------------- 1 file changed, 6 insertions(+), 13 deletions(-) diff --git a/Mathlib/Tactic/Linter/TestLinter.lean b/Mathlib/Tactic/Linter/TestLinter.lean index 25c0e8070a05b7..37cf4b2cb5b0c9 100644 --- a/Mathlib/Tactic/Linter/TestLinter.lean +++ b/Mathlib/Tactic/Linter/TestLinter.lean @@ -33,8 +33,7 @@ partial def _root_.Lean.Expr.hasUnusedForallBinderIdxsWhere | .letE _ _ _ body _ => body.hasUnusedForallBinderIdxsWhere p | _ => false -#check Nat.lt - +/-- quick lt -/ @[inline] protected def _root_.Lean.Position.qlt : Position → Position → Bool | ⟨l₁, c₁⟩, ⟨l₂, c₂⟩ => l₁.blt l₂ || l₁.beq l₂ && c₁.blt c₂ @@ -42,23 +41,17 @@ partial def _root_.Lean.Expr.hasUnusedForallBinderIdxsWhere If `pos` is a `String.Pos`, then `getNamesFrom pos` returns the array of identifiers for the names of the declarations whose syntax begins in position at least `pos`. -/ -def getNamesAndRanges {m} [Monad m] [MonadEnv m] [MonadFileMap m] (pos : String.Pos.Raw) : - m (Array Name) := do +def getDeclsAfterPos (env : Environment) (map : FileMap) (pos : String.Pos.Raw) : Array Name := -- declarations from parallelism branches should not be interesting here, so use `local` - let drs := declRangeExt.getState (asyncMode := .local) (← getEnv) - let fm ← getFileMap - let pos := fm.toPosition pos - let mut nms := #[] - for (name, { range .. }) in drs do - unless range.pos.qlt pos do - nms := nms.push name - return nms + let pos := map.toPosition pos + declRangeExt.getState (asyncMode := .local) env |>.foldl (init := #[]) + fun acc name { range .. } => if range.pos.qlt pos then acc else acc.push name /-- Does work. -/ def workLinter : Linter where run cmd := do let some pos := cmd.getPos? | return - for n in ← getNamesAndRanges pos do + for n in getDeclsAfterPos (← getEnv) (← getFileMap) pos do unless ← liftCoreM <| Meta.isInstance n do continue let some info := (← getEnv).find? n | continue let impossibleIdxs := info.type.hasUnusedForallBinderIdxsWhere fun bi _ => From f159f244139aaf078ac2422418c3c747b84ea9a7 Mon Sep 17 00:00:00 2001 From: thorimur Date: Fri, 27 Mar 2026 22:31:02 -0400 Subject: [PATCH 10/10] chore: perf? --- Mathlib/Tactic/Linter/TestLinter.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Tactic/Linter/TestLinter.lean b/Mathlib/Tactic/Linter/TestLinter.lean index 37cf4b2cb5b0c9..94bc695e2c2e2d 100644 --- a/Mathlib/Tactic/Linter/TestLinter.lean +++ b/Mathlib/Tactic/Linter/TestLinter.lean @@ -35,7 +35,7 @@ partial def _root_.Lean.Expr.hasUnusedForallBinderIdxsWhere /-- quick lt -/ @[inline] protected def _root_.Lean.Position.qlt : Position → Position → Bool - | ⟨l₁, c₁⟩, ⟨l₂, c₂⟩ => l₁.blt l₂ || l₁.beq l₂ && c₁.blt c₂ + | ⟨l₁, c₁⟩, ⟨l₂, c₂⟩ => l₁ < l₂ || l₁ = l₂ && c₁ < c₂ /-- If `pos` is a `String.Pos`, then `getNamesFrom pos` returns the array of identifiers