diff options
Diffstat (limited to 'lib/remoteCounter.ml')
| -rw-r--r-- | lib/remoteCounter.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml index 1983d2722..e0e2d5cbc 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 |