Adapt to coq/coq#19741 (parse_extra has an additional argument)

language-server/dm/delegationManager.ml

@@ -96,7 +96,11 @@ module type Worker = sig
 
   (* for worker toplevels *)
   type options
+  [%%if coq = "8.18" || coq = "8.19" || coq = "8.20"]
   val parse_options : string list -> options * string list
+  [%%else]
+  val parse_options : Coqargs.t -> string list -> options * string list
+  [%%endif]
   (* the sentence ids of the remote_mapping being delegated *)
   val setup_plumbing : options -> ((job_update_request -> unit) * job_t)
 
@@ -338,6 +342,12 @@ let parse_options extra_args =
     Printf.eprintf "unknown arguments: %s" (String.concat " " extra_args);
     exit 2
 
+[%%if coq = "8.18" || coq = "8.19" || coq = "8.20"]
+let parse_options a = parse_options a
+[%%else]
+let parse_options _ a = parse_options a
+[%%endif]
+
 let log = log_worker
 
 end

language-server/dm/delegationManager.mli

@@ -79,7 +79,11 @@ module type Worker = sig
 
    (* for worker toplevels *)
    type options
+[%%if coq = "8.18" || coq = "8.19" || coq = "8.20"]
    val parse_options : string list -> options * string list
+[%%else]
+   val parse_options : Coqargs.t -> string list -> options * string list
+[%%endif]
    (* the sentence ids of the remote_mapping being delegated *)
    val setup_plumbing : options -> ((job_update_request -> unit) * job_t)
 

language-server/dm/executionManager.mli

@@ -87,7 +87,11 @@ val print_exec_overview_of_state : state -> unit
 (** Coq toplevels for delegation without fork *)
 module ProofWorkerProcess : sig
   type options
-  val parse_options : string list -> options * string list
+[%%if coq = "8.18" || coq = "8.19" || coq = "8.20"]
+   val parse_options : string list -> options * string list
+[%%else]
+   val parse_options : Coqargs.t -> string list -> options * string list
+[%%endif]
   val main : st:Vernacstate.t -> options -> unit
   val log : string -> unit
 end

language-server/dm/parTactic.mli

@@ -13,7 +13,11 @@
 (**************************************************************************)
 module TacticWorkerProcess : sig
   type options
-  val parse_options : string list -> options * string list
+[%%if coq = "8.18" || coq = "8.19" || coq = "8.20"]
+   val parse_options : string list -> options * string list
+[%%else]
+   val parse_options : Coqargs.t -> string list -> options * string list
+[%%endif]
   val main : st:Vernacstate.t -> options -> unit
   val log : string -> unit
 end

language-server/vscoqtop/dune

@@ -4,4 +4,5 @@
  (modules vscoqtop lspManager)
  (flags -linkall)
  (package vscoq-language-server)
- (libraries coq-core.sysinit coq-core.tactics sel yojson dm lsp))
+ (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")"))
+ (libraries coq-core.sysinit coq-core.tactics sel yojson dm lsp))

language-server/vscoqtop/vscoqtop.ml

@@ -56,6 +56,13 @@ let rec skip_xd acc = function
   | "-vscoq-d" :: _ :: rest -> skip_xd acc rest
   | x :: rest -> skip_xd (x::acc) rest
 
+[%%if coq = "8.18" || coq = "8.19" || coq = "8.20"]
+let parse_extra x =
+  skip_xd [] x
+[%%else]
+let parse_extra _ x = skip_xd [] x
+[%%endif]
+
 let _ =
   Coqinit.init_ocaml ();
   log "------------------ begin ---------------";
@@ -70,7 +77,7 @@ let _ =
       let args = CoqProject_file.coqtop_args_from_project project in
       log (Printf.sprintf "Arguments from project file %s: %s" f (String.concat " " args));
       fst @@ Coqargs.parse_args ~usage:vscoqtop_specific_usage ~init:Coqargs.default args in
-  let opts, () = Coqinit.parse_arguments ~usage:vscoqtop_specific_usage ~initial_args ~parse_extra:(fun x -> skip_xd [] x) () in
+  let opts, () = Coqinit.parse_arguments ~usage:vscoqtop_specific_usage ~initial_args ~parse_extra () in
   let injections = Coqinit.init_runtime opts in
   Safe_typing.allow_delayed_constants := true; (* Needed to delegate or skip proofs *)
   Sys.(set_signal sigint Signal_ignore);