From 64ee7c21cedf806c8b9519b33e1e6c29ace18f05 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 23 Oct 2024 15:12:28 +0200 Subject: [PATCH] Adapt to coq/coq#19741 (STM worker spawning doesn't use Sys.argv directly) --- serapi/serapi_protocol.ml | 3 ++- sertop/sertop_init.ml | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/serapi/serapi_protocol.ml b/serapi/serapi_protocol.ml index c7c3bfa5..f69bc610 100644 --- 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 index 91ab73af..82e2f7c3 100644 --- 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