fix(lsp): correctness bugs in positions, lookups, and session state#1366
Draft
ciaran-matthew-dunne wants to merge 6 commits intoDeducteam:masterfrom
Draft
fix(lsp): correctness bugs in positions, lookups, and session state#1366ciaran-matthew-dunne wants to merge 6 commits intoDeducteam:masterfrom
ciaran-matthew-dunne wants to merge 6 commits intoDeducteam:masterfrom
Conversation
Member
|
Hi @ciaran-matthew-dunne . Thanks for your PR! Let me know when it is ready for review. |
path_of_file iterates every library mapping and keeps the one whose
filesystem prefix is the longest match. Inside the update branch, the
longer module-path prefix (mp) was being paired with the SHORTER
filesystem prefix (p) from the previous candidate instead of the new,
longer one (fp):
| Some(_, p) ->
if String.(length p < length fp) then mapping := Some(mp, p)
^
should be fp
Consequence: for <root>/Stdlib/Nat.lp under [Stdlib] -> <root>/Stdlib,
the chosen mp was ["Stdlib"] but the stored fs prefix stayed <root>.
The remainder computation saw "Stdlib/Nat" and the final module path
came out as ["Stdlib"; "Stdlib"; "Nat"].
Via sym_path, this doubled every qualified reference the signature
emitted; in the LSP it appeared as go-to-def URIs with a duplicated
directory component.
`Pure.handle_tactic` prepended `Pos.popt_to_string p ^ " "` to the error message before returning `Tac_Error(Some p, ...)`. The LSP diagnostic already carries the position as its range, so clients rendered the file:line:column twice — once as the underline and again inside the message body. Mirror `handle_command` and `end_proof`, which return the raw message unchanged.
Four correctness bugs in the same two handlers. Three of them share a root cause: the code carried its own hand-rolled conversions (URI vs path, short-name vs qualified lookup, 1-based vs 0-based columns) instead of reusing the helpers that the rest of the codebase already uses. 1. External symbols landed at line 1 of the target file. do_definition compared sym_pos.fname (raw path) against doc.uri (URI). The check always failed for external symbols and the code fell back to a synthesized line-1 position. Use sym_pos directly when present, and normalize mk_definfo's file argument into a URI. 2. Qualified references M.foo resolved wrong. A local foo shadowed the qualified target, and aliased paths (require M as A; A.foo) never resolved at all. The hand-rolled lookup tried short-name first and didn't know about aliases. Route both handlers through a new Pure.find_sym that wraps Sig_state.find_sym, which already has the correct precedence and handles aliases. 3. Hover returned a range shifted one column to the left. hover_symInfo was the only handler still building its range JSON by hand, with its own column math that had drifted out of sync with the rest of the server (a stale `column - 1` from when columns were 1-based). Replace the hand-rolled block with a new helper LSP.mk_range_of_interval — the same Range.t -> LSP-JSON conversion that diagnostics and go-to-def already go through. 4. Error-position fallback sent -1 on the wire. When initial_state raised, new_doc synthesized a fallback Pos.pos with start_line = 0. The 1-based -> 0-based conversion turned that into -1, which strict clients reject (LSP positions are uinteger). Introduce Pos.file_start for the fallback, and clamp negative values to 0 in mk_range / mk_range_of_interval as a defense-in-depth measure. Drive-by cleanups in the same handlers: - Generalize get_symbol from qident-specific to 'a RangeMap.t. - Wrap the hover/definition dispatch in try _ with _ -> null so a bogus request can't hang the handler. - Replace process_input's fake-goal_info fallback with plain null. - Drop the msg_fail helper (unused after the rewrite). - Use Lplib.String.is_prefix for the file:// URI guard, matching Lp_doc and Common.Library. UTF-16 note: LSP columns are UTF-16 code units; Lambdapi columns are codepoints. For every character Lambdapi syntax actually uses (ASCII plus BMP glyphs like ℕ → ≔ ↪) they coincide, so no conversion is needed. Supplementary-plane characters would require negotiation, left as a follow-up.
`Pure.initial_state` does `Time.restore t0` and then re-applies the package config for the opened file. That installs the file's library mappings but wipes out any mappings belonging to other open documents. As a result, opening doc A, then opening doc B (from a different package), caused subsequent go-to-def / hover / document-symbol requests on A to call `Library.file_of_path` against B's mappings — returning paths that collapse A's module path back to the lib root. Opening Nat.lp from Binom.lp and then querying inside Binom.lp, for example, produced URIs like `<lib_root>/Fermat/Binom.lp` instead of the real `<repo>/benchmarks/fermat/Binom.lp`. Expose `Pure.restore_time` and call it at the start of `do_definition`, `hover_symInfo`, and `do_symbols` so each request reads the timed globals from the target document's saved state rather than whatever was most recently opened.
do_close removed the URI from doc_table but not from completed_table, so every file the client had ever opened kept a fully-elaborated Lp_doc.t — including the pinned signature state and every term the file produced — alive for the lifetime of the LSP process. In a long editing session this grows without bound: a modest file can pin tens of MB of signature data, and nothing ever releases it. Remove from both tables.
…ommand
Every successful top-level command and tactic emits a severity-4 "hint"
diagnostic so the client can draw a success indicator. The server was
attaching that diagnostic to the range of the WHOLE command or tactic:
symbol foo : Nat → Nat ≔
λ x, add x x; <-- entire span underlined as "OK"
opaque symbol thm : … ≔ begin
assume h; apply h <-- whole proof underlined per tactic
end;
That range is wrong: the success applies to the *thing being declared*
or *the action that succeeded*, not to the body that follows. Wide
underlines over bodies and proofs also compete visually with the
tactic-error ranges a client cares about.
Attach each hint to the token that actually names the action:
- symbol / inductive / opaque: the declared name.
- rule / unif_rule / coerce_rule / notation / builtin / require /
require … as / open: the command keyword.
- query commands (assert, compute, type, print, …): the query keyword.
- tactics (refine, assume, rewrite, reflexivity, …): the tactic
keyword.
Mechanism: new Pure.keyword_pos (takes the start of a Pos.pos and a
length), Pure.query_keyword_len, and Command.get_focus_pos /
Tactic.get_focus_pos pure-syntax helpers. Lp_doc.process_cmd /
process_pstep feed the hint diagnostic from get_focus_pos instead of
get_pos; every other diagnostic path (errors, goal info) is unchanged.
ciaran-matthew-dunne
force-pushed
the
pr/lsp-correctness
branch
from
47074a8 to
819f767
Compare
6 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
path_of_file: a one-character typo paired the longermodule-path prefix with the shorter filesystem prefix in the
selected library mapping, so every URI the server emitted for a
mapped file had its directory component doubled
(
Stdlib/Stdlib/Nat.lp).Tactic error messages:
handle_tacticprependedPos.popt_to_stringto the error string. The diagnostic alreadycarries the position as its range, so clients rendered
file:line:coltwice. Mirrorshandle_command/end_proof.Go-to-definition and hover:
raw path comparison always failed).
M.fooresolved wrong — localfooshadowed it;require M as A; A.foodidn't resolve at all. Route throughSig_state.find_sym.column - 1from 1-based days).-1on the wire. AddPos.file_starthelper and clamp inmk_range.Timed state between documents:
initial_staterestoresTimeand re-applies the opened file's package config, wipingother open docs' library mappings. A subsequent request on the
older doc resolved paths against the newer doc's mappings. Call
Pure.restore_timeat the start of every affected handler.Session-lifetime memory leak:
do_closeremoved the URIfrom
doc_tablebut notcompleted_table, so every file theclient ever opened kept its fully-elaborated
Lp_doc.talivefor the process lifetime.
Success hints attached to wrong range: severity-4 "OK"
hints spanned the whole command/tactic, so the success underline
covered symbol bodies, proofs, and rule RHSs. Narrow to the
declared name (
symbol/inductive/opaque) or the leadingkeyword.