From 50159f9c1748ccf1d66341d171081a998d116d2f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 10 Jun 2017 04:27:21 +0200 Subject: [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. --- stm/stm.mli | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) (limited to 'stm/stm.mli') diff --git a/stm/stm.mli b/stm/stm.mli index 9fd35a0d3..ef95be0e4 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -225,3 +225,30 @@ val state_of_id : doc:doc -> (* Queries for backward compatibility *) val current_proof_depth : doc:doc -> int val get_all_proof_names : doc:doc -> Id.t list + +(** Enable STM debugging *) +val stm_debug : bool ref + +(* Flags *) +module AsyncOpts : sig + + (* Defaults for worker creation *) + val async_proofs_n_workers : int ref + val async_proofs_n_tacworkers : int ref + + 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_private_flags : string option ref + val async_proofs_full : bool ref + val async_proofs_never_reopen_branch : bool ref + + 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 + +end -- cgit v1.2.3