LSP: fix go-to-definition, hover, and stale session state

Go-to-definition and hover:
- External symbols landed at line 1 of the target file (URI vs raw
  path comparison always failed).
- "M.foo" resolved wrong: a local "foo" shadowed it, and with
  "require M as A", "A.foo" did not resolve at all. Route the
  qualified identifier through Sig_state.find_sym instead of the
  flat name map.
- Hover returned a range shifted one column left (stale "column - 1"
  from 1-based days).
- Illegal ranges reached the wire: the error fallback fabricated
  line-0 positions that became -1 after 1-based to 0-based
  conversion, and generated symbols carry virtual positions encoding
  their declaration order for the Dedukti export (a recursor points
  one column past the end of its inductive command, an inverted
  range). Add the Pos.file_start helper for the former, and sanitize
  in mk_range for the latter: floor coordinates at 0 and collapse
  inverted ranges to a caret at their start.
- Ghost symbols (internal: unification rules, string literals) have
  no user-facing definition site and are skipped.

Stale session state: initial_state restores Time and re-applies the
opened file's package config, wiping other open documents' library
mappings. A subsequent request on an older document resolved paths
against the newest document's mappings. Call Pure.restore_time at
the start of every affected request handler.

Also: mk_definfo takes a plain filesystem path (its only caller
never passes a URI); concise per-request logging in do_definition
and hover_symInfo, replacing the unbounded token-map/symbol-map
debug dumps; fix the misleading "Root state is missing" message in
hover_symInfo.

Author: ciaran-matthew-dunne

AUTHORS.md

@@ -7,6 +7,7 @@ Active Contributors (in alphabetical order)
 - Abdelghani Alidra (2024-)
 - Bruno Barras (2025-)
 - Jean-Paul Bodeveix (2026-)
+- Ciarán Dunne (2026-)
 
 Past Contributors (in alphabetical order)
 =========================================

CHANGES.md

@@ -47,6 +47,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 - Selection of the library mapping with the longest matching prefix in
   `path_of_file`: with nested mappings, the computed module path could get a
   duplicated directory component.
+- LSP server: go-to-definition and hover on qualified identifiers, and session
+  state leaking between open documents.
 
 ## 3.0.0 (2025-07-16)
 

src/common/pos.ml

@@ -36,6 +36,13 @@ let cat : pos -> pos -> pos = fun p1 p2 ->
   ; end_col = p2.end_col
   ; end_offset = p2.end_offset }
 
+(** [file_start fname] is a zero-length position at the start of file [fname],
+    used as a fallback for error reporting when no finer position is known. *)
+let file_start : string -> pos = fun fname ->
+  { fname = Some fname
+  ; start_line = 1; start_col = 0; start_offset = 0
+  ; end_line = 1; end_col = 0; end_offset = 0 }
+
 (** [locate ?fname (p1,p2)] converts the pair of Lexing positions [p1,p2] and
     filename [fname] into a {!type:pos}. *)
 let locate : ?fname:string -> Lexing.position * Lexing.position -> pos =

src/lsp/lp_doc.ml

@@ -148,17 +148,7 @@ let new_doc ~uri ~version ~text =
       let path = String.sub uri 7 (String.length uri - 7) in
       Some(Pure.initial_state path), []
     with Error.Fatal(_pos, msg, err_desc) ->
-      let loc : Pos.pos =
-        {
-          fname = Some(uri);
-          start_line = 0;
-          start_col  = 0;
-          start_offset  = 0;
-          end_line = 0;
-          end_col = 0;
-          end_offset  = 0
-        } in
-      (None, [(1, msg ^ "\n" ^ err_desc), Some(loc)])
+      (None, [(1, msg ^ "\n" ^ err_desc), Some (Pos.file_start uri)])
   in
   { uri;
     text;

src/lsp/lp_lsp.ml

@@ -10,7 +10,7 @@
 (* Status: Very Experimental                                            *)
 (************************************************************************)
 
-open Lplib open Extra
+open Lplib
 open Common
 open Core
 
@@ -59,17 +59,8 @@ let do_check_text ofmt ~doc =
     try
       Lp_doc.check_text ~doc
     with Common.Error.Fatal(_pos, msg, err_desc) ->
-      let loc : Pos.pos =
-        {
-          fname = Some(doc.uri);
-          start_line = 0;
-          start_col  = 0;
-          start_offset  = 0;
-          end_line = 0;
-          end_col = 0;
-          end_offset  = 0;
-        } in
-      (doc, Lp_doc.mk_error ~doc loc (msg ^ "\n" ^ err_desc))
+      (doc, Lp_doc.mk_error ~doc (Pos.file_start doc.uri)
+              (msg ^ "\n" ^ err_desc))
   in
   Hashtbl.replace doc_table doc.uri doc;
   Hashtbl.replace completed_table doc.uri doc;
@@ -131,9 +122,11 @@ let mk_syminfo file (name, _path, kind, pos) : J.t =
                   ]
   ]
 
+(* [file] is a plain filesystem path (as produced by
+   [Library.file_of_path]), never a URI. *)
 let mk_definfo file pos =
   `Assoc [
-      "uri", `String file
+      "uri", `String ("file://" ^ file)
     ; "range", LSP.mk_range pos
         ]
 
@@ -157,6 +150,7 @@ let do_symbols ofmt ~id params =
     let msg = LSP.mk_reply ~id ~result:`Null in
     LIO.send_json ofmt msg
   | Some ss ->
+    Pure.restore_time ss;
     let sym = Pure.get_symbols ss in
     let sym =
       Extra.StrMap.fold
@@ -231,9 +225,10 @@ let get_node_at_pos doc line pos =
   List.find_opt (fun { ast; _ } ->
       let loc = Pure.Command.get_pos ast in
       let res = in_range ?loc (line,pos) in
-      let ls = Format.asprintf "%B l:%d p:%d / %a"
-                 res line pos Pos.pp loc in
-      LIO.log_error "get_node_at_pos" ("call: "^ls);
+      (* trace, per command node, whether the query (line,pos) falls in its
+         range [loc] (header "get_node_at_pos") *)
+      LIO.log_error "get_node_at_pos"
+        (Format.asprintf "%b l:%d p:%d / %a" res line pos Pos.pp loc);
       res
     ) doc.Lp_doc.nodes
 
@@ -272,24 +267,18 @@ let rec get_goals ~doc ~line ~pos =
     | Some (v,_) -> Some v
 
 let get_logs ~doc ~line ~pos : string =
-  (* DEBUG LOG START *)
+  (* Log the query location and one line per document log element: its
+     severity, source position and a 30-char message preview (header
+     "get_logs"). *)
+  let elt ((sev, msg), po) =
+    let loc = match po with
+      | Some p -> Printf.sprintf "%d,%d" p.Pos.start_line p.Pos.start_col
+      | None -> "?" in
+    let preview = String.sub msg 0 (min 30 (String.length msg)) in
+    Format.asprintf "sev:%d @%s %S" sev loc preview in
   LIO.log_error "get_logs"
-    (Printf.sprintf "%s:%d,%d" doc.Lp_doc.uri line pos);
-  let log_to_str ((sev, log), posopt) =
-    let pos_str =
-      match posopt with
-      | None -> "None"
-      | Some Pos.{start_line; start_col; _} ->
-          Printf.sprintf "(%d, %d)" start_line start_col
-    in
-    let log_str =
-      let len = String.length log in
-      Printf.sprintf "length: %d | %s" len (String.sub log 0 (min 30 len))in
-    Format.asprintf "element(severity:%d): %s -> %s\n " sev pos_str log_str
-  in
-  Lsp_io.log_error "get_logs"
-    (List.fold_left (^) "\n" (List.map log_to_str doc.Lp_doc.logs));
-  (* DEBUG LOG END *)
+    (Printf.sprintf "%s:%d,%d\n%s" doc.Lp_doc.uri line pos
+       (String.concat "\n" (List.map elt doc.Lp_doc.logs)));
   let line = line+1 in
   let end_limit =
     match get_first_error doc with
@@ -318,20 +307,30 @@ let do_goals ofmt ~id params =
   let msg = LSP.mk_reply ~id ~result in
   LIO.send_json ofmt msg
 
-let msg_fail hdr msg =
-  LIO.log_error hdr msg;
-  failwith msg
 
-let get_symbol : Range.point ->
-('a * 'b) RangeMap.t -> ('b * Range.t) option
+let get_symbol : Range.point -> 'a RangeMap.t -> ('a * Range.t) option
 = fun pos doc ->
 
   let open RangeMap in
 
   match (find pos doc) with
   | None -> None
-  | Some(interval, (_, token)) -> Some (token, interval)
-
+  | Some(interval, value) -> Some (value, interval)
+
+(* Dump, to the LSP debug log, the two tables consulted when resolving the
+   symbol under the cursor: the token map ("token map": each source range ->
+   identifier), and the in-scope symbols with their declaration positions
+   ("symbol map"). Diagnostic aid for failed go-to-definition / hover. *)
+let log_symbol_maps doc ss =
+  LIO.log_error "token map" (RangeMap.to_string snd doc.Lp_doc.map);
+  let syms =
+    Pure.get_symbols ss
+    |> Extra.StrMap.bindings
+    |> List.map (fun (name, s) ->
+        Format.asprintf "%s: @[%a@]" name Pos.pp s.Term.sym_pos)
+    |> String.concat "\n"
+  in
+  LIO.log_error "symbol map" syms
 
 let do_definition ofmt ~id params =
 
@@ -341,122 +340,65 @@ let do_definition ofmt ~id params =
     let msg = LSP.mk_reply ~id ~result:`Null in
     LIO.send_json ofmt msg
   | Some ss ->
+    Pure.restore_time ss;
+    log_symbol_maps doc ss;
     let ln, pos = get_textPosition params in
 
-    (* Lines send by the client start at 0 *)
+    (* Lines sent by the client start at 0 *)
     let pt = Range.make_point (ln + 1) pos in
-    let sym_target =
-      match get_symbol pt doc.map with
-      | None -> "No symbol found"
-      | Some(token, _) -> token
-    in
-
-    (*Some printing in the log*)
-    LIO.log_error "token map" (RangeMap.to_string snd doc.map);
-    LIO.log_error "do_definition" sym_target;
-
-    let sym = Pure.get_symbols ss in
-    let map_pp : string =
-      Extra.StrMap.bindings sym
-      |> List.map (fun (key, sym) ->
-          Format.asprintf "{%s} / %s: @[%a@]"
-            key sym.Term.sym_name Pos.pp sym.sym_pos)
-      |> String.concat "\n"
-    in
-    LIO.log_error "symbol map" map_pp;
-
     let sym_info =
-      match StrMap.find_opt sym_target sym with
-      | None -> `Null
-      | Some s ->
-        match s.sym_pos with
+      match get_symbol pt doc.map with
+      | None ->
+        LIO.log_error "do_definition" "no symbol at point"; `Null
+      | Some (qid, _) ->
+        LIO.log_error "do_definition" (snd qid);
+        match Pure.find_sym ss qid with
         | None -> `Null
-        | Some pos ->
-        (* A JSON with the path towards the definition of the term
-          and its position is returned
-          /!\ : extension is fixed, only works for .lp files *)
-          mk_definfo
-            Library.(file_of_path s.Term.sym_path ^ lp_src_extension) pos
+        (* Ghost symbols (internal symbols used e.g. for unification
+           rules and string literals) have no user-facing definition
+           site one could jump to. *)
+        | Some s when s.Term.sym_path = Sign.Ghost.path -> `Null
+        | Some s ->
+          let file =
+            Library.(file_of_path s.Term.sym_path ^ lp_src_extension) in
+          let pos = Option.get (Pos.file_start file) s.sym_pos in
+          mk_definfo file pos
     in
     let msg = LSP.mk_reply ~id ~result:sym_info in
     LIO.send_json ofmt msg
 
 let hover_symInfo ofmt ~id params =
-
   let _, _, doc = grab_doc params in
   let ln, pos = get_textPosition params in
-
-  (* Positions sent by the client are one line late *)
   let pt = Range.make_point (ln + 1) pos in
-  LIO.log_error "searched point" (Range.point_to_string pt);
-
-  (* The hovered token and its start/finish positions are stored *)
-  let sym_target, interval  =
-  match get_symbol pt doc.map with
-    | None ->
-      "No symbol found", (Range.make_interval pt pt)
-    (* VSCode highlights the token properly if the interval is extended to the
-       character next to it. This might be handled differently in other
-       editors in the future, but it is the most practical solution for
-       now. *)
-    | Some(token, range) ->
-      token, (Range.translate range 0 1)
-  in
+  LIO.log_error "hover_symInfo" (Range.point_to_string pt);
 
-  (* Some printing in the log *)
-  (* LIO.log_error "token map" (RangeMap.to_string snd doc.map);
-
-  LIO.log_error "hoverSymInfo" sym_target;
-  LIO.log_error "hoverSymInfo" (Range.interval_to_string interval); *)
+  let send_null () =
+    LIO.send_json ofmt (LSP.mk_reply ~id ~result:`Null)
+  in
 
   try
-    (* The information about the tokens is stored *)
-    let sym =
-      match doc.final with
-      | Some ss -> Pure.get_symbols ss
-      | None    -> raise (Error.fatal_no_pos("Root state is missing
-      probably because new_doc has raised exception")) in
-
-    (* The start/finish positions are used to hover the full qualified term,
-      not just the token *)
-    let start = Range.interval_start interval
-    and finish = Range.interval_end interval in
-
-    (* FIXME: types and typed conversion should take care of this *)
-    let sl, sc, fl, fc =
-      (Range.line start - 1),
-      (Range.column start - 1),
-      (Range.line finish - 1),
-      (Range.column finish - 1)
-    in
-
-    let s = `Assoc["line", `Int sl; "character", `Int sc] in
-    let f = `Assoc["line", `Int fl; "character", `Int fc] in
-    let range = `Assoc["start", s; "end", f] in
-
-    let map_pp : string =
-      Extra.StrMap.bindings sym
-      |> List.map (fun (key, sym) ->
-          Format.asprintf "{%s} / %s: @[%a@]"
-            key sym.Term.sym_name Pos.pp sym.sym_pos)
-      |> String.concat "\n"
-    in
-    LIO.log_error "symbol map" map_pp;
-
-    let sym_found =
-      match StrMap.find_opt sym_target sym with
-      | None -> msg_fail "hover_SymInfo" "Sym not found"
-      | Some sym -> sym
-    in
-    let sym_type = Format.asprintf "%a" Core.Print.sym_type sym_found in
-    let result : J.t =
-      `Assoc [ "contents", `String sym_type; "range", range ] in
-    let msg = LSP.mk_reply ~id ~result in
-    LIO.send_json ofmt msg
-
-  with _ ->
-    let msg = LSP.mk_reply ~id ~result:`Null in
-    LIO.send_json ofmt msg
+    let ss = match doc.final with
+      | Some ss -> ss
+      | None ->
+        raise (Error.fatal_no_pos "Final state is missing: the document \
+                                   was never successfully loaded") in
+    Pure.restore_time ss;
+    log_symbol_maps doc ss;
+
+    match get_symbol pt doc.map with
+    | None -> send_null ()
+    | Some (qid, range) ->
+      match Pure.find_sym ss qid with
+      | None -> LIO.log_error "hover_symInfo" "Sym not found"; send_null ()
+      | Some sym_found ->
+        let sym_type = Format.asprintf "%a" Core.Print.sym_type sym_found in
+        let result = `Assoc [ "contents", `String sym_type
+                            ; "range", LSP.mk_range_of_interval range ] in
+        LIO.send_json ofmt (LSP.mk_reply ~id ~result)
+  with e ->
+    LIO.log_error "hover_symInfo" (Printexc.to_string e);
+    send_null ()
 
 let protect_dispatch p f x =
   try f x
@@ -488,10 +430,12 @@ let dispatch_message ofmt dict =
       (do_symbols ofmt ~id) params
 
   | "textDocument/hover" ->
-    hover_symInfo ofmt ~id params
+    (try hover_symInfo ofmt ~id params
+     with _ -> LIO.send_json ofmt (LSP.mk_reply ~id ~result:`Null))
 
   | "textDocument/definition" ->
-    do_definition ofmt ~id params
+    (try do_definition ofmt ~id params
+     with _ -> LIO.send_json ofmt (LSP.mk_reply ~id ~result:`Null))
 
   | "proof/goals" ->
     do_goals ofmt ~id params
@@ -528,13 +472,12 @@ let process_input ofmt (com : J.t) =
     let bt = Printexc.get_backtrace () in
     LIO.log_error "[BT]" bt;
     LIO.log_error "process_input" (Printexc.to_string exn);
-    (*Send an "empty" answer with Null goals when exception occurs*)
-    let id     = oint_field "id" (U.to_assoc com) in
-    let goals = None in
-    let logs = "" in
-    let result = LSP.json_of_goals goals ~logs in
-    let msg = LSP.mk_reply ~id ~result in
-    LIO.send_json ofmt msg
+    (* Send a null reply so the client doesn't hang *)
+    let id = oint_field "id" (U.to_assoc com) in
+    if id <> 0 then begin
+      let msg = LSP.mk_reply ~id ~result:`Null in
+      LIO.send_json ofmt msg
+    end
 
 let main std log_file =
 

src/lsp/lp_lsp.mli

@@ -13,3 +13,4 @@
 val default_log_file : string
 
 val main : bool -> string -> unit
+(** [main standard_lsp log_file] starts the LSP server. *)