feat: make go-to-definition on a typeclass projection application go to the instance(s) (#1767)

2023-01-19 01:10:01 -08:00 · 2023-01-19 01:10:01 -08:00 · 561e404fe4
commit 561e404fe4
parent 600758ba49
9 changed files with 281 additions and 45 deletions
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@ -66,11 +66,11 @@ def handleHover (p : HoverParams)
        | none => pure none

      -- now try info tree
-      if let some (ci, i) := snap.infoTree.hoverableInfoAt? hoverPos then
-        if let some range := i.range? then
+      if let some ictx := snap.infoTree.hoverableInfoAt? hoverPos then
+        if let some range := ictx.info.range? then
          -- prefer info tree if at least as specific as parser docstring
          if stxDoc?.all fun (_, stxRange) => stxRange.includes range then
-            if let some hoverFmt ← i.fmtHover? ci then
+            if let some hoverFmt ← ictx.info.fmtHover? ictx.ctx then
              return mkHover (toString hoverFmt.fmt) range

      if let some (doc, range) := stxDoc? then
@ -79,7 +79,7 @@ def handleHover (p : HoverParams)
      return none

 open Elab GoToKind in
-def locationLinksOfInfo (kind : GoToKind) (ci : Elab.ContextInfo) (i : Elab.Info)
+def locationLinksOfInfo (kind : GoToKind) (ictx : InfoWithCtx)
    (infoTree? : Option InfoTree := none) : RequestM (Array LocationLink) := do
  let rc ← read
  let doc ← readDoc
@ -116,6 +116,9 @@ def locationLinksOfInfo (kind : GoToKind) (ci : Elab.ContextInfo) (i : Elab.Info
      return #[ll]
    return #[]

+  let i := ictx.info
+  let ci := ictx.ctx
+  let children := ictx.children
  match i with
  | .ofTermInfo ti =>
    let mut expr := ti.expr
@ -126,6 +129,43 @@ def locationLinksOfInfo (kind : GoToKind) (ci : Elab.ContextInfo) (i : Elab.Info
    | Expr.const n .. => return ← ci.runMetaM i.lctx <| locationLinksFromDecl i n
    | Expr.fvar id .. => return ← ci.runMetaM i.lctx <| locationLinksFromBinder i id
    | _ => pure ()
+
+    -- Check whether this `TermInfo` node is directly responsible for its `.expr`.
+    -- This is the case iff all of its children represent strictly smaller subexpressions;
+    -- it is sufficient to check this of all direct children of this node (and that its elaborator didn't expand it as a macro)
+    let isExprGenerator := children.all fun
+      | .node (Info.ofTermInfo info) _ => info.expr != expr
+      | .node (Info.ofMacroExpansionInfo _) _ => false
+      | _ => true
+
+    -- don't go-to-instance if this `TermInfo` didn't directly generate its `.expr`
+    if kind != declaration && isExprGenerator then
+      -- go-to-definition on a projection application of a typeclass
+      -- should return all instances generated by TC
+      expr ← ci.runMetaM i.lctx do instantiateMVars expr
+      if let .const n _ := expr.getAppFn then
+        -- also include constant along with instance results
+        let mut results ← ci.runMetaM i.lctx <| locationLinksFromDecl i n
+        if let some info := ci.env.getProjectionFnInfo? n then
+          let mut elaborators := default
+          if let some ei := i.toElabInfo? then do
+            -- also include elaborator along with instance results, as this wouldn't be accessible otherwise
+            if ei.elaborator != `Delab -- prevent an error if this `TermInfo` came from the infoview
+              && ei.elaborator != `Lean.Elab.Term.elabApp && ei.elaborator != `Lean.Elab.Term.elabIdent -- don't include trivial elaborators
+              then do
+              elaborators ← ci.runMetaM i.lctx <| locationLinksFromDecl i ei.elaborator
+          let instIdx := info.numParams
+          let appArgs := expr.getAppArgs
+          let rec extractInstances : Expr → RequestM (Array Name)
+            | .const declName _ => do
+              if ← ci.runMetaM i.lctx do Lean.Meta.isInstance declName then pure #[declName] else pure #[]
+            | .app fn arg => do pure $ (← extractInstances fn).append (← extractInstances arg)
+            | _ => pure #[]
+          if let some instArg := appArgs.get? instIdx then
+            for inst in (← extractInstances instArg) do
+              results := results.append (← ci.runMetaM i.lctx <| locationLinksFromDecl i inst)
+            results := results.append elaborators -- put elaborators at the end of the results
+        return results
  | .ofFieldInfo fi =>
    if kind == type then
      let expr ← ci.runMetaM i.lctx do
@ -157,8 +197,8 @@ def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)

  withWaitFindSnap doc (fun s => s.endPos > hoverPos)
    (notFoundX := pure #[]) fun snap => do
-      if let some (ci, i) := snap.infoTree.hoverableInfoAt? (includeStop := true /- #767 -/) hoverPos then
-        locationLinksOfInfo kind ci i snap.infoTree
+      if let some infoWithCtx := snap.infoTree.hoverableInfoAt? (omitIdentApps := true) (includeStop := true /- #767 -/) hoverPos then
+        locationLinksOfInfo kind infoWithCtx snap.infoTree
      else return #[]

 open RequestM in
@ -214,7 +254,7 @@ def getInteractiveTermGoal (p : Lsp.PlainTermGoalParams)
  let hoverPos := text.lspPosToUtf8Pos p.position
  withWaitFindSnap doc (fun s => s.endPos > hoverPos)
    (notFoundX := pure none) fun snap => do
-      if let some (ci, i@(Elab.Info.ofTermInfo ti)) := snap.infoTree.termGoalAt? hoverPos then
+      if let some {ctx := ci, info := i@(Elab.Info.ofTermInfo ti), ..} := snap.infoTree.termGoalAt? hoverPos then
        let ty ← ci.runMetaM i.lctx do
          instantiateMVars <| ti.expectedType?.getD (← Meta.inferType ti.expr)
        -- for binders, hide the last hypothesis (the binder itself)
--- a/src/Lean/Server/FileWorker/WidgetRequests.lean
+++ b/src/Lean/Server/FileWorker/WidgetRequests.lean
@ -15,7 +15,7 @@ import Lean.Server.FileWorker.RequestHandling
 /-! Registers all widget-related RPC procedures. -/

 namespace Lean.Widget
-open Server
+open Server Lean.Elab

 structure MsgToInteractive where
  msg : WithRpcRef MessageData
@ -127,7 +127,7 @@ builtin_initialize
    (Array Lsp.LocationLink)
    fun ⟨kind, ⟨i⟩⟩ => RequestM.asTask do
      let rc ← read
-      let ls ← FileWorker.locationLinksOfInfo kind i.ctx i.info
+      let ls ← FileWorker.locationLinksOfInfo kind i
      if !ls.isEmpty then return ls
      -- TODO(WN): unify handling of delab'd (infoview) and elab'd (editor) applications
      let .ofTermInfo ti := i.info | return #[]
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@ -8,6 +8,33 @@ import Lean.PrettyPrinter

 namespace Lean.Elab

+/-- Elaborator information with elaborator context.
+
+It can be thought of as a "thunked" elaboration computation that allows us
+to retroactively extract type information, symbol locations, etc.
+through arbitrary invocations of `runMetaM` (where the necessary context and state
+can be reconstructed from `ctx` and `info.lctx`).
+
+W.r.t. widgets, this is used to tag different parts of expressions in `ppExprTagged`.
+This is the input to the RPC call `Lean.Widget.InteractiveDiagnostics.infoToInteractive`.
+It carries over information about delaborated
+`Info` nodes in a `CodeWithInfos`, and the associated pretty-printing
+functionality is purpose-specific to showing the contents of infoview popups.
+
+For use in standard LSP go-to-definition (see `Lean.Server.FileWorker.locationLinksOfInfo`),
+all the elaborator information we need for similar tasks is already fully recoverable via
+the `InfoTree` structure (see `Lean.Elab.InfoTree.visitM`).
+There we use this as a convienience wrapper for queried nodes (e.g. the return value of
+`Lean.Elab.InfoTree.hoverableInfoAt?`). It also includes the children info nodes
+as additional context (this is unused in the RPC case, as delaboration has no notion of child nodes).
+
+NOTE: This type is for internal use in the infoview/LSP. It should not be used in user widgets.
+-/
+structure InfoWithCtx where
+  ctx  : Elab.ContextInfo
+  info : Elab.Info
+  children : PersistentArray InfoTree
+
 /-- Visit nodes, passing in a surrounding context (the innermost one) and accumulating results on the way back up. -/
 partial def InfoTree.visitM [Monad m]
    (preNode  : ContextInfo → Info → (children : PersistentArray InfoTree) → m Unit := fun _ _ _ => pure ())
@ -135,11 +162,16 @@ def InfoTree.smallestInfo? (p : Info → Bool) (t : InfoTree) : Option (ContextI
  infos.toArray.getMax? (fun a b => a.1 > b.1) |>.map fun (_, ci, i) => (ci, i)

 /-- Find an info node, if any, which should be shown on hover/cursor at position `hoverPos`. -/
-partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) (includeStop := false) (omitAppFns := false) : Option (ContextInfo × Info) := Id.run do
-  let results := t.visitM (m := Id) (postNode := fun ctx info _ results => do
+partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) (includeStop := false) (omitAppFns := false) (omitIdentApps := false) : Option InfoWithCtx := Id.run do
+  let results := t.visitM (m := Id) (postNode := fun ctx info children results => do
    let mut results := results.bind (·.getD [])
    if omitAppFns && info.stx.isOfKind ``Parser.Term.app && info.stx[0].isIdent then
-      results := results.filter (·.2.2.stx != info.stx[0])
+        results := results.filter (·.2.info.stx != info.stx[0])
+    if omitIdentApps && info.stx.isIdent then
+      -- if an identifier stands for an application (e.g. in the case of a typeclass projection), prefer the application
+      if let .ofTermInfo ti := info then
+        if ti.expr.isApp then
+          results := results.filter (·.2.info.stx != info.stx)
    unless results.isEmpty do
      return results  -- prefer innermost results
    /-
@ -161,7 +193,7 @@ partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) (in
      Int.negOfNat (r.stop - r.start).byteIdx,
      -- prefer results for constants over variables (which overlap at declaration names)
      if info matches .ofTermInfo { expr := .fvar .., .. } then 0 else 1)
-    [(priority, ctx, info)]) |>.getD []
+    [(priority, {ctx, info, children})]) |>.getD []
  -- sort results by lexicographical priority
  let maxPrio? :=
    let _ := @lexOrd
@ -169,8 +201,8 @@ partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) (in
    let _ := @maxOfLe
    results.map (·.1) |>.maximum?
  let res? := results.find? (·.1 == maxPrio?) |>.map (·.2)
-  if let some (_, i) := res? then
-    if let .ofTermInfo ti := i then
+  if let some i := res? then
+    if let .ofTermInfo ti := i.info then
      if ti.expr.isSyntheticSorry then
        return none
  return res?
@ -328,7 +360,7 @@ where
    stx.getNumArgs == 2 && stx[0].isToken "by" && stx[1].getNumArgs == 1 && stx[1][0].isMissing


-partial def InfoTree.termGoalAt? (t : InfoTree) (hoverPos : String.Pos) : Option (ContextInfo × Info) :=
+partial def InfoTree.termGoalAt? (t : InfoTree) (hoverPos : String.Pos) : Option InfoWithCtx :=
  -- In the case `f a b`, where `f` is an identifier, the term goal at `f` should be the goal for the full application `f a b`.
  hoverableInfoAt? t hoverPos (includeStop := true) (omitAppFns := true)

--- a/src/Lean/Widget/Basic.lean
+++ b/src/Lean/Widget/Basic.lean
@ -1,26 +1,13 @@
 import Lean.Elab.InfoTree
 import Lean.Message
 import Lean.Server.Rpc.Basic
+import Lean.Server.InfoUtils

 namespace Lean.Widget

 open Elab Server

-/-- Elaborator information with elaborator context.
-
-This is used to tag different parts of expressions in `ppExprTagged`.
-This is the input to the RPC call `Lean.Widget.InteractiveDiagnostics.infoToInteractive`.
-
-The purpose of `InfoWithCtx` is to carry over information about delaborated
-`Info` nodes in a `CodeWithInfos`, and the associated pretty-printing
-functionality is purpose-specific to showing the contents of infoview popups.
-
-NOTE: This type is for internal use in the infoview. It should not be used in user widgets. -/
-structure InfoWithCtx where
-  ctx  : Elab.ContextInfo
-  info : Elab.Info
-  deriving TypeName
-
+deriving instance TypeName for InfoWithCtx
 deriving instance TypeName for MessageData
 deriving instance TypeName for LocalContext
 deriving instance TypeName for Elab.ContextInfo
--- a/src/Lean/Widget/InteractiveCode.lean
+++ b/src/Lean/Widget/InteractiveCode.lean
@ -6,6 +6,7 @@ Authors: Wojciech Nawrocki
 -/
 import Lean.PrettyPrinter
 import Lean.Server.Rpc.Basic
+import Lean.Server.InfoUtils
 import Lean.Widget.TaggedText
 import Lean.Widget.Basic

@ -28,7 +29,7 @@ inductive DiffTag where
 /-- Information about a subexpression within delaborated code. -/
 structure SubexprInfo where
  /-- The `Elab.Info` node with the semantics of this part of the output. -/
-  info : WithRpcRef InfoWithCtx
+  info : WithRpcRef Lean.Elab.InfoWithCtx
  /-- The position of this subexpression within the top-level expression. See `Lean.SubExpr`. -/
  subexprPos : Lean.SubExpr.Pos
  -- TODO(WN): add fields for semantic highlighting
@ -67,7 +68,7 @@ where
      | none   => go subTt
      | some i =>
        let t : SubexprInfo := {
-          info := WithRpcRef.mk { ctx, info := i }
+          info := WithRpcRef.mk { ctx, info := i, children := .empty }
          subexprPos := n
        }
        TaggedText.tag t (go subTt)
--- a/tests/lean/interactive/goTo.lean
+++ b/tests/lean/interactive/goTo.lean
@ -36,9 +36,9 @@ def mkFoo₂ := mkFoo₁

 syntax (name := elabTest) "test" : term

-@[term_elab elabTest] def elabElabTest : Lean.Elab.Term.TermElab := fun _ _ => do
+@[term_elab elabTest] def elabElabTest : Lean.Elab.Term.TermElab := fun orig _ => do
  let stx ← `(2)
-  Lean.Elab.Term.elabTerm stx none
+  Lean.Elab.withMacroExpansionInfo orig stx $ Lean.Elab.Term.elabTerm stx none

     --v textDocument/declaration
 #check test
@ -61,6 +61,54 @@ macro_rules | `(test) => `(3)
 #check test
     --^ textDocument/definition

+class Foo2 where
+  foo : Nat → Nat
+  foo' : Nat
+
+class Foo3 [Foo2] where
+  foo : [Foo2] → Nat
+
+class inductive Foo4 : Nat → Type where
+| mk : Nat → Foo4 0
+
+def Foo4.foo : [Foo4 n] → Nat
+| .mk n => n
+
+class Foo5 where
+  foo : Foo2
+
+
+instance : Foo2 := .mk id 0
+instance : Foo3 := .mk 0
+instance : Foo4 0 := .mk 0
+instance [foo2 : Foo2] : Foo5 := .mk foo2
+
+-- should go-to instance
+              --v textDocument/definition
+#check Foo2.foo  2
+          --^ textDocument/definition
+#check (Foo2.foo)
+           --^ textDocument/definition
+#check (Foo2.foo')
+           --^ textDocument/definition
+
+-- should go-to projection
+#check @Foo2.foo
+           --^ textDocument/definition
+
+-- test that the correct instance index is extracted
+#check (Foo3.foo)
+           --^ textDocument/definition
+
+-- non-projections should not go-to instance
+#check (Foo4.foo)
+           --^ textDocument/definition
+
+set_option pp.all true in
+-- test that multiple instances can be extracted
+#check (Foo5.foo)
+           --^ textDocument/definition
+
 -- duplicate definitions link to the original
 def mkFoo₁ := 1
     --^ textDocument/definition
--- a/tests/lean/interactive/goTo.lean.expected.out
+++ b/tests/lean/interactive/goTo.lean.expected.out
@ -93,7 +93,7 @@
   "end": {"line": 38, "character": 38}},
  "targetRange":
  {"start": {"line": 38, "character": 22},
-   "end": {"line": 40, "character": 34}},
+   "end": {"line": 40, "character": 78}},
  "originSelectionRange":
  {"start": {"line": 43, "character": 7},
   "end": {"line": 43, "character": 11}}}]
@ -136,12 +136,140 @@
  {"start": {"line": 60, "character": 7},
   "end": {"line": 60, "character": 11}}}]
 {"textDocument": {"uri": "file://goTo.lean"},
- "position": {"line": 64, "character": 7}}
+ "position": {"line": 87, "character": 16}}
+[{"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 64, "character": 2}, "end": {"line": 64, "character": 5}},
+  "targetRange":
+  {"start": {"line": 64, "character": 2}, "end": {"line": 64, "character": 5}},
+  "originSelectionRange":
+  {"start": {"line": 87, "character": 7},
+   "end": {"line": 87, "character": 18}}},
+ {"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 80, "character": 0}, "end": {"line": 80, "character": 8}},
+  "targetRange":
+  {"start": {"line": 80, "character": 0}, "end": {"line": 80, "character": 27}},
+  "originSelectionRange":
+  {"start": {"line": 87, "character": 7},
+   "end": {"line": 87, "character": 18}}}]
+{"textDocument": {"uri": "file://goTo.lean"},
+ "position": {"line": 87, "character": 12}}
+[{"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 64, "character": 2}, "end": {"line": 64, "character": 5}},
+  "targetRange":
+  {"start": {"line": 64, "character": 2}, "end": {"line": 64, "character": 5}},
+  "originSelectionRange":
+  {"start": {"line": 87, "character": 7},
+   "end": {"line": 87, "character": 15}}}]
+{"textDocument": {"uri": "file://goTo.lean"},
+ "position": {"line": 89, "character": 13}}
+[{"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 64, "character": 2}, "end": {"line": 64, "character": 5}},
+  "targetRange":
+  {"start": {"line": 64, "character": 2}, "end": {"line": 64, "character": 5}},
+  "originSelectionRange":
+  {"start": {"line": 89, "character": 8},
+   "end": {"line": 89, "character": 16}}},
+ {"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 80, "character": 0}, "end": {"line": 80, "character": 8}},
+  "targetRange":
+  {"start": {"line": 80, "character": 0}, "end": {"line": 80, "character": 27}},
+  "originSelectionRange":
+  {"start": {"line": 89, "character": 8},
+   "end": {"line": 89, "character": 16}}}]
+{"textDocument": {"uri": "file://goTo.lean"},
+ "position": {"line": 91, "character": 13}}
+[{"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 65, "character": 2}, "end": {"line": 65, "character": 6}},
+  "targetRange":
+  {"start": {"line": 65, "character": 2}, "end": {"line": 65, "character": 6}},
+  "originSelectionRange":
+  {"start": {"line": 91, "character": 8},
+   "end": {"line": 91, "character": 17}}},
+ {"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 80, "character": 0}, "end": {"line": 80, "character": 8}},
+  "targetRange":
+  {"start": {"line": 80, "character": 0}, "end": {"line": 80, "character": 27}},
+  "originSelectionRange":
+  {"start": {"line": 91, "character": 8},
+   "end": {"line": 91, "character": 17}}}]
+{"textDocument": {"uri": "file://goTo.lean"},
+ "position": {"line": 95, "character": 13}}
+[{"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 64, "character": 2}, "end": {"line": 64, "character": 5}},
+  "targetRange":
+  {"start": {"line": 64, "character": 2}, "end": {"line": 64, "character": 5}},
+  "originSelectionRange":
+  {"start": {"line": 95, "character": 8},
+   "end": {"line": 95, "character": 16}}}]
+{"textDocument": {"uri": "file://goTo.lean"},
+ "position": {"line": 99, "character": 13}}
+[{"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 68, "character": 2}, "end": {"line": 68, "character": 5}},
+  "targetRange":
+  {"start": {"line": 68, "character": 2}, "end": {"line": 68, "character": 5}},
+  "originSelectionRange":
+  {"start": {"line": 99, "character": 8},
+   "end": {"line": 99, "character": 16}}},
+ {"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 81, "character": 0}, "end": {"line": 81, "character": 8}},
+  "targetRange":
+  {"start": {"line": 81, "character": 0}, "end": {"line": 81, "character": 24}},
+  "originSelectionRange":
+  {"start": {"line": 99, "character": 8},
+   "end": {"line": 99, "character": 16}}}]
+{"textDocument": {"uri": "file://goTo.lean"},
+ "position": {"line": 103, "character": 13}}
+[{"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 73, "character": 4}, "end": {"line": 73, "character": 12}},
+  "targetRange":
+  {"start": {"line": 73, "character": 0}, "end": {"line": 74, "character": 12}},
+  "originSelectionRange":
+  {"start": {"line": 103, "character": 8},
+   "end": {"line": 103, "character": 16}}}]
+{"textDocument": {"uri": "file://goTo.lean"},
+ "position": {"line": 108, "character": 13}}
+[{"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 77, "character": 2}, "end": {"line": 77, "character": 5}},
+  "targetRange":
+  {"start": {"line": 77, "character": 2}, "end": {"line": 77, "character": 5}},
+  "originSelectionRange":
+  {"start": {"line": 108, "character": 8},
+   "end": {"line": 108, "character": 16}}},
+ {"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 83, "character": 0}, "end": {"line": 83, "character": 8}},
+  "targetRange":
+  {"start": {"line": 83, "character": 0}, "end": {"line": 83, "character": 41}},
+  "originSelectionRange":
+  {"start": {"line": 108, "character": 8},
+   "end": {"line": 108, "character": 16}}},
+ {"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 80, "character": 0}, "end": {"line": 80, "character": 8}},
+  "targetRange":
+  {"start": {"line": 80, "character": 0}, "end": {"line": 80, "character": 27}},
+  "originSelectionRange":
+  {"start": {"line": 108, "character": 8},
+   "end": {"line": 108, "character": 16}}}]
+{"textDocument": {"uri": "file://goTo.lean"},
+ "position": {"line": 112, "character": 7}}
 [{"targetUri": "file://goTo.lean",
  "targetSelectionRange":
  {"start": {"line": 9, "character": 4}, "end": {"line": 9, "character": 10}},
  "targetRange":
  {"start": {"line": 9, "character": 0}, "end": {"line": 17, "character": 1}},
  "originSelectionRange":
-  {"start": {"line": 64, "character": 4},
-   "end": {"line": 64, "character": 10}}}]
+  {"start": {"line": 112, "character": 4},
+   "end": {"line": 112, "character": 10}}}]
--- a/tests/lean/interactive/goTo2.lean
+++ b/tests/lean/interactive/goTo2.lean
--- a/tests/lean/interactive/goTo2.lean.expected.out
+++ b/tests/lean/interactive/goTo2.lean.expected.out
@ -1,6 +1,6 @@
-{"textDocument": {"uri": "file://goto2.lean"},
+{"textDocument": {"uri": "file://goTo2.lean"},
 "position": {"line": 10, "character": 15}}
-[{"targetUri": "file://goto2.lean",
+[{"targetUri": "file://goTo2.lean",
  "targetSelectionRange":
  {"start": {"line": 1, "character": 0}, "end": {"line": 1, "character": 55}},
  "targetRange":
@ -8,9 +8,9 @@
  "originSelectionRange":
  {"start": {"line": 10, "character": 11},
   "end": {"line": 10, "character": 20}}}]
-{"textDocument": {"uri": "file://goto2.lean"},
+{"textDocument": {"uri": "file://goTo2.lean"},
 "position": {"line": 10, "character": 27}}
-[{"targetUri": "file://goto2.lean",
+[{"targetUri": "file://goTo2.lean",
  "targetSelectionRange":
  {"start": {"line": 2, "character": 0}, "end": {"line": 2, "character": 55}},
  "targetRange":
@ -18,9 +18,9 @@
  "originSelectionRange":
  {"start": {"line": 10, "character": 23},
   "end": {"line": 10, "character": 30}}}]
-{"textDocument": {"uri": "file://goto2.lean"},
+{"textDocument": {"uri": "file://goTo2.lean"},
 "position": {"line": 10, "character": 11}}
-[{"targetUri": "file://goto2.lean",
+[{"targetUri": "file://goTo2.lean",
  "targetSelectionRange":
  {"start": {"line": 14, "character": 4}, "end": {"line": 14, "character": 5}},
  "targetRange":