From b03711803d833a1dfdeffb2cb15ecdd8bcbdb398 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 18 Dec 2024 10:04:26 +0100 Subject: [PATCH 1/7] support lsp >= 1.19 --- language-server/dm/documentManager.ml | 8 +++++++- language-server/dm/dune | 2 +- language-server/vscoq-language-server.opam | 2 +- 3 files changed, 9 insertions(+), 3 deletions(-) diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index 4f22860d5..04720a7b3 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -134,6 +134,12 @@ let observe_id_range st = let is_parsing st = st.document_state = Parsing +[%%if lsp = "1.5" || lsp = "1.6" || lsp = "1.7" || lsp = "1.8" || lsp = "1.9" || lsp = "1.10" || lsp = "1.11" || lsp = "1.12" || lsp = "1.13" || lsp = "1.14" || lsp = "1.15" || lsp = "1.16" || lsp = "1.17" || lsp = "1.18" ] +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 +151,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 = diff --git a/language-server/dm/dune b/language-server/dm/dune index e26bf4e95..1c086a620 100644 --- a/language-server/dm/dune +++ b/language-server/dm/dune @@ -2,7 +2,7 @@ (name dm) (public_name vscoq-language-server.dm) (modules :standard \ vscoqtop_proof_worker vscoqtop_tactic_worker) - (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")")) + (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\") ~lsp:(Defined \"%{version:lsp}\")")) (libraries base coq-core.sysinit coq-core.vernac coq-core.parsing lsp sel protocol language)) (executable diff --git a/language-server/vscoq-language-server.opam b/language-server/vscoq-language-server.opam index 7c75e16fe..46f09b35f 100644 --- a/language-server/vscoq-language-server.opam +++ b/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" From 15485556ece4be464a2e65142d0fe9aef41ecf28 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 18 Dec 2024 10:11:02 +0100 Subject: [PATCH 2/7] debug for nix --- language-server/dm/documentManager.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index 04720a7b3..9a745dcb4 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -134,7 +134,7 @@ let observe_id_range st = let is_parsing st = st.document_state = Parsing -[%%if lsp = "1.5" || lsp = "1.6" || lsp = "1.7" || lsp = "1.8" || lsp = "1.9" || lsp = "1.10" || lsp = "1.11" || lsp = "1.12" || lsp = "1.13" || lsp = "1.14" || lsp = "1.15" || lsp = "1.16" || lsp = "1.17" || lsp = "1.18" ] +[%%if (show lsp) = "1.5" || lsp = "1.6" || lsp = "1.7" || lsp = "1.8" || lsp = "1.9" || lsp = "1.10" || lsp = "1.11" || lsp = "1.12" || lsp = "1.13" || lsp = "1.14" || lsp = "1.15" || lsp = "1.16" || lsp = "1.17" || lsp = "1.18" ] let message_of_string x = x [%%else] let message_of_string x = `String x From 0d0e68ae872641ac961caaf467de52a26bab5714 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 18 Dec 2024 10:45:25 +0100 Subject: [PATCH 3/7] parse lsp version with a dedicated command --- language-server/dm/documentManager.ml | 4 +++- language-server/dm/dune | 12 +++++++++++- language-server/etc/dune | 7 +++++++ language-server/etc/version_parser.ml | 19 +++++++++++++++++++ 4 files changed, 40 insertions(+), 2 deletions(-) create mode 100644 language-server/etc/dune create mode 100644 language-server/etc/version_parser.ml diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index 9a745dcb4..8792daf43 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -12,6 +12,8 @@ (* *) (**************************************************************************) +[%%import "vscoq_config.mlh"] + open Lsp.Types open Protocol open Protocol.LspWrapper @@ -134,7 +136,7 @@ let observe_id_range st = let is_parsing st = st.document_state = Parsing -[%%if (show lsp) = "1.5" || lsp = "1.6" || lsp = "1.7" || lsp = "1.8" || lsp = "1.9" || lsp = "1.10" || lsp = "1.11" || lsp = "1.12" || lsp = "1.13" || lsp = "1.14" || lsp = "1.15" || lsp = "1.16" || lsp = "1.17" || lsp = "1.18" ] +[%%if lsp < (1,19,0) ] let message_of_string x = x [%%else] let message_of_string x = `String x diff --git a/language-server/dm/dune b/language-server/dm/dune index 1c086a620..66db22dbb 100644 --- a/language-server/dm/dune +++ b/language-server/dm/dune @@ -2,7 +2,7 @@ (name dm) (public_name vscoq-language-server.dm) (modules :standard \ vscoqtop_proof_worker vscoqtop_tactic_worker) - (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\") ~lsp:(Defined \"%{version:lsp}\")")) + (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")")) (libraries base coq-core.sysinit coq-core.vernac coq-core.parsing lsp sel protocol language)) (executable @@ -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"))))) diff --git a/language-server/etc/dune b/language-server/etc/dune new file mode 100644 index 000000000..6e3e7b3dd --- /dev/null +++ b/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) + ) \ No newline at end of file diff --git a/language-server/etc/version_parser.ml b/language-server/etc/version_parser.ml new file mode 100644 index 000000000..a9d0103cb --- /dev/null +++ b/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 + | 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 () From 562ccb0da24fecb7f00c0e92a4081fb3f9b12e03 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 18 Dec 2024 10:48:46 +0100 Subject: [PATCH 4/7] version_parser: ensure triple --- language-server/etc/version_parser.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/language-server/etc/version_parser.ml b/language-server/etc/version_parser.ml index a9d0103cb..d781adb82 100644 --- a/language-server/etc/version_parser.ml +++ b/language-server/etc/version_parser.ml @@ -9,7 +9,7 @@ let main () = (* sanitization *) let l = match l with - | l when List.for_all is_number l -> l + | [_;_;_] 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 From 346abfc51d76b58d0a2dc97abe5a7331ac7e8e04 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 18 Dec 2024 21:09:04 +0100 Subject: [PATCH 5/7] fix tests --- language-server/tests/common.ml | 12 ++++++++++-- language-server/tests/dune | 11 +++++++++++ 2 files changed, 21 insertions(+), 2 deletions(-) diff --git a/language-server/tests/common.ml b/language-server/tests/common.ml index 4ab84e8be..01645e9d8 100644 --- a/language-server/tests/common.ml +++ b/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) = diff --git a/language-server/tests/dune b/language-server/tests/dune index 1e1c5b904..5890a21c3 100644 --- a/language-server/tests/dune +++ b/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"))))) From 75c114774563d7da5d8669fbe99fc75504558e39 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 19 Dec 2024 09:48:33 +0100 Subject: [PATCH 6/7] [hack] install recent dune --- .github/workflows/ci.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 25db69618..10bf25ef7 100644 --- a/.github/workflows/ci.yml +++ b/.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: | From 462734353ac512b677594c16679aa603b44d7656 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 19 Dec 2024 10:56:35 +0100 Subject: [PATCH 7/7] do not move cursor or flash red in continuous mode --- language-server/dm/documentManager.ml | 25 +++++++++++++++---------- 1 file changed, 15 insertions(+), 10 deletions(-) diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index 8792daf43..ea7a9ae5a 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -103,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 = @@ -321,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 } @@ -562,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