support lsp >= 1.19

.github/workflows/ci.yml

@@ -153,7 +153,8 @@ jobs:
         OPAMYES: true
       run: |
         opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
-        opam install ./language-server/vscoq-language-server.opam --deps-only --with-doc --with-test
+        opam install dune
+        opam install ./language-server/vscoq-language-server.opam --deps-only --with-doc --with-test --ignore-constraints-on dune
 
     - name: Build vscoq-language-server
       run: |

language-server/dm/documentManager.ml

@@ -12,6 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+[%%import "vscoq_config.mlh"]
+
 open Lsp.Types
 open Protocol
 open Protocol.LspWrapper
@@ -101,15 +103,20 @@ let mk_observe_event id =
 let mk_move_cursor_event id = 
   let priority = PriorityManager.move_cursor in
   Sel.now ~priority @@ SendMoveCursor id
-let mk_block_on_error_event last_range error_id =
-  let priority = PriorityManager.move_cursor in
-  let event = Sel.now ~priority @@ SendBlockOnError error_id in
-  match last_range with
-  | None ->
-    [event] @ [mk_proof_view_event error_id]
-  | Some range ->
-    [event] @ [mk_move_cursor_event range] @ [mk_proof_view_event error_id]
 
+let mk_block_on_error_event last_range error_id background =
+  let update_goal_view = [mk_proof_view_event error_id] in
+  if background then
+    update_goal_view
+  else
+    let red_flash =
+      [Sel.now ~priority:PriorityManager.move_cursor @@ SendBlockOnError error_id] in
+    let move_cursor =
+      match last_range with
+      | Some last_range -> [mk_move_cursor_event last_range]
+      | None -> [] in
+    red_flash @ move_cursor @ update_goal_view
+
 type events = event Sel.Event.t list
 
 let executed_ranges st mode =
@@ -134,6 +141,12 @@ let observe_id_range st =
 
 let is_parsing st =  st.document_state = Parsing
 
+[%%if lsp < (1,19,0) ]
+let message_of_string x = x
+[%%else]
+let message_of_string x = `String x
+[%%endif]
+
 let make_diagnostic doc range oloc message severity code =
   let range =
     match oloc with
@@ -145,7 +158,7 @@ let make_diagnostic doc range oloc message severity code =
     match code with
     | None -> None, None
     | Some (x,z) -> Some x, Some z in
-  Diagnostic.create ?code ?data ~range ~message ~severity ()
+  Diagnostic.create ?code ?data ~range ~message:(message_of_string message) ~severity ()
 
 let mk_diag st (id,(lvl,oloc,qf,msg)) =
   let code = 
@@ -313,7 +326,7 @@ let observe ~background state id ~should_block_on_error : (state * event Sel.Eve
         {state with execution_state}, []
       | Some (error_id, loc) ->
         let state, error_range = state_before_error state error_id loc in
-        let events = mk_block_on_error_event error_range error_id in
+        let events = mk_block_on_error_event error_range error_id background in
         {state with execution_state}, events
 
 let reset_to_top st = { st with observe_id = Top }
@@ -554,7 +567,7 @@ let execute st id vst_for_next_todo started task background block =
       | None -> st, []
       | Some (error_id, loc) -> 
         let st, error_range = state_before_error st error_id loc in
-        let events = if block then mk_block_on_error_event error_range error_id else [] in
+        let events = if block then mk_block_on_error_event error_range error_id background else [] in
         st, events
       in
     let event = Option.map (fun task -> create_execution_event background (Execute {id; vst_for_next_todo; task; started })) next in

language-server/dm/dune

@@ -21,4 +21,14 @@
  (flags -linkall)
  (package vscoq-language-server)
  (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")"))
+ (preprocessor_deps vscoq_config.mlh)
  (libraries coq-core.sysinit coq-core.tactics lsp dm protocol))
+
+(rule
+  (target vscoq_config.mlh)
+  (action (with-stdout-to %{target}
+    (progn
+      (echo "(* Automatically generated, don't edit *)\n")
+      (echo "[%%define lsp ")
+      (run vscoq_version_parser %{version:lsp})
+      (echo "]\n")))))

language-server/etc/dune

@@ -0,0 +1,7 @@
+(executable
+ (name version_parser)
+ (public_name vscoq_version_parser)
+ (modules version_parser)
+ (libraries str)
+ (package vscoq-language-server)
+ )

language-server/etc/version_parser.ml

@@ -0,0 +1,19 @@
+
+let is_number x = try let _ = int_of_string x in true with _ -> false ;;
+
+let main () =
+  let v = Sys.argv.(1) in
+  let v' = Str.(replace_first (regexp "^v") "" v) in     (* v1.20... -> 1.20... *)
+  let v' = Str.(replace_first (regexp "-.*$") "" v') in  (* ...-10-fjdnfs -> ... *)
+  let l = String.split_on_char '.' v' in
+  (* sanitization *)
+  let l =
+    match l with
+    | [_;_;_] as l when List.for_all is_number l -> l
+    | [_] -> ["99";"99";"99"]
+    | _ -> Printf.eprintf "version_parser: cannot parse: %s\n" v; exit 1 in
+  let open Format in
+  printf "(%a)%!" (pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt ", ") pp_print_string) l
+;;
+
+main ()

language-server/tests/common.ml

@@ -12,11 +12,19 @@
 (*                                                                        *)
 (**************************************************************************)
 
+[%%import "vscoq_config.mlh"]
+
 open Dm
 open Base
 open Types
 open Protocol.LspWrapper
 
+[%%if lsp < (1,19,0) ]
+let string_of_message x = x
+[%%else]
+let string_of_message = function `String x -> x | _ -> assert false
+[%%endif]
+
 [%%if coq = "8.18" || coq = "8.19" || coq = "8.20"]
 let injections =
   Coqinit.init_ocaml ();
@@ -180,7 +188,7 @@ type diag_spec =
 
 let check_no_diag st =
   let diagnostics = DocumentManager.all_diagnostics st in
-  let diagnostics = List.map ~f:Lsp.Types.Diagnostic.(fun d -> d.range, d.message, d.severity) diagnostics in
+  let diagnostics = List.map ~f:Lsp.Types.Diagnostic.(fun d -> d.range, string_of_message d.message, d.severity) diagnostics in
   [%test_pred: (Range.t * string * DiagnosticSeverity.t option) list] List.is_empty diagnostics
 
 type diagnostic_summary = Range.t * string * DiagnosticSeverity.t option [@@deriving sexp]
@@ -189,7 +197,7 @@ let check_diag st specl =
   let open Result in
   let open Lsp.Types.Diagnostic in
   let diagnostic_summary { range; message; severity } =
-    let message = Str.global_replace (Str.regexp_string "\n") " " message in
+    let message = Str.global_replace (Str.regexp_string "\n") " " (string_of_message message) in
     let message = Str.global_replace (Str.regexp " Raised at .*$") "" message in
     (range, message, severity) in
   let match_diagnostic r s rex (range, message, severity) =

language-server/tests/dune

@@ -3,4 +3,15 @@
   (libraries base dm protocol)
   (preprocess
     (pps ppx_sexp_conv ppx_inline_test ppx_assert ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")"))
+    (preprocessor_deps vscoq_config.mlh)
   (inline_tests))
+
+
+ (rule
+  (target vscoq_config.mlh)
+  (action (with-stdout-to %{target}
+    (progn
+      (echo "(* Automatically generated, don't edit *)\n")
+      (echo "[%%define lsp ")
+      (run vscoq_version_parser %{version:lsp})
+      (echo "]\n")))))

language-server/vscoq-language-server.opam

@@ -27,7 +27,7 @@ depends: [
   "ppx_import"
   "ppx_optcomp"
   "result" { >= "1.5" }
-  "lsp" { >= "1.15" < "1.19"}
+  "lsp" { >= "1.15"}
   "sel" {>= "0.4.0"}
 ]
 synopsis: "VSCoq language server"