fix(lsp): go-to-definition, hover, and stale session state by ciaran-matthew-dunne · Pull Request #1366 · Deducteam/lambdapi

ciaran-matthew-dunne · 2026-04-20T16:14:08Z

1. Fix go-to-definition and hover

Four bugs in do_definition/hover_symInfo. Three share a root cause: the handlers carried hand-rolled conversions (URI vs path, short-name vs qualified lookup, 1-based vs 0-based columns) instead of reusing the helpers the rest of the codebase uses.

1a. Go-to-definition on an external symbol lands at line 1 of the target file

Issue: Go-to-definition on any symbol defined in another module always points to line 1 of the file.
Cause: do_definition compared the symbol's sym_pos.fname (a raw filesystem path) against doc.uri (a file:// URI). The comparison never succeeds for external symbols, so the code fell back to a synthesized line-1 position.
Fix: use sym_pos directly when present; mk_definfo takes the filesystem path (the only thing its caller ever passes) and builds the URI from it.

1b. Qualified identifiers resolve to the wrong symbol; aliases don't resolve at all

Issue:
(i). go-to-definition/hover on M.foo while a local symbol is also named foo targets the local foo.
(ii). go-to-definition/hover on a qualified symbol (i.e., A.foo given require M as A;) gives no result.
Cause: the handlers looked the name up in the flat in-scope short-name map, trying the unqualified name first, with no knowledge of module aliases.
Fix: new Pure.find_sym wrapping Sig_state.find_sym as used by scoper, with correct shadowing precedence and alias support. Both handlers now pass the full qualified identifier through it.

1c. Hover highlights a range shifted one column to the left

Cause: hover_symInfo was the only handler still assembling its range JSON by hand, and its column arithmetic had drifted: a stale column - 1 from when columns were 1-based.
Fix: new helper LSP.mk_range_of_interval; hover now uses the same Range.t → JSON conversion that diagnostics and go-to-definition go through.

1d. Illegal positions reach the client

Issue: LSP positions must be uinteger with start <= end.
Fix: json_of_range sanitizes every outgoing range: coordinates floored at 0, inverted ranges collapsed to a caret at their start.

2. Requests on one document run against another document's state

Issue: open document A, then open document B from a different package; any go-to-definition / hover / documentSymbol request on A afterwards resolves paths against B's configuration.
e.g., with Foo.lp open, opening Nat.lp from Stdlib made subsequent queries in Foo.lp produce URIs relative to <lib_root>/Stdlib/... rather than that of the package.
Cause: Pure.initial_state does Time.restore t0 and re-applies the opened file's package config, which installs that file's library mappings and wipes the mappings of every other open document (they live in timed state).
Fix: expose Pure.restore_time and call it at the start of do_definition, hover_symInfo and do_symbols, so each request restores the timed state saved with its own document before touching timed globals like Library.lib_mappings.

fblanqui · 2026-04-21T17:35:29Z

Hi @ciaran-matthew-dunne . Thanks for your PR! Let me know when it is ready for review.

ciaran-matthew-dunne · 2026-05-22T15:26:09Z

@Alidra !

ciaran-matthew-dunne · 2026-07-01T14:23:04Z

  let doc_file = string_field "uri" document in
-  Hashtbl.remove doc_table doc_file
+  Hashtbl.remove doc_table doc_file;
+  Hashtbl.remove completed_table doc_file


questionable that this actually solves any 'memory leak' issue. needs deeper investigation/profiling. assigned to @ciaran-matthew-dunne

ciaran-matthew-dunne · 2026-07-01T14:53:16Z

 let mk_event m p   =
  `Assoc [ "jsonrpc", `String "2.0"; "method", `String m; "params", `Assoc p ]

+(* LSP positions are uinteger; clamp defensively to avoid rejection by


why do we need this? when do we pass Pos.pos with negative or zero line/col values? then why does file_start have a col values 0? is there a difference between client-side/server-side line/col position indexing? does this differ between vscode/zed/emacs/vim???

It may be the case that symbols generated by the inductive commands internally have negative positions (to be checked). I don't know whether this can affect LSP which normally only sees user declared symbols (which have >=0 positions).

Emacs counts columns from 0.

Thanks. The inductive N : TYPE ≔ ... command generates an illegal position for ind_N where the end col is before the start col. I won't touch this since a comment in term.ml says: "These virtual positions are however important for exporting lambdapi files to other formats. "

json_of_range now handles the sanitization.

With this PR, do you get meaningful positions for these generated symbols?

Yes, doing go-to-definition on ind_T now points to the end of the inductive command that defined T.

Alidra · 2026-07-02T11:32:57Z

Thank you @ciaran-matthew-dunne for the PR.
It would be nice to have different PRs for different features. That would help a lot with the management of changes and review (for instance the fix related to redundant position prefix in tactic error messages seems to be outdated)

The test harness was written against the old bundled LSP branch. The fixes split out into Deducteam#1366 (file:// URIs in definition responses, qualified-name resolution) and Deducteam#1444 (keyword-anchored OK hints) are not on this branch, so the cases asserting them are marked expectedFailure, each tagged with the PR it waits for. When those PRs merge and this branch rebases, they flip to unexpected-success and the decorators come off.

Python harness driving the server over stdio (make test_lsp): lifecycle, diagnostics, definition, hover, goals, symbols, completion, debouncing. Five cases assert behavior from Deducteam#1366 and Deducteam#1444 and are marked expectedFailure until those PRs merge.

fblanqui

Thanks Ciaran for this PR! You removed quite some logging code. It is not useful anymore, or do you have other ways to get these information?

fblanqui · 2026-07-07T12:00:49Z

 let get_symbols : state -> Term.sym Extra.StrMap.t =
  fun (_, ss) -> ss.in_scope

+let find_sym : state -> Term.qident Pos.loc -> Term.sym option =


Pure.find_sym is always called with (Pos.none qid) and Sig_state.find_sym uses the position in Fatal only. Therefore, Pure.find_sym could take a Term.qident as argument (with no position).

fblanqui · 2026-07-07T12:07:40Z

@ciaran-matthew-dunne Please add your name in AUTHORS.md and update CHANGES.md.

ciaran-matthew-dunne · 2026-07-08T11:38:13Z

Thanks Ciaran for this PR! You removed quite some logging code. It is not useful anymore, or do you have other ways to get these information?

I removed it because it seemed somewhat excessive and could degrade performance (e.g., the logging commands within get_node_at_pos log are inside the function passed to find_opt which runs over every node in the document).

~~I've restored it now and made it a bit leaner in case somebody currently relies on this info.~~

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.

Python harness driving the server over stdio (make test_lsp): lifecycle, diagnostics, definition, hover, goals, symbols, completion, debouncing. Five cases assert behavior from Deducteam#1366 and Deducteam#1444 and are marked expectedFailure until those PRs merge.

ciaran-matthew-dunne marked this pull request as draft April 20, 2026 21:36

ciaran-matthew-dunne force-pushed the pr/lsp-correctness branch from 47074a8 to 819f767 Compare April 22, 2026 13:10

ciaran-matthew-dunne mentioned this pull request Apr 22, 2026

LSP: completion, document outline, documentation hovers, tests #1371

Open

ciaran-matthew-dunne commented May 29, 2026

View reviewed changes

Comment thread src/pure/pure.ml Outdated

ciaran-matthew-dunne commented May 29, 2026

View reviewed changes

Comment thread src/pure/pure.ml Outdated