Skip to content

Commit 3402967

Browse files
authored
Merge pull request #970 from coq/bump-dep-on-lsp
support lsp >= 1.19
2 parents 99168d0 + 4627343 commit 3402967

File tree

8 files changed

+84
-15
lines changed

8 files changed

+84
-15
lines changed

.github/workflows/ci.yml

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -153,7 +153,8 @@ jobs:
153153
OPAMYES: true
154154
run: |
155155
opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
156-
opam install ./language-server/vscoq-language-server.opam --deps-only --with-doc --with-test
156+
opam install dune
157+
opam install ./language-server/vscoq-language-server.opam --deps-only --with-doc --with-test --ignore-constraints-on dune
157158
158159
- name: Build vscoq-language-server
159160
run: |

language-server/dm/documentManager.ml

Lines changed: 24 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,8 @@
1212
(* *)
1313
(**************************************************************************)
1414

15+
[%%import "vscoq_config.mlh"]
16+
1517
open Lsp.Types
1618
open Protocol
1719
open Protocol.LspWrapper
@@ -101,15 +103,20 @@ let mk_observe_event id =
101103
let mk_move_cursor_event id =
102104
let priority = PriorityManager.move_cursor in
103105
Sel.now ~priority @@ SendMoveCursor id
104-
let mk_block_on_error_event last_range error_id =
105-
let priority = PriorityManager.move_cursor in
106-
let event = Sel.now ~priority @@ SendBlockOnError error_id in
107-
match last_range with
108-
| None ->
109-
[event] @ [mk_proof_view_event error_id]
110-
| Some range ->
111-
[event] @ [mk_move_cursor_event range] @ [mk_proof_view_event error_id]
112106

107+
let mk_block_on_error_event last_range error_id background =
108+
let update_goal_view = [mk_proof_view_event error_id] in
109+
if background then
110+
update_goal_view
111+
else
112+
let red_flash =
113+
[Sel.now ~priority:PriorityManager.move_cursor @@ SendBlockOnError error_id] in
114+
let move_cursor =
115+
match last_range with
116+
| Some last_range -> [mk_move_cursor_event last_range]
117+
| None -> [] in
118+
red_flash @ move_cursor @ update_goal_view
119+
113120
type events = event Sel.Event.t list
114121

115122
let executed_ranges st mode =
@@ -134,6 +141,12 @@ let observe_id_range st =
134141

135142
let is_parsing st = st.document_state = Parsing
136143

144+
[%%if lsp < (1,19,0) ]
145+
let message_of_string x = x
146+
[%%else]
147+
let message_of_string x = `String x
148+
[%%endif]
149+
137150
let make_diagnostic doc range oloc message severity code =
138151
let range =
139152
match oloc with
@@ -145,7 +158,7 @@ let make_diagnostic doc range oloc message severity code =
145158
match code with
146159
| None -> None, None
147160
| Some (x,z) -> Some x, Some z in
148-
Diagnostic.create ?code ?data ~range ~message ~severity ()
161+
Diagnostic.create ?code ?data ~range ~message:(message_of_string message) ~severity ()
149162

150163
let mk_diag st (id,(lvl,oloc,qf,msg)) =
151164
let code =
@@ -313,7 +326,7 @@ let observe ~background state id ~should_block_on_error : (state * event Sel.Eve
313326
{state with execution_state}, []
314327
| Some (error_id, loc) ->
315328
let state, error_range = state_before_error state error_id loc in
316-
let events = mk_block_on_error_event error_range error_id in
329+
let events = mk_block_on_error_event error_range error_id background in
317330
{state with execution_state}, events
318331

319332
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 =
554567
| None -> st, []
555568
| Some (error_id, loc) ->
556569
let st, error_range = state_before_error st error_id loc in
557-
let events = if block then mk_block_on_error_event error_range error_id else [] in
570+
let events = if block then mk_block_on_error_event error_range error_id background else [] in
558571
st, events
559572
in
560573
let event = Option.map (fun task -> create_execution_event background (Execute {id; vst_for_next_todo; task; started })) next in

language-server/dm/dune

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,4 +21,14 @@
2121
(flags -linkall)
2222
(package vscoq-language-server)
2323
(preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")"))
24+
(preprocessor_deps vscoq_config.mlh)
2425
(libraries coq-core.sysinit coq-core.tactics lsp dm protocol))
26+
27+
(rule
28+
(target vscoq_config.mlh)
29+
(action (with-stdout-to %{target}
30+
(progn
31+
(echo "(* Automatically generated, don't edit *)\n")
32+
(echo "[%%define lsp ")
33+
(run vscoq_version_parser %{version:lsp})
34+
(echo "]\n")))))

language-server/etc/dune

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
(executable
2+
(name version_parser)
3+
(public_name vscoq_version_parser)
4+
(modules version_parser)
5+
(libraries str)
6+
(package vscoq-language-server)
7+
)

language-server/etc/version_parser.ml

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
2+
let is_number x = try let _ = int_of_string x in true with _ -> false ;;
3+
4+
let main () =
5+
let v = Sys.argv.(1) in
6+
let v' = Str.(replace_first (regexp "^v") "" v) in (* v1.20... -> 1.20... *)
7+
let v' = Str.(replace_first (regexp "-.*$") "" v') in (* ...-10-fjdnfs -> ... *)
8+
let l = String.split_on_char '.' v' in
9+
(* sanitization *)
10+
let l =
11+
match l with
12+
| [_;_;_] as l when List.for_all is_number l -> l
13+
| [_] -> ["99";"99";"99"]
14+
| _ -> Printf.eprintf "version_parser: cannot parse: %s\n" v; exit 1 in
15+
let open Format in
16+
printf "(%a)%!" (pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt ", ") pp_print_string) l
17+
;;
18+
19+
main ()

language-server/tests/common.ml

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,11 +12,19 @@
1212
(* *)
1313
(**************************************************************************)
1414

15+
[%%import "vscoq_config.mlh"]
16+
1517
open Dm
1618
open Base
1719
open Types
1820
open Protocol.LspWrapper
1921

22+
[%%if lsp < (1,19,0) ]
23+
let string_of_message x = x
24+
[%%else]
25+
let string_of_message = function `String x -> x | _ -> assert false
26+
[%%endif]
27+
2028
[%%if coq = "8.18" || coq = "8.19" || coq = "8.20"]
2129
let injections =
2230
Coqinit.init_ocaml ();
@@ -180,7 +188,7 @@ type diag_spec =
180188

181189
let check_no_diag st =
182190
let diagnostics = DocumentManager.all_diagnostics st in
183-
let diagnostics = List.map ~f:Lsp.Types.Diagnostic.(fun d -> d.range, d.message, d.severity) diagnostics in
191+
let diagnostics = List.map ~f:Lsp.Types.Diagnostic.(fun d -> d.range, string_of_message d.message, d.severity) diagnostics in
184192
[%test_pred: (Range.t * string * DiagnosticSeverity.t option) list] List.is_empty diagnostics
185193

186194
type diagnostic_summary = Range.t * string * DiagnosticSeverity.t option [@@deriving sexp]
@@ -189,7 +197,7 @@ let check_diag st specl =
189197
let open Result in
190198
let open Lsp.Types.Diagnostic in
191199
let diagnostic_summary { range; message; severity } =
192-
let message = Str.global_replace (Str.regexp_string "\n") " " message in
200+
let message = Str.global_replace (Str.regexp_string "\n") " " (string_of_message message) in
193201
let message = Str.global_replace (Str.regexp " Raised at .*$") "" message in
194202
(range, message, severity) in
195203
let match_diagnostic r s rex (range, message, severity) =

language-server/tests/dune

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,15 @@
33
(libraries base dm protocol)
44
(preprocess
55
(pps ppx_sexp_conv ppx_inline_test ppx_assert ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")"))
6+
(preprocessor_deps vscoq_config.mlh)
67
(inline_tests))
8+
9+
10+
(rule
11+
(target vscoq_config.mlh)
12+
(action (with-stdout-to %{target}
13+
(progn
14+
(echo "(* Automatically generated, don't edit *)\n")
15+
(echo "[%%define lsp ")
16+
(run vscoq_version_parser %{version:lsp})
17+
(echo "]\n")))))

language-server/vscoq-language-server.opam

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ depends: [
2727
"ppx_import"
2828
"ppx_optcomp"
2929
"result" { >= "1.5" }
30-
"lsp" { >= "1.15" < "1.19"}
30+
"lsp" { >= "1.15"}
3131
"sel" {>= "0.4.0"}
3232
]
3333
synopsis: "VSCoq language server"

0 commit comments

Comments
 (0)