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

coq · Oct 23, 2024 · e9a3f2e · e9a3f2e
1 parent 50b41ad
commit e9a3f2e
Show file tree

Hide file tree

Showing 5 changed files with 6 additions and 6 deletions.
diff --git a/language-server/dm/delegationManager.ml b/language-server/dm/delegationManager.ml
@@ -96,7 +96,7 @@ module type Worker = sig
 
   (* for worker toplevels *)
   type options
-  val parse_options : string list -> options * string list
+  val parse_options : Coqargs.t -> string list -> options * string list
   (* the sentence ids of the remote_mapping being delegated *)
   val setup_plumbing : options -> ((job_update_request -> unit) * job_t)
 
@@ -331,7 +331,7 @@ let setup_plumbing port =
     log_worker @@ Printf.sprintf "error starting: %s: %s: %s" syscall param (Unix.error_message code);
     exit 1
 
-let parse_options extra_args =
+let parse_options _baseopts extra_args =
   match extra_args with
   | [ o ; port ] when o = option_name -> int_of_string port, []
   | _ ->

diff --git a/language-server/dm/delegationManager.mli b/language-server/dm/delegationManager.mli
@@ -79,7 +79,7 @@ module type Worker = sig
 
    (* for worker toplevels *)
    type options
-   val parse_options : string list -> options * string list
+   val parse_options : Coqargs.t -> string list -> options * string list
    (* the sentence ids of the remote_mapping being delegated *)
    val setup_plumbing : options -> ((job_update_request -> unit) * job_t)
 

diff --git a/language-server/dm/executionManager.mli b/language-server/dm/executionManager.mli
@@ -87,7 +87,7 @@ 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
+  val parse_options : Coqargs.t -> string list -> options * string list
   val main : st:Vernacstate.t -> options -> unit
   val log : string -> unit
 end
diff --git a/language-server/dm/parTactic.mli b/language-server/dm/parTactic.mli
@@ -13,7 +13,7 @@
 (**************************************************************************)
 module TacticWorkerProcess : sig
   type options
-  val parse_options : string list -> options * string list
+  val parse_options : Coqargs.t -> string list -> options * string list
   val main : st:Vernacstate.t -> options -> unit
   val log : string -> unit
 end

diff --git a/language-server/vscoqtop/vscoqtop.ml b/language-server/vscoqtop/vscoqtop.ml
@@ -70,7 +70,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:(fun _ x -> skip_xd [] x) () 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);