summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Tue, 24 Apr 2018 18:10:08 +0200 | |

changeset 68030 | 0a6d6ba383dc |

parent 68029 | df9044efd054 |

child 68032 | 412fe0623c5d |

more ambitious parallelism (in contrast to a8ee8e4884ec): pri = 1 ensures that internal proof tasks are executed before the already forked theory outline with pri = 0;

--- a/src/Pure/proofterm.ML Tue Apr 24 16:59:40 2018 +0200 +++ b/src/Pure/proofterm.ML Tue Apr 24 18:10:08 2018 +0200 @@ -1610,16 +1610,14 @@ val argsP = map OfClass outer_constraints @ map Hyp hyps; fun make_body0 proof0 = PBody {oracles = oracles0, thms = thms0, proof = proof0}; - fun make_body () = - make_body0 (shrink_proof (rew_proof thy (fold_rev implies_intr_proof hyps prf))); val body0 = if not (proofs_enabled ()) then Future.value (make_body0 MinProof) - else if not (Multithreading.parallel_proofs_enabled 1) then Future.value (make_body ()) else (singleton o Future.cond_forks) {name = "Proofterm.prepare_thm_proof", group = NONE, - deps = [], pri = 0, interrupts = true} - make_body; + deps = [], pri = 1, interrupts = true} + (fn () => + make_body0 (shrink_proof (rew_proof thy (fold_rev implies_intr_proof hyps prf)))); fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0); val (i, body') =