Adapt to coq/coq#19741 (STM worker spawning doesn't use Sys.argv dire…

…ctly)
rocq-archive · Oct 23, 2024 · 64ee7c2 · 64ee7c2
1 parent ee470bb
commit 64ee7c2
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/serapi/serapi_protocol.ml b/serapi/serapi_protocol.ml
@@ -890,7 +890,8 @@ let exec_cmd (st : State.t) (cmd : cmd) : answer_kind list * State.t =
   let doc = Stm.get_doc !doc_id in
   coq_protect st @@ fun () -> match cmd with
   | NewDoc opts   ->
-    let stm_options = Stm.AsyncOpts.default_opts in
+    (* spawn_args probably wrong *)
+    let stm_options = Stm.AsyncOpts.default_opts ~spawn_args:[] in
     let require_libs = Option.default [{Coqargs.lib="Stdlib.Init.Prelude"; prefix=None; export=Some Lib.Export; allow_failure=false}] opts.require_libs in
     Stm.init_process stm_options;
     let ndoc = { Stm.doc_type = Stm.(Interactive opts.top_name)

diff --git a/sertop/sertop_init.ml b/sertop/sertop_init.ml
@@ -130,7 +130,8 @@ let update_fb_handler ~pp_feed out_fmt =
 
 (* Set async flags; IMPORTANT, this has to happen before STM.init () ! *)
 let process_stm_flags opts =
-  let stm_opts = Stm.AsyncOpts.default_opts in
+  (* spawn_args probably wrong *)
+  let stm_opts = Stm.AsyncOpts.default_opts ~spawn_args:[] in
   (* Process error resilience *)
   let async_proofs_tac_error_resilience, async_proofs_cmd_error_resilience =
     if opts.error_recovery