diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/flags.ml | 12 | ||||
| -rw-r--r-- | lib/flags.mli | 8 | ||||
| -rw-r--r-- | lib/future.ml | 4 | ||||
| -rw-r--r-- | lib/remoteCounter.ml | 12 |
4 files changed, 24 insertions, 12 deletions
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 |