LSP: completion, document outline, documentation hovers, tests

.gitignore

@@ -21,3 +21,5 @@ libraries/zenon_modulo
 .DS_Store
 *.map
 *.log
+__pycache__/
+*.pyc

CHANGES.md

@@ -22,6 +22,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 - Tactic `#print` to print a symbol or the current goal.
 - Export to Lean.
 - Tactic `all_hyps t` calls parameterized tactic term t on all hypotheses ignoring failing calls.
+- LSP server: completion (in-scope symbols; command keywords with snippets; inside proofs, documented tactic keywords and the local symbols introduced by `assume`), documentation on hover for tactics, command keywords and modifiers, hover on `assume`-introduced local symbols showing their types, hierarchical document symbols, go-to-definition on `require`/`open` module paths, hover/go-to-definition fallback to in-scope symbols in unchecked regions, and an integration test suite (`make test_lsp`).
+- LSP server: context-aware completion, with `.` as a trigger character: module paths after `require`/`open`, qualified identifiers (symbols of the required module, resolving `require as` aliases), notation/associativity/flag arguments, and hypothesis-first ranking in the argument of `apply`, `rewrite`, etc.
+- LSP server: keyword completions are driven by the parser's follow sets: at any cursor position, exactly the keywords the grammar accepts there are offered (`open`/`private`/`as` after `require`, `rule` after `simplify`, `begin` after a statement's type, etc.), and symbols are only offered where a term or identifier reference can appear. New parser entry point `Parser.Lp.expected_tokens` returning the acceptable tokens at the end of a source prefix; parser error messages list more of the acceptable alternatives and render term starters as "a term".
 
 ### Changed
 
@@ -36,6 +39,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 
 ### Fixed
 
+- A bare `open` (not preceded by `require`) was parsed as `require open`
+  since the parser rework, silently loading not yet required modules
+  instead of failing.
 - Convertibility test of non-linear higher-order pattern variables in rule LHS.
 - Syntactical errors in Dedukti export.
 - Weak head normal form test.
@@ -49,6 +55,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
   duplicated directory component.
 - LSP server: go-to-definition and hover on qualified identifiers, and session
   state leaking between open documents.
+- LSP server: the success ("OK") diagnostic of a command or tactic is now
+  shown on its introducing keyword ("symbol", "rule", "assume", …), instead
+  of underlining the whole command or tactic (symbol body, rule right-hand
+  side, proof, etc.).
 
 ## 3.0.0 (2025-07-16)
 

Makefile

@@ -36,6 +36,11 @@ test_all: test
 test: lambdapi
 	@dune runtest
 	@tests/dtrees.sh
+	@$(MAKE) test_lsp
+
+.PHONY: test_lsp
+test_lsp: lambdapi
+	@python3 -m tests.lsp
 
 .PHONY: test_load
 test_load: lambdapi

src/cli/lambdapi.ml

@@ -28,7 +28,8 @@ let sig_state_of_require l : Sig_state.sig_state =
     Handle.Command.handle Compile.compile ss
      (Pos.none
       (Parsing.Syntax.P_require
-        (Some false, [Pos.none (Parsing.Parser.path_of_string req)]))))
+        (Some false,
+         [Pos.none (Parsing.Parser.path_of_string req)]))))
   Core.Sig_state.dummy l
 
 let search_cmd cfg rules require s dbpath_opt =

src/common/pos.ml

@@ -111,6 +111,16 @@ let cat : popt -> popt -> popt = fun p1 p2 ->
   | None, Some p -> Some p
   | None, None -> None
 
+(** [prefix n p] is the sub-position of [p] covering only its first [n]
+    characters, which are assumed to lie on the first line of [p] and to be
+    ASCII (so that [n] is both a column count and a character count). *)
+let prefix : int -> popt -> popt = fun n p ->
+  match p with
+  | None -> None
+  | Some p -> Some { p with end_line = p.start_line
+                          ; end_col = p.start_col + n
+                          ; end_offset = p.start_offset + n }
+
 (** [shift k p] returns a position that is [k] characters after [p]. *)
 let shift : int -> popt -> popt = fun k p ->
   match p with

src/export/coq.ml

@@ -114,9 +114,9 @@ and typopt oc t = Option.iter (prefix " : " term oc) t
 
 let command oc {elt; pos} =
   begin match elt with
-  | P_open(true,ps) ->
+  | P_open(_,true,ps) ->
       string oc "Import "; list path " " oc ps; string oc ".\n"
-  | P_open(false,ps) ->
+  | P_open(_,false,ps) ->
       string oc "Export "; list path " " oc ps; string oc ".\n"
   | P_require (None, ps) ->
       string oc "Require "; list path " " oc ps; string oc ".\n"
@@ -129,7 +129,7 @@ let command oc {elt; pos} =
     string oc "Module "; ident oc i; string oc " := "; path oc p;
     string oc ".\n"
   | P_symbol
-    { p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ;
+    { p_sym_mod; p_sym_kw=_; p_sym_nam; p_sym_arg; p_sym_typ;
       p_sym_trm; p_sym_prf=_; p_sym_def } ->
       if not (is_mapped p_sym_nam.elt) then
         begin match p_sym_def, p_sym_trm, p_sym_arg, p_sym_typ with

src/export/lean.ml

@@ -140,7 +140,7 @@ let openings = ref []
 
 let command oc {elt; pos} =
   begin match elt with
-  | P_open(_,ps) -> List.iter (open_mod oc) ps
+  | P_open(_,_,ps) -> List.iter (open_mod oc) ps
   | P_require(b,ps) ->
       List.iter (req_mod oc) ps;
       begin
@@ -149,8 +149,8 @@ let command oc {elt; pos} =
         | _ -> () (*FIXME?*)
       end
   | P_require_as(p,i) -> Stt.alias := StrMap.add i.elt p.elt !Stt.alias
-  | P_symbol { p_sym_mod; p_sym_nam; p_sym_arg; p_sym_typ; p_sym_trm;
-               p_sym_prf=_; p_sym_def } ->
+  | P_symbol { p_sym_mod; p_sym_kw=_; p_sym_nam; p_sym_arg; p_sym_typ;
+               p_sym_trm; p_sym_prf=_; p_sym_def } ->
     if not (is_mapped p_sym_nam.elt) then
         begin match p_sym_def, p_sym_trm, p_sym_arg, p_sym_typ with
           | true, Some t, _, Some a when List.exists is_lem p_sym_mod ->

src/export/rawdk.ml

@@ -198,7 +198,7 @@ let command : p_command pp = fun ppf ({elt; pos} as c) ->
   | P_query q -> query ppf q
   | P_require(None,ps) ->
       List.iter (fun {elt;_} -> out ppf "#REQUIRE %a@." Dk.mident elt) ps
-  | P_symbol{p_sym_mod; p_sym_nam=n; p_sym_arg; p_sym_typ;
+  | P_symbol{p_sym_mod; p_sym_kw=_; p_sym_nam=n; p_sym_arg; p_sym_typ;
              p_sym_trm; p_sym_prf=None; p_sym_def=_;} ->
       let ms = partition_modifiers p_sym_mod in
       begin match get_ac_typ pos ms p_sym_arg p_sym_typ with

src/handle/command.ml

@@ -249,7 +249,7 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
   | P_require(bo,ps) ->
       (List.fold_left (handle_require compile bo) ss ps, None, None)
   | P_require_as(p,id) -> (handle_require_as compile ss p id, None, None)
-  | P_open(b,ps) -> (List.fold_left (handle_open b) ss ps, None, None)
+  | P_open(_,b,ps) -> (List.fold_left (handle_open b) ss ps, None, None)
   | P_rules(rs) ->
     (* Scope rules, and check that they preserve typing. Return the list of
        rules [srs] and also a [map] mapping every symbol defined by a rule
@@ -344,7 +344,7 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
       Console.out 2 (Color.gre "coercion %a") sym_rule r;
       (ss, None, None)
 
-  | P_inductive(ms, params, p_ind_list) ->
+  | P_inductive(_, ms, params, p_ind_list) ->
       (* Check modifiers. *)
       let (prop, expo, mstrat, opaq) = handle_modifiers ms in
       if prop <> Defin then
@@ -446,8 +446,8 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
         rec_sym_list;
       (ss, None, None)
 
-  | P_symbol {p_sym_mod;p_sym_nam;p_sym_arg;p_sym_typ;p_sym_trm;p_sym_prf;
-              p_sym_def} ->
+  | P_symbol {p_sym_mod;p_sym_kw=_;p_sym_nam;p_sym_arg;p_sym_typ;p_sym_trm;
+              p_sym_prf;p_sym_def} ->
     (* We check that the identifier is not already used. *)
     let {elt=id; _} = p_sym_nam in
     if Sign.mem ss.signature id then

src/lsp/lp_doc.ml

@@ -22,7 +22,7 @@ module LSP = Lsp_base
 let lp_logger = Buffer.create 100
 
 type doc_node =
-  { ast   : Pure.Command.t
+  { cmd   : Pure.Command.t
   ; exec  : bool
   (*; tactics : Proof.Tactic.t list*)
   ; goals : (Goal.info list * Pos.popt) list
@@ -39,9 +39,17 @@ type t = {
   mutable root  : Pure.state option; (* Only mutated after parsing. *)
   mutable final : Pure.state option; (* Only mutated after parsing. *)
   nodes : doc_node list;
+  (* [nodes] of the last parse-error-free check. A mid-edit text (a
+     partial tactic name, say) fails to parse, dropping the command
+     being edited from [nodes]; queries that need the cursor's command
+     (proof context for completion and hover) fall back to these.
+     Edits happen within a line, so line-based positions stay valid
+     until the next clean parse resyncs them. *)
+  good_nodes : doc_node list;
   (* severity is same as LSP specifications : https://git.io/JiGAB *)
   logs : ((int * string) * Pos.popt) list; (*((severity, message), location)*)
   map : Core.Term.qident RangeMap.t;
+  path_map : Common.Path.t RangeMap.t;
 }
 
 let option_default o1 d =
@@ -63,7 +71,10 @@ let process_pstep (pstate,diags,logs) tac nb_subproofs =
   | Tac_OK (pstate, qres) ->
     let goals = Some (current_goals pstate) in
     let qres = match qres with None -> "OK" | Some x -> x in
-    pstate, (tac_loc, 4, qres, goals) :: diags, logs
+    (* Show the success hint on the tactic's leading keyword only. This
+       tuple also anchors the goals panel (see [get_goals]), whose lookup
+       reads the start of the position: the start must not move. *)
+    pstate, (Tactic.keyword_pos tac, 4, qres, goals) :: diags, logs
   | Tac_Error(loc,msg) ->
     let loc = option_default loc tac_loc in
     let goals = Some (current_goals pstate) in
@@ -83,27 +94,32 @@ let get_goals dg_proof =
   in get_goals_aux [] dg_proof
 (* XXX: Imperative problem *)
 
-let process_cmd _file (nodes,st,dg,logs) ast =
+let process_cmd _file (nodes,st,dg,logs) cmd =
   let open Pure in
   (* let open Timed in *)
   (* XXX: Capture output *)
   (* Console.out_fmt := lp_fmt;
    * Console.err_fmt := lp_fmt; *)
-  let cmd_loc = Command.get_pos ast in
-  let hndl_cmd_res = handle_command st ast in
+  let cmd_loc = Command.get_pos cmd in
+  let hndl_cmd_res = handle_command st cmd in
   let logs = ((3, buf_get_and_clear lp_logger), cmd_loc) :: logs in
   match hndl_cmd_res with
   | Cmd_OK (st, qres) ->
     let qres = match qres with None -> "OK" | Some x -> x in
-    let nodes = { ast; exec = true; goals = [] } :: nodes in
-    let ok_diag = cmd_loc, 4, qres, None in
+    let nodes = { cmd; exec = true; goals = [] } :: nodes in
+    (* Show the success hint on the command's introducing keyword only. *)
+    let ok_diag = Command.keyword_pos cmd, 4, qres, None in
     nodes, st, ok_diag :: dg, logs
   | Cmd_Proof (pst, tlist, thm_loc, qed_loc) ->
     let start_goals = current_goals pst in
     let pst, dg_proof, logs = process_proof pst tlist logs in
-    let dg_proof = (thm_loc, 4, "OK", Some start_goals) :: dg_proof in
-    let goals = get_goals dg_proof in
-    let nodes = { ast; exec = true; goals } :: nodes in
+    (* Initial goals stay anchored at the symbol, for the goals panel. *)
+    let goals =
+      get_goals ((thm_loc, 4, "OK", Some start_goals) :: dg_proof) in
+    let nodes = { cmd; exec = true; goals } :: nodes in
+    (* Visible success hint on the "symbol" keyword, not on the symbol
+       name. *)
+    let dg_proof = (Command.keyword_pos cmd, 4, "OK", None) :: dg_proof in
     let st, dg_proof, logs =
       match end_proof pst with
       | Cmd_OK (st, qres)   ->
@@ -123,7 +139,7 @@ let process_cmd _file (nodes,st,dg,logs) ast =
     nodes, st, dg_proof @ dg, logs
 
   | Cmd_Error(loc, msg) ->
-    let nodes = { ast; exec = false; goals = [] } :: nodes in
+    let nodes = { cmd; exec = false; goals = [] } :: nodes in
     let cmd_loc, loc, diag, log = match cmd_loc, loc with
     | Some l, Some Some l' ->
         if l.fname = l'.fname then
@@ -156,8 +172,10 @@ let new_doc ~uri ~version ~text =
     root;
     final = root;
     nodes = [];
+    good_nodes = [];
     logs = logs;
     map = RangeMap.empty;
+    path_map = RangeMap.empty;
   }
 
 (* XXX: Save on close. *)
@@ -200,5 +218,10 @@ let check_text ~doc =
     | Some(pos,msg) -> logs @ [((1, msg), Some pos)], diags @ [pos,1,msg,None]
   in
   let map = Pure.rangemap cmds in
-  let doc = { doc with nodes; final=Some(final); map; logs } in
+  let path_map = Pure.path_rangemap cmds in
+  let good_nodes =
+    match error with None -> nodes | Some _ -> doc.good_nodes in
+  let doc =
+    { doc with nodes; good_nodes; final=Some(final); map; path_map; logs }
+  in
   doc, LSP.mk_diagnostics ~uri ~version diags