Merge pull request #936 from SkySkimmer/argv-topbin

Adapt to coq/coq#19763 (parse_arguments does not implicitly use Sys.argv)
coq · Oct 31, 2024 · 3221ee5 · 3221ee5
2 parents 927ec49 + 2999498
commit 3221ee5
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/language-server/dm/vscoqtop_proof_worker.ml b/language-server/dm/vscoqtop_proof_worker.ml
@@ -53,7 +53,7 @@ let _ =
 [%%else]
 let () =
   Coqinit.init_ocaml ();
-  let opts, emoptions = Coqinit.parse_arguments ~parse_extra:Dm.ExecutionManager.ProofWorkerProcess.parse_options () in
+  let opts, emoptions = Coqinit.parse_arguments ~parse_extra:Dm.ExecutionManager.ProofWorkerProcess.parse_options (List.tl (Array.to_list Sys.argv)) in
   let injections = Coqinit.init_runtime ~usage:vscoqtop_specific_usage opts in
   start_library (Coqinit.dirpath_of_top opts.config.logic.toplevel_name) injections;
   log @@ "started";

diff --git a/language-server/dm/vscoqtop_tactic_worker.ml b/language-server/dm/vscoqtop_tactic_worker.ml
@@ -52,7 +52,7 @@ let () =
 [%%else]
 let () =
   Coqinit.init_ocaml ();
-  let opts, emoptions = Coqinit.parse_arguments ~parse_extra:Dm.ParTactic.TacticWorkerProcess.parse_options () in
+  let opts, emoptions = Coqinit.parse_arguments ~parse_extra:Dm.ParTactic.TacticWorkerProcess.parse_options (List.tl (Array.to_list Sys.argv)) in
   let injections = Coqinit.init_runtime ~usage:vscoqtop_specific_usage opts in
   start_library (Coqinit.dirpath_of_top opts.config.logic.toplevel_name) injections;
   log @@ "started";

diff --git a/language-server/vscoqtop/vscoqtop.ml b/language-server/vscoqtop/vscoqtop.ml
@@ -96,7 +96,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 ~init:Coqargs.default args in
-  let opts, () = Coqinit.parse_arguments ~initial_args ~parse_extra () in
+  let opts, () = Coqinit.parse_arguments ~initial_args ~parse_extra (List.tl (Array.to_list Sys.argv)) in
   let injections = Coqinit.init_runtime ~usage:vscoqtop_specific_usage opts in
   Safe_typing.allow_delayed_constants := true; (* Needed to delegate or skip proofs *)
   Sys.(set_signal sigint Signal_ignore);