diff options
| author | Enrico Tassi | 2014-06-30 23:25:19 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-07-10 15:22:58 +0200 |
| commit | 3abbc93733b7f820a436beedcd0b9292378e1840 (patch) | |
| tree | f310b829a8a2ce2335663d4976bcd029c9c5b102 /stm | |
| parent | 4f554c88aa7ecc8ebeb8af1a11bf3a12d255c25b (diff) | |
option to always delegate futures to workers
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index f62bae4b12..2007dba811 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1151,9 +1151,11 @@ let pstate = ["meta counter"; "evar counter"; "program-tcc-table"] let delegate_policy_check time = if interactive () = `Yes then (!Flags.async_proofs_mode = Flags.APonParallel 0 || - !Flags.async_proofs_mode = Flags.APonLazy) && time >= 1.0 + !Flags.async_proofs_mode = Flags.APonLazy) && + (time >= 1.0 || !Flags.async_proofs_always_delegate) else if !Flags.compilation_mode = Flags.BuildVi then true - else !Flags.async_proofs_mode <> Flags.APoff && time >= 1.0 + else !Flags.async_proofs_mode <> Flags.APoff && + (time >= 1.0 || !Flags.async_proofs_always_delegate) let collect_proof cur hd brkind id = prerr_endline ("Collecting proof ending at "^Stateid.to_string id); |