Skip to content

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

Open
ciaran-matthew-dunne wants to merge 14 commits into
Deducteam:masterfrom
ciaran-matthew-dunne:pr/lsp-ux
Open

LSP: completion, document outline, documentation hovers, tests#1371
ciaran-matthew-dunne wants to merge 14 commits into
Deducteam:masterfrom
ciaran-matthew-dunne:pr/lsp-ux

Conversation

@ciaran-matthew-dunne

@ciaran-matthew-dunne ciaran-matthew-dunne commented Apr 22, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Stacked on #1444 — its 3 commits appear here until it merges.

LSP UX additions, split out of the old bundled branch per review; the bug fixes went to #1443 and #1366 (both merged) and #1444.

Completion

  • in-scope symbols (ghost symbols excluded); no completion kind is assigned — the LSP kinds don't match lambdapi's notions
  • keyword completions are grammar-driven: the parser reports the tokens it accepts at the cursor (new Parser.Lp.expected_tokens, see below), and exactly those keywords are offered — open/private/as after require, the notation kinds after notation f, left/right after infix or associative, on/off after flag "…", rule after simplify, begin after a statement's type, tactic keywords, queries and proof enders at proof-step positions, command keywords and modifiers between commands, …
  • symbols are only offered where the grammar accepts an identifier reference — never in binder positions (after assume, require M as, a symbol name, …)
  • context-aware items with . as a trigger character: module paths after require/open (as a textEdit, since . is not a word character), qualified identifiers after M. (the non-private symbols of the required module, resolving require as aliases), flag names inside flag ", and hypothesis-first ranking in the argument of apply, rewrite, etc.
  • keyword docs and snippets come from the same tables as before; snippets no longer presume one alternative (e.g. require $0; — open, private or a path completes after the keyword)
  • when the text before the cursor does not parse (mid-edit), keyword completions fall back to the context-blind tables and the proof context of the last successful parse
  • type details are attached lazily on completionItem/resolve; docs are sent as markdown MarkupContent when the client supports it

Hover

  • documentation for tactic keywords (inside proofs) and for command and query keywords and modifiers (symbol, inductive, rule, constant, injective, flag, …), sourced from doc/*.rst
  • types of local symbols introduced by assume, inside proofs; types are printed with the document's own printer state; names in a tactic's arguments resolve in the state before the tactic runs (goal snapshots are post-tactic, so a tactic that closes its subgoal or the whole proof used to lose its own arguments' hypotheses)
  • falls back to the token under the cursor looked up in the in-scope symbol table when the checked-AST lookup misses — hover works in mid-edit text and past parse errors

Go-to-definition

  • on require/open module paths (jumps to the start of that module's file)
  • same in-scope fallback as hover

Document outline

  • hierarchical DocumentSymbol[] when the client supports it (constructors as children of their inductive type); the flat SymbolInformation[] list is kept as fallback; symbols are not classified into LSP kinds

Parser

  • new entry point Parser.Lp.expected_tokens (exposed as Pure.expected_tokens): parses a source prefix and returns the tokens acceptable at its end — the follow set the completion handler uses
  • the expected-token recordings behind Expected: … error messages now accumulate until the next consumed token instead of overwriting one another, and a finished application records that the term could continue; syntax errors list more of the true alternatives, with a full set of term starters rendered as one word: Expected: "begin", "≔", ";", "→", a term.

Protocol robustness

  • initialize honours rootUri and workspaceFolders (deduplicated — clients typically send both for the same directory; package-config failures are logged, never fatal) and reads client capabilities
  • unknown request methods get a JSON-RPC MethodNotFound error reply instead of silence; notifications stay unanswered per spec; request ids are echoed back verbatim, including 0 (Zed's first request) and strings
  • message framing parses header lines up to the blank separator, accepting Content-Length in any position

Tests

  • Python integration test suite: make test_lsp (also part of make test), 143 tests speaking JSON-RPC over stdio to a lambdapi lsp subprocess — lifecycle, diagnostics, symbols, hover, definition, completion (including the grammar follow-set contexts), goals, and cross-cutting invariants (range validity, repeated-request stability, boundary positions, both protocol modes)
  • the tactic and query completion lists are checked against the names documented in doc/*.rst
  • Python ≥ 3.8, standard library only; stdlib-dependent tests skip when no lambdapi stdlib is installed

An earlier didChange-debouncing scheme was dropped to keep the diff reviewable.

@ciaran-matthew-dunne ciaran-matthew-dunne force-pushed the pr/lsp-ux branch 2 times, most recently from 5d5de8c to 51e2a70 Compare July 6, 2026 21:12
@ciaran-matthew-dunne ciaran-matthew-dunne changed the title feat(lsp): UX additions — completions, debouncing, outlines, tests LSP: completion, document outline, didChange debouncing, tests Jul 6, 2026
@ciaran-matthew-dunne ciaran-matthew-dunne marked this pull request as ready for review July 6, 2026 21:26
fblanqui
fblanqui reviewed Jul 8, 2026
View reviewed changes

@fblanqui fblanqui left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for your PR!

What is the empty file tests/lsp/init.py for?

Comment thread tests/lsp/README.md
- `source.py` — pattern-based position finder for fixtures
- `base.py` — `LSPTestCase` with per-test server + fixture helpers
- `fixtures/*.lp` — small focused test documents
- `test_*.py` — one file per LSP concern (lifecycle, diagnostics, …)

@fblanqui fblanqui Jul 8, 2026

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not all py files are listed here.

@ciaran-matthew-dunne

ciaran-matthew-dunne commented Jul 8, 2026

Copy link
Copy Markdown
Contributor Author

Still working on this now. Give me 30min.

@ciaran-matthew-dunne ciaran-matthew-dunne changed the title LSP: completion, document outline, didChange debouncing, tests LSP: completion, document outline, documentation hovers, tests Jul 8, 2026
@ciaran-matthew-dunne

ciaran-matthew-dunne commented Jul 8, 2026

Copy link
Copy Markdown
Contributor Author

More or less ready for review. May change some things tomorrow morning.
Removed changes to the stdin buffer that were previously included in this PR.

@ciaran-matthew-dunne ciaran-matthew-dunne force-pushed the pr/lsp-ux branch 3 times, most recently from dcbd946 to 1a18a32 Compare July 9, 2026 15:00
@ciaran-matthew-dunne
parser: map a bare open to P_open again
4d9e95d 
A bare open (not preceded by require) was parsed as require open
since the LL(1) parser rework (Deducteam#1441), silently loading not yet
required modules instead of failing, and pretty-printing back as
require open.
@ciaran-matthew-dunne
LSP: success hints on the ";" of commands and the keyword of tactics
070c614 
The severity-4 "OK" diagnostic of a command or tactic previously spanned
the whole command or tactic, so the success underline covered symbol
bodies, rule right-hand sides and whole proofs. Instead:

- A command's hint is shown on its terminating ";". The command's
  recorded position stops one character before it (the parser's
  extend_pos), so lp_doc derives the ";" position from it (at_semicolon).

- Symbol declarations always create proof data, so their "OK" went
  through the proof path and landed on the symbol name. The initial
  goals stay anchored at the symbol (for the goals panel), but the
  visible hint now goes on the ";".

- A tactic's hint is shown on its leading keyword (Syntax.tactic_keyword,
  exposed as Pure.Tactic.keyword), since a tactic's end is ill-defined
  once it has subproofs. These diagnostics also anchor the goals panel,
  whose lookup (closest_before) only reads the start of each position,
  which does not move.

Also rename the lp_doc node field "ast" to "cmd".
@ciaran-matthew-dunne
LSP: review fixes for success hint positions
b490ace 
Set the character offsets of hint positions consistently with their
columns (at_keyword left end_offset at the end of the whole tactic,
at_semicolon did not update offsets at all).

Handle a ";" at the beginning of a line: the parser's extend_pos does
not back up at column 0, so a command position with end_col = 0 cannot
distinguish a ";" at column 0 from one at column 1 (the hint used to
underline column 1, one character past a line-initial ";"). Cover both
columns in that case.
@ciaran-matthew-dunne
LSP: show command success hints on the introducing keyword
1e2e768 
Show the "OK" hint of a command on its keyword ("symbol", "rule",
"require", ...) rather than on the terminating ";".

The keyword of a symbol, inductive or open command is not always at
the command's start (modifiers or parameters may precede it), so the
parser records the keyword position in the AST for these three
constructors. For the other commands, Syntax.command_keyword_pos
computes it as a prefix of the command's position. Tactics use the
same mechanism (tactic_keyword_pos); at_keyword and at_semicolon
disappear from lp_doc, replaced by Pos.prefix.
@ciaran-matthew-dunne
LSP groundwork: expose command AST, module-path ranges, printer state
d194bc4 
Additions to the pure/parsing API for the LSP server:
- Syntax.fold_paths and Pure.path_rangemap map the source ranges of
  require/open module paths; Lp_doc stores this path range map
  alongside the identifier range map
- Pure.Command.get_elt exposes the parser-level command shape so
  clients can pattern-match on declaration forms (outlines)
- Pure.set_print_state installs a document's signature state in the
  printer for correctly qualified output
@ciaran-matthew-dunne ciaran-matthew-dunne force-pushed the pr/lsp-ux branch 2 times, most recently from fcc3b0d to bdd0076 Compare July 9, 2026 18:56
@ciaran-matthew-dunne
LSP: robust message framing and JSON-RPC replies
e4329be 
- read header lines up to the blank separator, accepting Content-Length
  in any position (clients may send Content-Type too)
- keep request ids verbatim (JSON-RPC ids are numbers or strings,
  including 0) and echo them back as-is; key the crash-recovery null
  reply on the presence of the id field
- reply MethodNotFound (-32601) to unknown request methods so clients
  do not wait forever; unknown notifications are logged and dropped
- didChange: apply all content changes of a message, then re-check once
@ciaran-matthew-dunne
LSP: initialize reads workspace folders and client capabilities
dc8d492 
- apply the workspace's lambdapi.pkg before the first document opens,
  from rootUri (pre-3.6 clients) and workspaceFolders, deduplicated —
  clients typically send both for the same directory; a package-config
  failure is logged, never fatal (the client would kill the server and
  retry in a loop)
- record snippetSupport, hierarchicalDocumentSymbolSupport and the
  completion documentationFormat, for the handlers that gate on them
@ciaran-matthew-dunne
LSP: hierarchical document symbols
5ebb4b4 
- when the client supports it, answer documentSymbol with a
  DocumentSymbol[] tree built from the parsed AST: symbol declarations,
  and inductive types with their constructors as children; the flat
  SymbolInformation[] list remains the fallback
- drop the kind classification: no LSP SymbolKind matches lambdapi's
  notions (axiom, constructor, definable symbol, theorem, ...), so
  every symbol reports the least surprising kind, Function
@ciaran-matthew-dunne
LSP: go-to-definition on module paths, with in-scope fallback
62a0931 
- the module paths of require/open commands jump to the start of that
  module's file (via the path range map added with the groundwork)
- when the identifier map has no resolvable entry at the cursor, look
  up the raw token under the cursor (code-point aware) in the in-scope
  symbol table: definition keeps working in mid-edit text and in code
  past a parse error
@ciaran-matthew-dunne
LSP: keyword documentation and hypothesis types on hover
eec0202 
- documentation for tactic keywords (inside proofs) and for command
  and query keywords and modifiers, sourced from doc/*.rst; the tables
  carry (name, detail, doc, snippet) so completion can reuse them
- types of the hypotheses introduced by assume, from the goal
  snapshots; names in a tactic's arguments resolve in the state before
  the tactic runs (snapshots are post-tactic, so a tactic that closes
  its subgoal or the proof used to lose its own arguments' hypotheses)
- types print with the document's own printer state (set_print_state),
  not whichever document's notations were installed last
- fallback to the token under the cursor when the identifier map
  misses: keyword docs, hypotheses and in-scope symbols hover in
  mid-edit text and past parse errors; the proof context of a broken
  edit comes from the nodes of the last parse-error-free check
  (good_nodes)
@ciaran-matthew-dunne
parser: expose the tokens acceptable at the end of a source prefix
ced33a1 
- expected-token recordings accumulate until the next consumed token
  instead of overwriting one another, and a finished application
  records that a term can be continued (a further argument, an arrow):
  syntax errors now list more of the true alternatives, with the full
  set of term starters rendered as one word: a term
- new entry point Parser.Lp.expected_tokens (exposed as
  Pure.expected_tokens): parse a source prefix and return the tokens
  the grammar accepts at its end — the command starters between
  commands, the follow set of the truncated command within one, [] on
  a syntax error before the end.  This is the follow set LSP
  completion is built on
@ciaran-matthew-dunne
LSP: grammar-driven completion
34b2afa 
- in-scope symbols (ghost symbols excluded; no completion kind — the
  LSP kinds don't match lambdapi's notions), offered only where the
  grammar accepts an identifier reference, never in binder positions;
  per-item type details attach lazily on completionItem/resolve
- keyword membership comes from the parser's follow sets: exactly the
  keywords the grammar accepts at the cursor are offered, with docs
  and snippets from the hover tables; when the prefix does not parse
  (a broken edit earlier in the file), fall back to the context-blind
  tables — tactics and proof enders inside proofs, command keywords
  outside, queries in both
- "." as trigger character: module paths after require/open (as a
  textEdit — "." is not a word character), qualified names after M.
  (the non-private symbols of that module, resolving require-as
  aliases; new Pure.get_aliases), flag names inside flag "..."
- hypotheses of the focused goal complete inside proofs, ranked first
  in the argument of apply, rewrite, etc.; already-typed modifiers are
  filtered from the offers
@ciaran-matthew-dunne
LSP: integration test suite (make test_lsp)
4e13d2c 
- Python tests speaking JSON-RPC over stdio to a lambdapi lsp
  subprocess: lifecycle, diagnostics, document symbols, hover,
  definition, completion (including the grammar follow-set contexts),
  goals, incremental changes, and cross-cutting invariants (range
  validity, repeated-request stability, boundary positions, both
  protocol modes)
- the tactic and query completion lists are checked against the names
  documented in doc/*.rst, so the tables cannot silently fall behind
- Python >= 3.8, standard library only; stdlib-dependent tests skip
  when no lambdapi stdlib is installed; runs as part of make test
@ciaran-matthew-dunne
add CHANGES.md entry
f235ea5
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@fblanqui fblanqui fblanqui left review comments

At least 1 approving review is required to merge this pull request.

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@ciaran-matthew-dunne @fblanqui