test: improve language server test coverage (#10574)

This PR significantly improves the test coverage of the language server,
providing at least a single basic test for every request that is used by
the client. It also implements infrastructure for testing all of these
requests, e.g. the ability to run interactive tests in a project context
and refactors the interactive test runner to be more maintainable.
Finally, it also fixes a small bug with the recently implemented unknown
identifier code actions for auto-implicits (#10442) that was discovered
in testing, where the "import all unambiguous unknown identifiers" code
action didn't work correctly on auto-implicit identifiers.

Author: mhuisi

doc/dev/testing.md

@@ -59,7 +59,7 @@ All these tests are included by [src/shell/CMakeLists.txt](https://github.com/le
     open Foo in
     theorem tst2 (h : a ≤ b) : a + 2 ≤ b + 2 :=
     Bla.
-      --^ textDocument/completion
+      --^ completion
     ```
     In this example, the test driver [`test_single.sh`](https://github.com/leanprover/lean4/tree/master/tests/lean/interactive/test_single.sh) will simulate an
     auto-completion request at `Bla.`. The expected output is stored in

src/CMakeLists.txt

@@ -797,6 +797,9 @@ install(DIRECTORY "${CMAKE_BINARY_DIR}/lib/" DESTINATION lib
 
 # symlink source into expected installation location for go-to-definition, if file system allows it
 file(MAKE_DIRECTORY ${CMAKE_BINARY_DIR}/src)
+# get rid of all files in `src/lean` that may have been loaded from the cache
+# (at the time of writing this, this is the case for some lake test .c files)
+file(REMOVE_RECURSE ${CMAKE_BINARY_DIR}/src/lean)
 if(${STAGE} EQUAL 0)
   file(CREATE_LINK ${CMAKE_SOURCE_DIR}/../../src ${CMAKE_BINARY_DIR}/src/lean RESULT _IGNORE_RES SYMBOLIC)
 else()

src/Init/Notation.lean

@@ -643,7 +643,7 @@ applications of this function as `↑` when printing expressions.
 syntax (name := Attr.coe) "coe" : attr
 
 /--
-This attribute marks a code action, which is used to suggest new tactics or replace existing ones.
+This attribute marks a code action that triggers on specific commands.
 
 * `@[command_code_action kind]`: This is a code action which applies to applications of the command
   `kind` (a command syntax kind), which can replace the command or insert things before or after it.

src/Lean/Data/Lsp/Ipc.lean

@@ -13,6 +13,7 @@ public import Lean.Data.Lsp.Communication
 public import Lean.Data.Lsp.Diagnostics
 public import Lean.Data.Lsp.Extra
 import Init.Data.List.Sort.Basic
+public import Lean.Data.Lsp.LanguageFeatures
 
 public section
 
@@ -160,10 +161,191 @@ where
       | Except.error inner => throw $ userError s!"Cannot decode publishDiagnostics parameters\n{inner}"
     | _ => loop
 
-def runWith (lean : System.FilePath) (args : Array String := #[]) (test : IpcM α) : IO α := do
+structure CallHierarchy where
+  item       : CallHierarchyItem
+  fromRanges : Array Range
+  children   : Array CallHierarchy
+  deriving FromJson, ToJson
+
+partial def expandIncomingCallHierarchy (requestNo : Nat) (uri : DocumentUri) (pos : Lsp.Position) : IpcM (Array CallHierarchy × Nat) := do
+  writeRequest {
+    id := requestNo
+    method := "textDocument/prepareCallHierarchy"
+    param := {
+      textDocument := { uri }
+      position := pos
+      : CallHierarchyPrepareParams
+    }
+  }
+  let r ← readResponseAs requestNo (Option (Array CallHierarchyItem))
+  let mut requestNo := requestNo + 1
+  let roots := r.result.getD #[]
+  let mut hierarchies := #[]
+  for root in roots do
+    let (hierarchy, rootRequestNo) ← go requestNo root #[] {}
+    requestNo := rootRequestNo
+    hierarchies := hierarchies.push hierarchy
+  return (hierarchies, requestNo)
+where
+  go (requestNo : Nat) (item : CallHierarchyItem) (fromRanges : Array Range) (visited : Std.TreeSet String) : IpcM (CallHierarchy × Nat) := do
+    if visited.contains item.name then
+      return ({ item, fromRanges := #[], children := #[] }, requestNo)
+    writeRequest {
+      id := requestNo
+      method := "callHierarchy/incomingCalls"
+      param := {
+        item
+        : CallHierarchyIncomingCallsParams
+      }
+    }
+    let r ← readResponseAs requestNo (Option (Array CallHierarchyIncomingCall))
+    let visited : Std.TreeSet String := visited.insert item.name
+    let mut requestNo := requestNo + 1
+    let children := r.result.getD #[]
+    let mut childHierarchies := #[]
+    for c in children do
+      let (childHierarchy, childRequestNo) ← go requestNo c.from c.fromRanges visited
+      childHierarchies := childHierarchies.push childHierarchy
+      requestNo := childRequestNo
+    return ({ item, fromRanges, children := childHierarchies }, requestNo)
+
+partial def expandOutgoingCallHierarchy (requestNo : Nat) (uri : DocumentUri) (pos : Lsp.Position) : IpcM (Array CallHierarchy × Nat) := do
+  writeRequest {
+    id := requestNo
+    method := "textDocument/prepareCallHierarchy"
+    param := {
+      textDocument := { uri }
+      position := pos
+      : CallHierarchyPrepareParams
+    }
+  }
+  let r ← readResponseAs requestNo (Option (Array CallHierarchyItem))
+  let mut requestNo := requestNo + 1
+  let roots := r.result.getD #[]
+  let mut hierarchies := #[]
+  for root in roots do
+    let (hierarchy, rootRequestNo) ← go requestNo root #[] {}
+    requestNo := rootRequestNo
+    hierarchies := hierarchies.push hierarchy
+  return (hierarchies, requestNo)
+where
+  go (requestNo : Nat) (item : CallHierarchyItem) (fromRanges : Array Range) (visited : Std.TreeSet String) : IpcM (CallHierarchy × Nat) := do
+    if visited.contains item.name then
+      return ({ item, fromRanges := #[], children := #[] }, requestNo)
+    writeRequest {
+      id := requestNo
+      method := "callHierarchy/outgoingCalls"
+      param := {
+        item
+        : CallHierarchyOutgoingCallsParams
+      }
+    }
+    let r ← readResponseAs requestNo (Option (Array CallHierarchyOutgoingCall))
+    let visited : Std.TreeSet String := visited.insert item.name
+    let mut requestNo := requestNo + 1
+    let children := r.result.getD #[]
+    let mut childHierarchies := #[]
+    for c in children do
+      let (childHierarchy, childRequestNo) ← go requestNo c.to c.fromRanges visited
+      childHierarchies := childHierarchies.push childHierarchy
+      requestNo := childRequestNo
+    return ({ item, fromRanges, children := childHierarchies }, requestNo)
+
+structure ModuleHierarchy where
+  item : LeanImport
+  children : Array ModuleHierarchy
+  deriving FromJson, ToJson
+
+partial def expandModuleHierarchyImports (requestNo : Nat) (uri : DocumentUri) : IpcM (Option ModuleHierarchy × Nat) := do
+  writeRequest {
+    id := requestNo
+    method := "$/lean/prepareModuleHierarchy"
+    param := {
+      textDocument := { uri }
+      : LeanPrepareModuleHierarchyParams
+    }
+  }
+  let r ← readResponseAs requestNo (Option LeanModule)
+  let mut requestNo := requestNo + 1
+  let some root := r.result
+    | return (none, requestNo)
+  let root := {
+    module := root
+    kind := { isAll := false, isPrivate := false, metaKind := .full }
+  }
+  let (hierarchy, rootRequestNo) ← go requestNo root {}
+  requestNo := rootRequestNo
+  return (hierarchy, requestNo)
+where
+  go (requestNo : Nat) (item : LeanImport) (visited : Std.TreeSet String) : IpcM (ModuleHierarchy × Nat) := do
+    if visited.contains item.module.name then
+      return ({ item, children := #[] }, requestNo)
+    writeRequest {
+      id := requestNo
+      method := "$/lean/moduleHierarchy/imports"
+      param := {
+        module := item.module
+        : LeanModuleHierarchyImportsParams
+      }
+    }
+    let r ← readResponseAs requestNo (Array LeanImport)
+    let visited : Std.TreeSet String := visited.insert item.module.name
+    let mut requestNo := requestNo + 1
+    let children := r.result
+    let mut childHierarchies := #[]
+    for c in children do
+      let (childHierarchy, childRequestNo) ← go requestNo c visited
+      childHierarchies := childHierarchies.push childHierarchy
+      requestNo := childRequestNo
+    return ({ item, children := childHierarchies }, requestNo)
+
+partial def expandModuleHierarchyImportedBy (requestNo : Nat) (uri : DocumentUri) : IpcM (Option ModuleHierarchy × Nat) := do
+  writeRequest {
+    id := requestNo
+    method := "$/lean/prepareModuleHierarchy"
+    param := {
+      textDocument := { uri }
+      : LeanPrepareModuleHierarchyParams
+    }
+  }
+  let r ← readResponseAs requestNo (Option LeanModule)
+  let mut requestNo := requestNo + 1
+  let some root := r.result
+    | return (none, requestNo)
+  let root := {
+    module := root
+    kind := { isAll := false, isPrivate := false, metaKind := .full }
+  }
+  let (hierarchy, rootRequestNo) ← go requestNo root {}
+  requestNo := rootRequestNo
+  return (hierarchy, requestNo)
+where
+  go (requestNo : Nat) (item : LeanImport) (visited : Std.TreeSet String) : IpcM (ModuleHierarchy × Nat) := do
+    if visited.contains item.module.name then
+      return ({ item, children := #[] }, requestNo)
+    writeRequest {
+      id := requestNo
+      method := "$/lean/moduleHierarchy/importedBy"
+      param := {
+        module := item.module
+        : LeanModuleHierarchyImportedByParams
+      }
+    }
+    let r ← readResponseAs requestNo (Array LeanImport)
+    let visited : Std.TreeSet String := visited.insert item.module.name
+    let mut requestNo := requestNo + 1
+    let children := r.result
+    let mut childHierarchies := #[]
+    for c in children do
+      let (childHierarchy, childRequestNo) ← go requestNo c visited
+      childHierarchies := childHierarchies.push childHierarchy
+      requestNo := childRequestNo
+    return ({ item, children := childHierarchies }, requestNo)
+
+def runWith (lean : String) (args : Array String := #[]) (test : IpcM α) : IO α := do
   let proc ← Process.spawn {
     toStdioConfig := ipcStdioConfig
-    cmd := lean.toString
+    cmd := lean
     args := args }
   ReaderT.run test proc
 

src/Lean/Elab/GuardMsgs.lean

@@ -235,7 +235,7 @@ def guardMsgsCodeAction : CommandCodeAction := fun _ _ _ node => do
   let some (stx, res) := res | return #[]
   let doc ← readDoc
   let eager := {
-    title := "Update #guard_msgs with tactic output"
+    title := "Update #guard_msgs with generated message"
     kind? := "quickfix"
     isPreferred? := true
   }

src/Lean/Server/CodeActions/Attr.lean

@@ -17,9 +17,6 @@ public section
 * Attribute `@[hole_code_action]` collects code actions which will be called
   on each occurrence of a hole (`_`, `?_` or `sorry`).
 
-* Attribute `@[tactic_code_action]` collects code actions which will be called
-  on each occurrence of a tactic.
-
 * Attribute `@[command_code_action]` collects code actions which will be called
   on each occurrence of a command.
 -/

src/Lean/Server/CodeActions/UnknownIdentifier.lean

@@ -20,6 +20,18 @@ namespace Lean.Server.FileWorker
 open Lean.Lsp
 open Lean.Server.Completion
 
+private def compareRanges (r1 r2 : String.Range) : Ordering :=
+  if r1.start < r2.start then
+    .lt
+  else if r1.start > r2.start then
+    .gt
+  else if r1.stop < r2.stop then
+    .lt
+  else if r1.stop > r2.stop then
+    .gt
+  else
+    .eq
+
 def waitUnknownIdentifierRanges (doc : EditableDocument) (requestedRange : String.Range)
     : BaseIO (Array String.Range × Bool) := do
   let text := doc.meta.text
@@ -37,32 +49,46 @@ def waitUnknownIdentifierRanges (doc : EditableDocument) (requestedRange : Strin
       continue
     ranges := ranges.push msgRange
   let isAnyUnknownIdentifierMessage := ! ranges.isEmpty
-  let autoImplicitUsages := tree.foldInfosInRange requestedRange #[] fun ctx i acc => Id.run do
-    let .ofTermInfo ti := i
-      | return acc
-    let some r := ti.stx.getRange? (canonicalOnly := true)
-      | return acc
-    if ! ti.expr.isFVar then
-      return acc
-    if ! ctx.autoImplicits.contains ti.expr then
-      return acc
-    return acc.push r
-  let autoImplicitUsages := autoImplicitUsages.get
+  let autoImplicitUsages : ServerTask (Std.TreeSet String.Range compareRanges) :=
+    tree.foldInfosInRange requestedRange ∅ fun ctx i acc => Id.run do
+      let .ofTermInfo ti := i
+        | return acc
+      let some r := ti.stx.getRange? (canonicalOnly := true)
+        | return acc
+      if ! ti.expr.isFVar then
+        return acc
+      if ! ctx.autoImplicits.contains ti.expr then
+        return acc
+      return acc.insert r
+  let autoImplicitUsages := autoImplicitUsages.get.toArray
   ranges := ranges ++ autoImplicitUsages
   return (ranges, isAnyUnknownIdentifierMessage)
 
 def waitAllUnknownIdentifierMessageRanges (doc : EditableDocument)
     : BaseIO (Array String.Range) := do
   let text := doc.meta.text
-  let msgLog : MessageLog := Language.toSnapshotTree doc.initSnap
-    |>.getAll.map (·.diagnostics.msgLog)
-    |>.foldl (· ++ ·) {}
+  let snaps := Language.toSnapshotTree doc.initSnap |>.getAll
+  let msgLog : MessageLog := snaps.map (·.diagnostics.msgLog) |>.foldl (· ++ ·) {}
   let mut ranges := #[]
   for msg in msgLog.unreported do
     if ! msg.data.hasTag (· == unknownIdentifierMessageTag) then
       continue
     let msgRange : String.Range := ⟨text.ofPosition msg.pos, text.ofPosition <| msg.endPos.getD msg.pos⟩
     ranges := ranges.push msgRange
+  let (cmdSnaps, _) := doc.cmdSnaps.waitAll.get
+  for snap in cmdSnaps do
+    let autoImplicitUsages : Std.TreeSet String.Range compareRanges :=
+      snap.infoTree.foldInfo (init := ∅) fun ctx i acc => Id.run do
+        let .ofTermInfo ti := i
+          | return acc
+        let some r := ti.stx.getRange? (canonicalOnly := true)
+          | return acc
+        if ! ti.expr.isFVar then
+          return acc
+        if ! ctx.autoImplicits.contains ti.expr then
+          return acc
+        return acc.insert r
+    ranges := ranges ++ autoImplicitUsages.toArray
   return ranges
 
 structure Insertion where

src/Lean/Server/Test.lean

@@ -9,5 +9,6 @@ module
 prelude
 public import Lean.Server.Test.Cancel
 public import Lean.Server.Test.Runner
+public import Lean.Server.Test.Refs
 
 public section

src/Lean/Server/Test/Refs.lean

@@ -0,0 +1,27 @@
+/-
+Copyright (c) 2025 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: Marc Huisinga
+-/
+module
+
+prelude
+import Init.Prelude
+
+public def LeanServerTestRefsTest0 := Nat
+
+namespace Lean.Server.Test.Refs
+
+public def Test1 := Nat
+public def Test2 := Test1
+public def Test3 := Test1
+public def Test4 := Test2
+public def Test5 := Test2
+
+public inductive Test6
+  | mk
+public def test7 : Test6 := .mk
+public def test8 : Test6 := .mk
+public def test9 := test7
+public def test10 := test9