6 |
6 |
7 signature BASIC_GOAL = |
7 signature BASIC_GOAL = |
8 sig |
8 sig |
9 val skip_proofs: bool Unsynchronized.ref |
9 val skip_proofs: bool Unsynchronized.ref |
10 val parallel_proofs: int Unsynchronized.ref |
10 val parallel_proofs: int Unsynchronized.ref |
11 val parallel_subproofs_saturation: int Unsynchronized.ref |
|
12 val parallel_subproofs_threshold: real Unsynchronized.ref |
|
13 val SELECT_GOAL: tactic -> int -> tactic |
11 val SELECT_GOAL: tactic -> int -> tactic |
14 val CONJUNCTS: tactic -> int -> tactic |
12 val CONJUNCTS: tactic -> int -> tactic |
15 val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic |
13 val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic |
16 val PARALLEL_CHOICE: tactic list -> tactic |
14 val PARALLEL_CHOICE: tactic list -> tactic |
17 val PARALLEL_GOALS: tactic -> tactic |
15 val PARALLEL_GOALS: tactic -> tactic |
198 (* scheduling parameters *) |
196 (* scheduling parameters *) |
199 |
197 |
200 val skip_proofs = Unsynchronized.ref false; |
198 val skip_proofs = Unsynchronized.ref false; |
201 |
199 |
202 val parallel_proofs = Unsynchronized.ref 1; |
200 val parallel_proofs = Unsynchronized.ref 1; |
203 val parallel_subproofs_saturation = Unsynchronized.ref 100; |
|
204 val parallel_subproofs_threshold = Unsynchronized.ref 0.01; |
|
205 |
201 |
206 fun future_enabled_level n = |
202 fun future_enabled_level n = |
207 Multithreading.enabled () andalso ! parallel_proofs >= n andalso |
203 Multithreading.enabled () andalso ! parallel_proofs >= n andalso |
208 is_some (Future.worker_task ()); |
204 is_some (Future.worker_task ()); |
209 |
205 |
210 fun future_enabled () = future_enabled_level 1; |
206 fun future_enabled () = future_enabled_level 1; |
211 |
207 |
212 fun future_enabled_nested n = |
208 fun future_enabled_nested n = |
213 future_enabled_level n andalso |
209 future_enabled_level n andalso |
214 forked_count () < ! parallel_subproofs_saturation * Multithreading.max_threads_value (); |
210 forked_count () < |
|
211 Options.default_int "parallel_subproofs_saturation" * Multithreading.max_threads_value (); |
215 |
212 |
216 fun future_enabled_timing t = |
213 fun future_enabled_timing t = |
217 future_enabled () andalso Time.toReal t >= ! parallel_subproofs_threshold; |
214 future_enabled () andalso |
|
215 Time.toReal t >= Options.default_real "parallel_subproofs_threshold"; |
218 |
216 |
219 |
217 |
220 (* future_result *) |
218 (* future_result *) |
221 |
219 |
222 fun future_result ctxt result prop = |
220 fun future_result ctxt result prop = |