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

author | wenzelm |

Tue, 24 Apr 2018 11:07:18 +0200 | |

changeset 68026 | a8ee8e4884ec |

parent 68025 | 7fb7a6366a40 |

child 68027 | 64559e1ca05b |

less ambitious parallelism: avoid problems with HOL-Proofs and threads=2 (congestion with many thousands futures and rather dense heap);

--- a/src/Pure/proofterm.ML Tue Apr 24 11:03:51 2018 +0200 +++ b/src/Pure/proofterm.ML Tue Apr 24 11:07:18 2018 +0200 @@ -1610,14 +1610,16 @@ 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} - (fn () => - make_body0 (shrink_proof (rew_proof thy (fold_rev implies_intr_proof hyps prf)))); + make_body; fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0); val (i, body') =