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: | diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index 4f22860d5..ea7a9ae5a 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 @@ -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 diff --git a/language-server/dm/dune b/language-server/dm/dune index e26bf4e95..66db22dbb 100644 --- a/language-server/dm/dune +++ b/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"))))) 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..d781adb82 --- /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 + | [_;_;_] 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 () 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"))))) 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"