aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/coq.ml2
-rw-r--r--kernel/reduction.ml8
-rw-r--r--lib/flags.ml12
-rw-r--r--lib/flags.mli8
-rw-r--r--lib/future.ml4
-rw-r--r--lib/remoteCounter.ml12
-rw-r--r--tools/coqc.ml9
-rw-r--r--toplevel/coqtop.ml25
-rw-r--r--toplevel/stm.ml67
9 files changed, 90 insertions, 57 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index 87387c5f9a..7d1267c3af 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -480,7 +480,7 @@ let install_input_watch handle respawner feedback_processor =
let spawn_handle args =
let prog = coqtop_path () in
let args = Array.of_list (
- prog :: "-coq-slaves" :: "on" :: "-ideslave" :: args) in
+ prog :: "-async-proofs" :: "on" :: "-ideslave" :: args) in
let pid, ic, gic, oc, close_channels = open_process_pid prog args in
let xml_ic = Xml_parser.make (Xml_parser.SChannel ic) in
let xml_oc = Xml_printer.make (Xml_printer.TChannel oc) in
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index f7805459f2..5397e42f9e 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -246,6 +246,12 @@ let in_whnf (t,stk) =
let steps = ref 0
+let slave_process =
+ let rec f = ref (fun () ->
+ match !Flags.async_proofs_mode with
+ | Flags.APonParallel n -> let b = n > 0 in f := (fun () -> b); !f ()
+ | _ -> f := (fun () -> false); !f ()) in
+ fun () -> !f ()
(* Conversion between [lft1]term1 and [lft2]term2 *)
let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
@@ -255,7 +261,7 @@ let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
Util.check_for_interrupt ();
incr steps;
- if !steps = 10000 && !Flags.coq_slave_mode > 0 then begin
+ if !steps = 10000 && slave_process () then begin
Thread.yield ();
steps := 0;
end;
diff --git a/lib/flags.ml b/lib/flags.ml
index 0cefc90c4b..3a79a83e33 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -47,10 +47,16 @@ let batch_mode = ref false
type compilation_mode = BuildVo | BuildVi
let compilation_mode = ref BuildVo
-let coq_slave_mode = ref (-1)
-let coq_slaves_number = ref 1
-let coq_slave_options = ref None
+type async_proofs = APoff | APonLazy | APonParallel of int
+let async_proofs_mode = ref APoff
+let async_proofs_n_workers = ref 1
+let async_proofs_worker_flags = ref None
+
+let async_proofs_is_worker () =
+ match !async_proofs_mode with
+ | APonParallel n -> n > 0
+ | _ -> false
let debug = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index f0b6766411..476b52a7a6 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -14,10 +14,12 @@ val batch_mode : bool ref
type compilation_mode = BuildVo | BuildVi
val compilation_mode : compilation_mode ref
-val coq_slave_mode : int ref
-val coq_slaves_number : int ref
+type async_proofs = APoff | APonLazy | APonParallel of int
+val async_proofs_mode : async_proofs ref
+val async_proofs_n_workers : int ref
+val async_proofs_worker_flags : string option ref
-val coq_slave_options : string option ref
+val async_proofs_is_worker : unit -> bool
val debug : bool ref
diff --git a/lib/future.ml b/lib/future.ml
index 391f5a65c7..191fc3fddc 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -17,12 +17,12 @@ let _ = Errors.register_handler (function
| NotReady ->
Pp.strbrk("The value you are asking for is not ready yet. " ^
"Please wait or pass "^
- "the \"-coq-slaves off\" option to CoqIDE to disable "^
+ "the \"-async-proofs off\" option to CoqIDE to disable "^
"asynchronous script processing.")
| NotHere ->
Pp.strbrk("The value you are asking for is not available "^
"in this process. If you really need this, pass "^
- "the \"-coq-slaves off\" option to CoqIDE to disable"^
+ "the \"-async-proofs off\" option to CoqIDE to disable"^
"asynchronous script processing.")
| _ -> raise Errors.Unhandled)
diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml
index 1983d27220..e0e2d5cbc7 100644
--- a/lib/remoteCounter.ml
+++ b/lib/remoteCounter.ml
@@ -16,14 +16,18 @@ let new_counter a ~incr ~build =
(* - slaves must use a remote counter getter, not this one! *)
(* - in the main process there is a race condition between slave
managers (that are threads) and the main thread, hence the mutex *)
- if !Flags.coq_slave_mode > 0 then
- Errors.anomaly(Pp.str"Slave processes must install remote counters");
+ (match !Flags.async_proofs_mode with
+ | Flags.APonParallel n when n > 0 ->
+ Errors.anomaly(Pp.str"Slave processes must install remote counters");
+ | _ -> ());
Mutex.lock m; let x = f () in Mutex.unlock m;
build x in
let getter = ref (mk_thsafe_getter (fun () -> data := incr !data; !data)) in
let installer f =
- if !Flags.coq_slave_mode < 1 then
+ (match !Flags.async_proofs_mode with
+ | Flags.APoff | Flags.APonLazy | Flags.APonParallel 0 ->
Errors.anomaly(Pp.str"Only slave processes can install a remote counter")
- else getter := f in
+ | _ -> ());
+ getter := f in
(fun () -> !getter ()), installer
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 378f493adf..5e63322c5a 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -117,8 +117,10 @@ let parse_args () =
|"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
|"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit"
|"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs"
- |"-impredicative-set"|"-vm"|"-no-native-compiler"|"-quick"
- |"-verbose-compat-notations"|"-no-compat-notations" as o) :: rem ->
+ |"-impredicative-set"|"-vm"|"-no-native-compiler"
+ |"-verbose-compat-notations"|"-no-compat-notations"
+ |"-quick"
+ as o) :: rem ->
parse (cfiles,o::args) rem
(* Options for coqtop : b) options with 1 argument *)
@@ -127,7 +129,8 @@ let parse_args () =
|"-load-vernac-source"|"-l"|"-load-vernac-object"
|"-load-ml-source"|"-require"|"-load-ml-object"
|"-init-file"|"-dump-glob"|"-compat"|"-coqlib"
- |"-check-vi-tasks" as o) :: rem ->
+ |"-async-proofs-j" |"-async-proofs-worker-flags" |"-async-proofs"
+ as o) :: rem ->
begin
match rem with
| s :: rem' -> parse (cfiles,s::o::args) rem'
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index f902206e23..b1d3e0cc24 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -218,10 +218,14 @@ let no_compat_ntn = ref false
let print_where = ref false
let print_config = ref false
-let get_slave_number = function
- | "off" -> -1
- | "on" -> 0
- | s -> let n = int_of_string s in assert (n > 0); n
+let get_async_proofs_mode opt next = function
+ | "off" -> Flags.APoff
+ | "on" -> Flags.APonParallel 0
+ | "worker" ->
+ let n = int_of_string (next()) in assert (n > 0);
+ Flags.APonParallel n
+ | "lazy" -> Flags.APonLazy
+ | _ -> prerr_endline ("Error: on/off/lazy/worker expected after "^opt); exit 1
let get_bool opt = function
| "yes" -> true
@@ -310,9 +314,12 @@ let parse_args arglist =
(* Options with one arg *)
|"-coqlib" -> Flags.coqlib_spec:=true; Flags.coqlib:=(next ())
- |"-coq-slaves" -> Flags.coq_slave_mode := (get_slave_number (next ()))
- |"-coq-slaves-j" -> Flags.coq_slaves_number := (get_int opt (next ()))
- |"-coq-slaves-opts" -> Flags.coq_slave_options := Some (next ())
+ |"-async-proofs" ->
+ Flags.async_proofs_mode := get_async_proofs_mode opt next (next())
+ |"-async-proofs-j" ->
+ Flags.async_proofs_n_workers := (get_int opt (next ()))
+ |"-async-proofs-worker-flags" ->
+ Flags.async_proofs_worker_flags := Some (next ())
|"-compat" -> Flags.compat_version := get_compat_version (next ())
|"-compile" -> add_compile false (next ())
|"-compile-verbose" -> add_compile true (next ())
@@ -414,7 +421,7 @@ let init arglist =
if !Flags.ide_slave then begin
Flags.make_silent true;
Ide_slave.init_stdout ()
- end else if !Flags.coq_slave_mode > 0 then begin
+ end else if Flags.async_proofs_is_worker () then begin
Flags.make_silent true;
Stm.slave_init_stdout ()
end;
@@ -467,7 +474,7 @@ let start () =
Dumpglob.noglob () in
if !Flags.ide_slave then
Ide_slave.loop ()
- else if !Flags.coq_slave_mode > 0 then
+ else if Flags.async_proofs_is_worker () then
Stm.slave_main_loop ()
else
Coqloop.loop();
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index bb531056f3..86b7794e8b 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -6,9 +6,14 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+let process_id () =
+ match !Flags.async_proofs_mode with
+ | Flags.APoff | Flags.APonLazy | Flags.APonParallel 0 -> "master"
+ | Flags.APonParallel n -> "worker" ^ string_of_int n
+
let prerr_endline s =
if !Flags.debug then begin
- prerr_endline (Printf.sprintf "%d] %s" !Flags.coq_slave_mode s);
+ prerr_endline (Printf.sprintf "%s] %s" (process_id ()) s);
flush stderr
end else ()
@@ -27,8 +32,7 @@ let interactive () =
let fallback_to_lazy_if_marshal_error = ref true
let fallback_to_lazy_if_slave_dies = ref true
-let min_proof_length_to_delegate = ref 20
-let coq_slave_extra_env = ref [||]
+let async_proofs_workers_extra_env = ref [||]
type ast = { verbose : bool; loc : Loc.t; mutable expr : vernac_expr }
let pr_ast { expr } = pr_vernac expr
@@ -232,7 +236,7 @@ end = struct (* {{{ *)
open Printf
let print_dag vcs () = (* {{{ *)
- let fname = "stm" ^ string_of_int (max 0 !Flags.coq_slave_mode) in
+ let fname = "stm_" ^ process_id () in
let string_of_transaction = function
| Cmd (t, _) | Fork (t, _,_,_) ->
(try string_of_ppcmds (pr_ast t) with _ -> "ERR")
@@ -692,16 +696,16 @@ end = struct (* {{{ *)
Unix.set_close_on_exec s2c_r;
let prog = Sys.argv.(0) in
let rec set_slave_opt = function
- | [] -> ["-coq-slaves"; string_of_int n]
+ | [] -> ["-async-proofs"; "worker"; string_of_int n]
| ("-ideslave"|"-emacs"|"-emacs-U")::tl -> set_slave_opt tl
- | ("-coq-slaves"
+ | ("-async-proofs"
|"-compile"
|"-compile-verbose")::_::tl -> set_slave_opt tl
| x::tl -> x :: set_slave_opt tl in
let args = Array.of_list (set_slave_opt (Array.to_list Sys.argv)) in
prerr_endline ("EXEC: " ^ prog ^ " " ^
(String.concat " " (Array.to_list args)));
- let env = Array.append !coq_slave_extra_env (Unix.environment ()) in
+ let env = Array.append !async_proofs_workers_extra_env (Unix.environment ()) in
let pid = Unix.create_process_env prog args env c2s_r s2c_w Unix.stderr in
Unix.close c2s_r;
Unix.close s2c_w;
@@ -897,7 +901,14 @@ end = struct (* {{{ *)
exception KillRespawn
- let report_status ?(id = !Flags.coq_slave_mode) s =
+ let report_status ?id s =
+ let id =
+ match id with
+ | Some n -> n
+ | None ->
+ match !Flags.async_proofs_mode with
+ | Flags.APonParallel n -> n
+ | _ -> assert false in
Pp.feedback ~state_id:Stateid.initial (Interface.SlaveStatus(id, s))
let rec manage_slave respawn =
@@ -1004,7 +1015,7 @@ end = struct (* {{{ *)
flush_all (); exit 1
- let init () = SlavesPool.init !Flags.coq_slaves_number manage_slave
+ let init () = SlavesPool.init !Flags.async_proofs_n_workers manage_slave
let slave_ic = ref stdin
let slave_oc = ref stdout
@@ -1077,7 +1088,7 @@ end = struct (* {{{ *)
prerr_endline "Slave: failed with the following exception:";
prerr_endline (string_of_ppcmds (print e))
| e ->
- Printf.eprintf "Slave: failed with the following CRITICAL exception: %s\n"
+ Printf.eprintf "Slave: critical exception: %s\n"
(Pp.string_of_ppcmds (print e));
flush_all (); exit 1
done
@@ -1103,9 +1114,10 @@ end = struct (* {{{ *)
let pstate = ["meta counter"; "evar counter"; "program-tcc-table"]
-let delegate_policy_check l =
- (interactive () = `Yes || List.length l > !min_proof_length_to_delegate) &&
- (if interactive () = `Yes then !Flags.coq_slave_mode = 0 else true)
+let delegate_policy_check () =
+ if interactive () = `Yes then !Flags.async_proofs_mode = Flags.APonParallel 0
+ else if !Flags.compilation_mode = Flags.BuildVi then true
+ else !Flags.async_proofs_mode <> Flags.APoff
let collect_proof cur hd id =
prerr_endline ("Collecting proof ending at "^Stateid.to_string id);
@@ -1118,15 +1130,14 @@ let collect_proof cur hd id =
match last, view.step with
| _, `Cmd (x, _) -> collect (Some (id,x)) (id::accn) view.next
| _, `Alias _ -> `Sync `Alias
- | _, `Fork(_,_,_,_::_::_)->
- `Sync `MutualProofs (* TODO: enderstand where we need that *)
+ | _, `Fork(_,_,_,_::_::_)-> `Sync `MutualProofs
| _, `Fork(_,_,Doesn'tGuaranteeOpacity,_) ->
`Sync `Doesn'tGuaranteeOpacity
| Some (parent, ({ expr = VernacProof(_,Some _)} as v)),
`Fork (_, hd', GuaranteesOpacity, ids) ->
assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
- if delegate_policy_check accn then `ASync (parent,Some v,accn,ids)
- else `Sync `TooShort
+ if delegate_policy_check () then `ASync (parent,Some v,accn,ids)
+ else `Sync `Policy
| Some (parent, ({ expr = VernacProof(t,None)} as v)),
`Fork (_, hd', GuaranteesOpacity, ids) when
not (State.is_cached parent) &&
@@ -1135,13 +1146,13 @@ let collect_proof cur hd id =
let hint = get_hint_ctx loc in
assert (VCS.Branch.equal hd hd'||VCS.Branch.equal hd VCS.edit_branch);
v.expr <- VernacProof(t, Some hint);
- if delegate_policy_check accn then `ASync (parent,Some v,accn,ids)
- else `Sync `TooShort
+ if delegate_policy_check () then `ASync (parent,Some v,accn,ids)
+ else `Sync `Policy
with Not_found -> `Sync `NoHint)
| Some (parent, _), `Fork (_, hd', GuaranteesOpacity, ids) ->
assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
- if delegate_policy_check accn then `MaybeASync (parent, accn, ids)
- else `Sync `TooShort
+ if delegate_policy_check () then `MaybeASync (parent, accn, ids)
+ else `Sync `Policy
| _, `Sideff (`Ast (x,_)) -> collect (Some (id,x)) (id::accn) view.next
| _, `Sideff (`Id _) -> `Sync `NestedProof
| _ -> `Sync `Unknown in
@@ -1156,7 +1167,7 @@ let collect_proof cur hd id =
let string_of_reason = function
| `Transparent -> "Transparent"
| `AlreadyEvaluated -> "AlreadyEvaluated"
- | `TooShort -> "TooShort"
+ | `Policy -> "Policy"
| `NestedProof -> "NestedProof"
| `Immediate -> "Immediate"
| `Alias -> "Alias"
@@ -1423,9 +1434,9 @@ let init () =
set_undo_classifier Backtrack.undo_vernac_classifier;
State.define ~cache:`Yes (fun () -> ()) Stateid.initial;
Backtrack.record ();
- if Int.equal !Flags.coq_slave_mode 0 then begin (* We are the master process *)
+ if !Flags.async_proofs_mode = Flags.APonParallel 0 then begin
Slaves.init ();
- let opts = match !Flags.coq_slave_options with
+ let opts = match !Flags.async_proofs_worker_flags with
| None -> []
| Some s -> Str.split_delim (Str.regexp ",") s in
if String.List.mem "fallback-to-lazy-if-marshal-error=no" opts then
@@ -1435,15 +1446,9 @@ let init () =
begin try
let env_opt = Str.regexp "^extra-env=" in
let env = List.find (fun s -> Str.string_match env_opt s 0) opts in
- coq_slave_extra_env := Array.of_list
+ async_proofs_workers_extra_env := Array.of_list
(Str.split_delim (Str.regexp ";") (Str.replace_first env_opt "" env))
with Not_found -> () end;
- begin try
- let minlen_opt = Str.regexp "^min-proof-length-to-delegate=" in
- let len = List.find (fun s -> Str.string_match minlen_opt s 0) opts in
- min_proof_length_to_delegate :=
- int_of_string (Str.replace_first minlen_opt "" len)
- with Not_found -> () end;
end
let slave_main_loop () = Slaves.slave_main_loop Ephemeron.clear
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:35:43 +0000