Merge branch 'main' into v9.1

Author: ejgallego

CHANGES.md

@@ -1,5 +1,5 @@
-unreleased
-----------
+# coq-lsp 0.2.4: (W)Activation
+------------------------------
 
  - [js] [deps] Bump to findlib 1.9.8, use vanilla API for loading and
    remove our own local wrapper (@ejgallego, #975).
@@ -53,6 +53,14 @@ unreleased
  - [coq] incorporate experimental `coq-layout-engine` printer, both in
    client and server parts (@ejgallego, #668, see also #72 and
    https://github.com/jscoq/jscoq/pull/282 )
+ - [lsp] [code] New notification `$/coq/executionInformation` which
+   will signal clients when rocq-lsp does intent to start to execute a
+   sentence. Experimentally, this is used to provide a red glow on
+   long-running commands in coq-lsp/VSCode, to provide better user
+   feedback on long-running commands (@ejgallego, suggested by
+   @jpoiret, #1002)
+ - [lsp] [outline] Support `Notation`, `Ltac` and `Ltac Notation` in
+   outline entries (@ejgallego, #1025, fixes #632)
 
 # coq-lsp 0.2.3: Barrage
 ------------------------

CONTRIBUTING.md

@@ -410,11 +410,12 @@ The checklist for the release as of today is the following:
 
 ### Prepare a release commit
 
-- update the version number at `editor/code/package.json`, do `npm i`
-- update the version number at `fleche/version.ml`
 - update the client changelog at `editor/code/CHANGELOG.md`, commit
+- update the version number at `lsp-server/wasm/package.json`
+- update the version number at `editor/code/package.json`
+- do `make extension` to update the `package-lock.json` files
+- update the version number at `fleche/version.ml`
 - add release notes in `etc/release_notes/` if needed
-- do `make extension` to update the `package-lock.json` file
 
 ### Tag and test release commit
 

compiler/output.ml

@@ -27,6 +27,7 @@ module Fcc_verbose = struct
 
   let serverVersion _ = ()
   let serverStatus _ = ()
+  let execInfo ~uri:_ ~version:_ ~range:_ = ()
 
   let cb =
     Fleche.Io.CallBack.
@@ -37,6 +38,7 @@ module Fcc_verbose = struct
       ; perfData
       ; serverVersion
       ; serverStatus
+      ; execInfo
       }
 end
 

controller/lsp_core.ml

@@ -827,6 +827,9 @@ struct
   let serverVersion vi = Lsp.JFleche.mk_serverVersion vi |> ofn
   let serverStatus st = Lsp.JFleche.mk_serverStatus st |> ofn
 
+  let execInfo ~uri ~version ~range =
+    Lsp.JFleche.mk_execinfo ~uri ~version ~range |> ofn
+
   let cb =
     Fleche.Io.CallBack.
       { trace
@@ -836,5 +839,6 @@ struct
       ; perfData
       ; serverVersion
       ; serverStatus
+      ; execInfo
       }
 end

coq-layout-engine/boxModel.ml

@@ -72,7 +72,7 @@ module H = Tyxml.Html
 
 module Render = struct
   let xxx kind = H.txt ("uninplemented: " ^ kind)
-  let _class c = [ H.a_class [ c ] ]
+  let _class c = [ H.a_class [ c; "box" ] ]
 
   let span ?(extra = []) c e =
     let a = _class c in

coq-layout-engine/dune

@@ -1,4 +1,8 @@
 (library
  (name layout)
  (public_name coq-lsp.layout-printer)
- (libraries rocq-runtime.interp rocq-runtime.parsing rocq-runtime.printing tyxml))
+ (libraries
+  rocq-runtime.interp
+  rocq-runtime.parsing
+  rocq-runtime.printing
+  tyxml))

coq/ast.ml

@@ -151,7 +151,7 @@ module Kinds = struct
   let enumMember = 22
   let struct_ = 23
   let _event = 24
-  let _operator = 25
+  let operator = 25
   let _typeParameter = 26
 end
 
@@ -233,6 +233,9 @@ let mk_name ~lines (id : Names.lname) : Lang.Ast.Name.t Lang.With_range.t =
 let mk_id ~lines (id : Names.lident) =
   CAst.map (fun id -> Names.Name id) id |> mk_name ~lines
 
+let mk_string ~lines (id : Names.lstring) =
+  CAst.map (fun id -> Names.(Name (Id.of_string_soft id))) id |> mk_name ~lines
+
 let constructor_info ~lines ((_, (id, _typ)) : constructor_expr) =
   let range = Option.get id.loc in
   let range = Utils.to_range ~lines range in
@@ -300,6 +303,11 @@ let symbol_info ~lines ~range
   in
   List.map mk_info idents
 
+let fixup_range ~loc id =
+  match id.loc with
+  | None -> CAst.make ?loc id.v
+  | Some _ -> id
+
 let make_info ~st:_ ~lines CAst.{ loc; v } : Lang.Ast.Info.t list option =
   let open Vernacexpr in
   match loc with
@@ -339,4 +347,36 @@ let make_info ~st:_ ~lines CAst.{ loc; v } : Lang.Ast.Info.t list option =
       let kind = Kinds.method_ in
       let detail = "Rewrite Rule" in
       Some [ Lang.Ast.Info.make ~range ~name ~kind ~detail () ]
+    | VernacSynterp (VernacNotation (_infix, { ntn_decl_string; _ })) ->
+      let name = mk_string ~lines ntn_decl_string in
+      let kind = Kinds.operator in
+      let detail = "Notation" in
+      Some [ Lang.Ast.Info.make ~range ~name ~kind ~detail () ]
+    | VernacSynterp
+        (VernacExtend
+          ({ ext_entry = "VernacDeclareTacticDefinition"; _ }, glist)) ->
+      let ids =
+        List.concat_map Serlib.Ser_analysis.NameAnalysis.analyze glist
+      in
+      let kind = Kinds.function_ in
+      let detail = "Tactic" in
+      let mk_info id =
+        let name = mk_name ~lines id in
+        Lang.Ast.Info.make ~range ~name ~detail ~kind ()
+      in
+      Some (List.map mk_info ids)
+    | VernacSynterp
+        (VernacExtend ({ ext_entry = "VernacTacticNotation"; _ }, glist)) ->
+      let ids =
+        List.concat_map Serlib.Ser_analysis.NameAnalysis.analyze glist
+      in
+      let kind = Kinds.function_ in
+      let detail = "Tactic Notation" in
+      let mk_info id =
+        (* Tactic notation doesn't properly set id location *)
+        let id = fixup_range ~loc id in
+        let name = mk_name ~lines id in
+        Lang.Ast.Info.make ~range ~name ~detail ~kind ()
+      in
+      Some (List.map mk_info ids)
     | _ -> None)

editor/code/CHANGELOG.md

@@ -1,3 +1,19 @@
+# coq-lsp 0.2.4: (W)Activation
+------------------------------
+
+ - The coq-lsp extension now includes a fully working rocq-lsp
+   compiled with WebAssembly. This means you can run Rocq without
+   having to install it, directly from `vscode.dev` or `github.dev`
+
+   This was made possible thanks to Shachar Itzhaky's excellent
+   `ocaml-wasm`.
+ - Sentences that take long to execute will be highlighted with a red
+   glowing on the client.
+ - Support for Rocq 9.1, `_RocqProject`, `rocq` markdown and LaTeX
+   codeblocks.
+ - Document outline now supports `Notation`, `Ltac`, and `Ltac
+   Notation`.
+
 # coq-lsp 0.2.3: Barrage
 ------------------------
 

editor/code/lib/types.ts

@@ -228,3 +228,9 @@ export interface PetRunParams {
   st: number;
   tac: string;
 }
+
+// Exec Info
+export interface ExecutionInfoParams {
+  textDocument: VersionedTextDocumentIdentifier;
+  range: Range;
+}