diff options
Diffstat (limited to 'lib')
-rw-r--r-- | lib/control.ml | 7 | ||||
-rw-r--r-- | lib/control.mli | 3 | ||||
-rw-r--r-- | lib/flags.ml | 28 | ||||
-rw-r--r-- | lib/flags.mli | 25 |
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 *) |