[flags] [stm] Reorganize flags.

We move the main async flags to the STM in preparation for
more state encapsulation.

There is still more work to do, in particular we should make some of
the defaults a parameter instead of a flag.

4 files changed, 8 insertions, 55 deletions

diff --git a/lib/control.ml b/lib/control.ml
index d936d7557..c6489938e 100644
--- a/lib/control.ml
+++ b/lib/control.ml
@@ -12,15 +12,12 @@ let interrupt = ref false
 
 let steps = ref 0
 
-let are_we_threading = lazy (
-  match !Flags.async_proofs_mode with
-  | Flags.APon -> true
-  | _ -> false)
+let enable_thread_delay = ref false
 
 let check_for_interrupt () =
   if !interrupt then begin interrupt := false; raise Sys.Break end;
   incr steps;
-  if !steps = 1000 && Lazy.force are_we_threading then begin
+  if !enable_thread_delay && !steps = 1000 then begin
     Thread.delay 0.001;
     steps := 0;
   end
diff --git a/lib/control.mli b/lib/control.mli
index f6c63ffb3..261b07693 100644
--- a/lib/control.mli
+++ b/lib/control.mli
@@ -8,6 +8,9 @@
 
 (** Global control of Coq. *)
 
+(** Will periodically call [Thread.delay] if set to true *)
+val enable_thread_delay : bool ref
+
 val interrupt : bool ref
 (** Coq interruption: set the following boolean reference to interrupt Coq
     (it eventually raises [Break], simulating a Ctrl-C) *)
diff --git a/lib/flags.ml b/lib/flags.ml
index ddc8f8482..b43d5f74d 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -35,36 +35,10 @@ let record_aux_file = ref false
 
 let test_mode = ref false
 
-type async_proofs = APoff | APonLazy | APon
-let async_proofs_mode = ref APoff
-type cache = Force
-let async_proofs_cache = ref None
-let async_proofs_n_workers = ref 1
-let async_proofs_n_tacworkers = ref 2
-let async_proofs_private_flags = ref None
-let async_proofs_full = ref false
-let async_proofs_never_reopen_branch = ref false
-let async_proofs_flags_for_workers = ref []
 let async_proofs_worker_id = ref "master"
-type priority = Low | High
-let async_proofs_worker_priority = ref Low
-let string_of_priority = function Low -> "low" | High -> "high"
-let priority_of_string = function
-  | "low" -> Low
-  | "high" -> High
-  | _ -> raise (Invalid_argument "priority_of_string")
-type tac_error_filter = [ `None | `Only of string list | `All ]
-let async_proofs_tac_error_resilience = ref (`Only [ "curly" ])
-let async_proofs_cmd_error_resilience = ref true
-
-let async_proofs_is_worker () =
-  !async_proofs_worker_id <> "master"
-let async_proofs_is_master () =
-  !async_proofs_mode = APon && !async_proofs_worker_id = "master"
-let async_proofs_delegation_threshold = ref 0.03
+let async_proofs_is_worker () = !async_proofs_worker_id <> "master"
 
 let debug = ref false
-let stm_debug = ref false
 
 let in_debugger = ref false
 let in_toplevel = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index c4afb8318..b82fe6128 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -21,35 +21,14 @@ val record_aux_file : bool ref
 val test_mode : bool ref
 
 (** Async-related flags *)
-type async_proofs = APoff | APonLazy | APon
-val async_proofs_mode : async_proofs ref
-type cache = Force
-val async_proofs_cache : cache option ref
-val async_proofs_n_workers : int ref
-val async_proofs_n_tacworkers : int ref
-val async_proofs_private_flags : string option ref
-val async_proofs_is_worker : unit -> bool
-val async_proofs_is_master : unit -> bool
-val async_proofs_full : bool ref
-val async_proofs_never_reopen_branch : bool ref
-val async_proofs_flags_for_workers : string list ref
 val async_proofs_worker_id : string ref
-type priority = Low | High
-val async_proofs_worker_priority : priority ref
-val string_of_priority : priority -> string
-val priority_of_string : string -> priority
-type tac_error_filter = [ `None | `Only of string list | `All ]
-val async_proofs_tac_error_resilience : tac_error_filter ref
-val async_proofs_cmd_error_resilience : bool ref
-val async_proofs_delegation_threshold : float ref
+val async_proofs_is_worker : unit -> bool
 
+(** Debug flags *)
 val debug : bool ref
 val in_debugger : bool ref
 val in_toplevel : bool ref
 
-(** Enable STM debugging *)
-val stm_debug : bool ref
-
 val profile : bool
 
 (* -ide_slave: printing will be more verbose, will affect stm caching *)