From d758328971ce41013e395119e67918443d940005 Mon Sep 17 00:00:00 2001 From: Wojciech Rozowski Date: Fri, 21 Aug 2026 13:47:08 +0000 Subject: [PATCH 1/4] feat: find declaration name inside of linters --- src/Lean/Linter/Util.lean | 14 ++++++++++++++ tests/pkg/module_linter/ModLinter.lean | 11 +++++++++++ tests/pkg/module_linter/ModLinter/Def.lean | 7 +++++++ 3 files changed, 32 insertions(+) diff --git a/src/Lean/Linter/Util.lean b/src/Lean/Linter/Util.lean index a70b19ab8b69..cc69c11eca23 100644 --- a/src/Lean/Linter/Util.lean +++ b/src/Lean/Linter/Util.lean @@ -74,3 +74,17 @@ def getNewDecls (t : InfoTree) : List Name := else acc | _ => acc + +open Elab in +def findMatchingDecl? [Monad m] [MonadInfoTree m] [MonadEnv m] [MonadFileMap m] + (stx : Syntax) : m (Option Name) := do + let some stxRange ← getDeclarationRange? stx | return none + let mut best? : Option (Name × DeclarationRange) := none + for t in ← getInfoTrees do + for declName in getNewDecls t do + let some ranges ← findDeclarationRangesCore? declName | continue + let r := ranges.range + unless !r.pos.lt stxRange.pos && !stxRange.endPos.lt r.endPos do continue + if best?.all fun (_, b) => r.pos.lt b.pos then + best? := some (declName, r) + return best?.map (·.1) diff --git a/tests/pkg/module_linter/ModLinter.lean b/tests/pkg/module_linter/ModLinter.lean index 2a4c4df9531f..dc075bee96c4 100644 --- a/tests/pkg/module_linter/ModLinter.lean +++ b/tests/pkg/module_linter/ModLinter.lean @@ -3,3 +3,14 @@ import ModLinter.Def def a := 1 def b := 2 def c := 3 + +inductive Foo where + | mk : Foo + +mutual + def hello2 : Option Nat := hello1 + partial_fixpoint + + def hello1 : Option Nat := hello2 + partial_fixpoint +end diff --git a/tests/pkg/module_linter/ModLinter/Def.lean b/tests/pkg/module_linter/ModLinter/Def.lean index e9637f1c9061..e6abc2520979 100644 --- a/tests/pkg/module_linter/ModLinter/Def.lean +++ b/tests/pkg/module_linter/ModLinter/Def.lean @@ -1,4 +1,5 @@ import Lean.Elab.Command +import Lean.Linter.Util open Lean Elab Command @@ -7,4 +8,10 @@ def dummyModuleLinter : ModuleLinter where let ref := cmds[0]?.getD .missing logWarningAt ref m!"cmds: {cmds}" +def myLinter : Linter where + run stx := do + if let some decl := (← Linter.findMatchingDecl? stx) then + logInfoAt stx m!"best match is: {decl}" + initialize addModuleLinter dummyModuleLinter +initialize addLinter myLinter From 389672ced559cb6788fea22fcb2d930cc56b8ce9 Mon Sep 17 00:00:00 2001 From: Wojciech Rozowski Date: Thu, 3 Sep 2026 10:43:50 +0000 Subject: [PATCH 2/4] chore: add more tests --- .../find_matching_decl/FindMatchingDecl.lean | 26 +++++++++++++++++++ .../FindMatchingDecl/Linter.lean | 14 ++++++++++ tests/pkg/find_matching_decl/lakefile.toml | 5 ++++ tests/pkg/find_matching_decl/lean-toolchain | 1 + tests/pkg/find_matching_decl/run_test.sh | 15 +++++++++++ tests/pkg/module_linter/ModLinter.lean | 11 -------- tests/pkg/module_linter/ModLinter/Def.lean | 7 ----- 7 files changed, 61 insertions(+), 18 deletions(-) create mode 100644 tests/pkg/find_matching_decl/FindMatchingDecl.lean create mode 100644 tests/pkg/find_matching_decl/FindMatchingDecl/Linter.lean create mode 100644 tests/pkg/find_matching_decl/lakefile.toml create mode 100644 tests/pkg/find_matching_decl/lean-toolchain create mode 100755 tests/pkg/find_matching_decl/run_test.sh diff --git a/tests/pkg/find_matching_decl/FindMatchingDecl.lean b/tests/pkg/find_matching_decl/FindMatchingDecl.lean new file mode 100644 index 000000000000..d00757820fa9 --- /dev/null +++ b/tests/pkg/find_matching_decl/FindMatchingDecl.lean @@ -0,0 +1,26 @@ +import FindMatchingDecl.Linter + +/-! Declarations of various shapes for `Linter.findMatchingDecl?` to match: plain definitions, +an inductive, a mutual block whose definitions are compiled via `partial_fixpoint`, a class, +and an anonymous instance. -/ + +def a := 1 +def b := 2 +def c := 3 + +inductive Foo where + | mk : Foo + +mutual + def hello2 : Option Nat := hello1 + partial_fixpoint + + def hello1 : Option Nat := hello2 + partial_fixpoint +end + +class Magma (carrier : Type u) where + op : carrier → carrier → carrier + +instance : Magma Nat where + op := (· + ·) diff --git a/tests/pkg/find_matching_decl/FindMatchingDecl/Linter.lean b/tests/pkg/find_matching_decl/FindMatchingDecl/Linter.lean new file mode 100644 index 000000000000..66efbf4769c5 --- /dev/null +++ b/tests/pkg/find_matching_decl/FindMatchingDecl/Linter.lean @@ -0,0 +1,14 @@ +import Lean.Elab.Command +import Lean.Linter.Util + +/-! A linter that reports the declaration `Linter.findMatchingDecl?` associates with each +command it runs on. -/ + +open Lean Elab Command + +def matchingDeclLinter : Linter where + run stx := do + if let some decl := (← Linter.findMatchingDecl? stx) then + logInfoAt stx m!"best match is: {decl}" + +initialize addLinter matchingDeclLinter diff --git a/tests/pkg/find_matching_decl/lakefile.toml b/tests/pkg/find_matching_decl/lakefile.toml new file mode 100644 index 000000000000..d83573854699 --- /dev/null +++ b/tests/pkg/find_matching_decl/lakefile.toml @@ -0,0 +1,5 @@ +name = "find_matching_decl" +defaultTargets = ["FindMatchingDecl"] + +[[lean_lib]] +name = "FindMatchingDecl" diff --git a/tests/pkg/find_matching_decl/lean-toolchain b/tests/pkg/find_matching_decl/lean-toolchain new file mode 100644 index 000000000000..d55e55c3660e --- /dev/null +++ b/tests/pkg/find_matching_decl/lean-toolchain @@ -0,0 +1 @@ +../../../build/release/stage1 diff --git a/tests/pkg/find_matching_decl/run_test.sh b/tests/pkg/find_matching_decl/run_test.sh new file mode 100755 index 000000000000..2c80d72e1bf8 --- /dev/null +++ b/tests/pkg/find_matching_decl/run_test.sh @@ -0,0 +1,15 @@ +rm -rf .lake + +# Build the library; the linter registered in `FindMatchingDecl.Linter` runs on each +# command of `FindMatchingDecl` and reports the declaration `findMatchingDecl?` picks. +capture lake build + +check_out_contains "FindMatchingDecl.lean:7:0: best match is: a" +check_out_contains "FindMatchingDecl.lean:8:0: best match is: b" +check_out_contains "FindMatchingDecl.lean:9:0: best match is: c" +check_out_contains "FindMatchingDecl.lean:11:0: best match is: Foo" +# The whole `mutual` command resolves to the earliest declaration in the block. +check_out_contains "FindMatchingDecl.lean:14:0: best match is: hello2" +check_out_contains "FindMatchingDecl.lean:22:0: best match is: Magma" +# An anonymous instance resolves to its generated name. +check_out_contains "FindMatchingDecl.lean:25:0: best match is: instMagmaNat" diff --git a/tests/pkg/module_linter/ModLinter.lean b/tests/pkg/module_linter/ModLinter.lean index dc075bee96c4..2a4c4df9531f 100644 --- a/tests/pkg/module_linter/ModLinter.lean +++ b/tests/pkg/module_linter/ModLinter.lean @@ -3,14 +3,3 @@ import ModLinter.Def def a := 1 def b := 2 def c := 3 - -inductive Foo where - | mk : Foo - -mutual - def hello2 : Option Nat := hello1 - partial_fixpoint - - def hello1 : Option Nat := hello2 - partial_fixpoint -end diff --git a/tests/pkg/module_linter/ModLinter/Def.lean b/tests/pkg/module_linter/ModLinter/Def.lean index e6abc2520979..e9637f1c9061 100644 --- a/tests/pkg/module_linter/ModLinter/Def.lean +++ b/tests/pkg/module_linter/ModLinter/Def.lean @@ -1,5 +1,4 @@ import Lean.Elab.Command -import Lean.Linter.Util open Lean Elab Command @@ -8,10 +7,4 @@ def dummyModuleLinter : ModuleLinter where let ref := cmds[0]?.getD .missing logWarningAt ref m!"cmds: {cmds}" -def myLinter : Linter where - run stx := do - if let some decl := (← Linter.findMatchingDecl? stx) then - logInfoAt stx m!"best match is: {decl}" - initialize addModuleLinter dummyModuleLinter -initialize addLinter myLinter From 4f363e7db5a66753cd44df334b333de961365da4 Mon Sep 17 00:00:00 2001 From: Wojciech Rozowski Date: Thu, 3 Sep 2026 12:26:32 +0000 Subject: [PATCH 3/4] chore: add helpers for finding code quality source out of syntax --- src/Lean/Linter/Util.lean | 16 ++++++++++++++-- .../pkg/find_matching_decl/FindMatchingDecl.lean | 3 +++ .../FindMatchingDecl/Linter.lean | 7 ++++++- tests/pkg/find_matching_decl/run_test.sh | 9 +++++++++ 4 files changed, 32 insertions(+), 3 deletions(-) diff --git a/src/Lean/Linter/Util.lean b/src/Lean/Linter/Util.lean index cc69c11eca23..0a78c2beceea 100644 --- a/src/Lean/Linter/Util.lean +++ b/src/Lean/Linter/Util.lean @@ -9,12 +9,12 @@ prelude public import Lean.Server.InfoUtils public import Lean.Linter.Init public import Lean.Elab.Term - +public import Lean.Linter.CodeQuality.Basic public section namespace Lean.Linter -open Lean.Elab +open Lean.Elab CodeQuality /-- Go upwards through the given `tree` starting from the smallest node that contains the given `range` and collect all `MacroExpansionInfo`s on the way up. @@ -88,3 +88,15 @@ def findMatchingDecl? [Monad m] [MonadInfoTree m] [MonadEnv m] [MonadFileMap m] if best?.all fun (_, b) => r.pos.lt b.pos then best? := some (declName, r) return best?.map (·.1) + + +def findCodeQualitySource? [Monad m] [MonadInfoTree m] [MonadEnv m] [MonadFileMap m] + (stx : Syntax) : m (Option Source) := do + let some name ← findMatchingDecl? stx | return none + return some (.declaration (← getEnv).mainModule name) + +def findCodeQualitySource [Monad m] [MonadInfoTree m] [MonadEnv m] [MonadFileMap m] + (stx : Syntax) : m Source := do + match ← findMatchingDecl? stx with + | some name => return .declaration (← getEnv).mainModule name + | none => return .module (← getEnv).mainModule diff --git a/tests/pkg/find_matching_decl/FindMatchingDecl.lean b/tests/pkg/find_matching_decl/FindMatchingDecl.lean index d00757820fa9..ac3e8023c1ab 100644 --- a/tests/pkg/find_matching_decl/FindMatchingDecl.lean +++ b/tests/pkg/find_matching_decl/FindMatchingDecl.lean @@ -24,3 +24,6 @@ class Magma (carrier : Type u) where instance : Magma Nat where op := (· + ·) + +-- A command with no matching declaration: `findCodeQualitySource` falls back to the module. +#check Nat diff --git a/tests/pkg/find_matching_decl/FindMatchingDecl/Linter.lean b/tests/pkg/find_matching_decl/FindMatchingDecl/Linter.lean index 66efbf4769c5..25a2f0cab977 100644 --- a/tests/pkg/find_matching_decl/FindMatchingDecl/Linter.lean +++ b/tests/pkg/find_matching_decl/FindMatchingDecl/Linter.lean @@ -2,7 +2,8 @@ import Lean.Elab.Command import Lean.Linter.Util /-! A linter that reports the declaration `Linter.findMatchingDecl?` associates with each -command it runs on. -/ +command it runs on, and the code-quality source derived from it by +`Linter.findCodeQualitySource` and `Linter.findCodeQualitySource?`. -/ open Lean Elab Command @@ -10,5 +11,9 @@ def matchingDeclLinter : Linter where run stx := do if let some decl := (← Linter.findMatchingDecl? stx) then logInfoAt stx m!"best match is: {decl}" + let src ← Linter.findCodeQualitySource stx + let src? ← Linter.findCodeQualitySource? stx + -- `compress` keeps each message on one line so the test can grep for it + logInfoAt stx m!"source: {(toJson src).compress}; source?: {(toJson src?).compress}" initialize addLinter matchingDeclLinter diff --git a/tests/pkg/find_matching_decl/run_test.sh b/tests/pkg/find_matching_decl/run_test.sh index 2c80d72e1bf8..4e60548807e2 100755 --- a/tests/pkg/find_matching_decl/run_test.sh +++ b/tests/pkg/find_matching_decl/run_test.sh @@ -13,3 +13,12 @@ check_out_contains "FindMatchingDecl.lean:14:0: best match is: hello2" check_out_contains "FindMatchingDecl.lean:22:0: best match is: Magma" # An anonymous instance resolves to its generated name. check_out_contains "FindMatchingDecl.lean:25:0: best match is: instMagmaNat" + +# Commands inside a declaration yield a declaration source, in both variants. +check_out_contains 'FindMatchingDecl.lean:7:0: source: {"declaration":{"module":"FindMatchingDecl","name":"a"}}; source?: {"declaration":{"module":"FindMatchingDecl","name":"a"}}' +check_out_contains 'FindMatchingDecl.lean:14:0: source: {"declaration":{"module":"FindMatchingDecl","name":"hello2"}}' +check_out_contains 'FindMatchingDecl.lean:25:0: source: {"declaration":{"module":"FindMatchingDecl","name":"instMagmaNat"}}' +# The module docstring and `#check` match no declaration: the total variant falls back to the +# module source while the optional variant returns `none`. +check_out_contains 'FindMatchingDecl.lean:3:0: source: {"module":{"name":"FindMatchingDecl"}}; source?: null' +check_out_contains 'FindMatchingDecl.lean:30:0: source: {"module":{"name":"FindMatchingDecl"}}; source?: null' From c6b72498f5f5f0f4a92686ccb9881736fda4e406 Mon Sep 17 00:00:00 2001 From: Wojciech Rozowski Date: Thu, 3 Sep 2026 12:41:00 +0000 Subject: [PATCH 4/4] chore: cleanup --- src/Lean/Linter/Util.lean | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/src/Lean/Linter/Util.lean b/src/Lean/Linter/Util.lean index 0a78c2beceea..fae77aa38046 100644 --- a/src/Lean/Linter/Util.lean +++ b/src/Lean/Linter/Util.lean @@ -10,6 +10,7 @@ public import Lean.Server.InfoUtils public import Lean.Linter.Init public import Lean.Elab.Term public import Lean.Linter.CodeQuality.Basic + public section namespace Lean.Linter @@ -75,7 +76,13 @@ def getNewDecls (t : InfoTree) : List Name := acc | _ => acc -open Elab in +/-- Find the declaration in the current file that `stx` belongs to. + +Searches the info trees of the current command for declarations (see `getNewDecls`) whose +declaration range contains the range of `stx`, and returns the one whose range starts earliest. +Returns `none` if `stx` has no position or no declaration's range contains it (e.g. for commands +such as `#check` or `open`). +-/ def findMatchingDecl? [Monad m] [MonadInfoTree m] [MonadEnv m] [MonadFileMap m] (stx : Syntax) : m (Option Name) := do let some stxRange ← getDeclarationRange? stx | return none @@ -89,12 +96,15 @@ def findMatchingDecl? [Monad m] [MonadInfoTree m] [MonadEnv m] [MonadFileMap m] best? := some (declName, r) return best?.map (·.1) - +/-- Build a code-quality `Source` attributing `stx` to the declaration it belongs to +(see `findMatchingDecl?`), or `none` if no declaration matches. -/ def findCodeQualitySource? [Monad m] [MonadInfoTree m] [MonadEnv m] [MonadFileMap m] (stx : Syntax) : m (Option Source) := do let some name ← findMatchingDecl? stx | return none return some (.declaration (← getEnv).mainModule name) +/-- Build a code-quality `Source` attributing `stx` to the declaration it belongs to +(see `findMatchingDecl?`), falling back to the current module if no declaration matches. -/ def findCodeQualitySource [Monad m] [MonadInfoTree m] [MonadEnv m] [MonadFileMap m] (stx : Syntax) : m Source := do match ← findMatchingDecl? stx with