diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-07-21 10:03:04 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-08-05 18:38:28 +0200 |
| commit | 7dba9d3f3ce62246b9d8562d2818c63ba37b206e (patch) | |
| tree | fbf0e133e160a5f7ff03f8a0b5bb4d0f47b43105 /stm/vernac_classifier.ml | |
| parent | 4e724634839726aa11534f16e4bfb95cd81232a4 (diff) | |
STM: new "par:" goal selector, like "all:" but in parallel
par: distributes the goals among a number of workers given
by -async-proofs-tac-j (defaults to 2).
Diffstat (limited to 'stm/vernac_classifier.ml')
| -rw-r--r-- | stm/vernac_classifier.ml | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 2b8c36ca9..5bbd857d9 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -18,7 +18,8 @@ let string_of_vernac_type = function | VtSideff _ -> "Sideff" | VtQed VtKeep -> "Qed(keep)" | VtQed VtDrop -> "Qed(drop)" - | VtProofStep -> "ProofStep" + | VtProofStep false -> "ProofStep" + | VtProofStep true -> "ProofStep (parallel)" | VtProofMode s -> "ProofMode " ^ s | VtQuery (b,_) -> "Query" ^ string_of_in_script b | VtStm ((VtFinish|VtJoinDocument|VtObserve _|VtPrintDag|VtWait), b) -> @@ -80,9 +81,9 @@ let rec classify_vernac e = | VernacTime e -> classify_vernac_list e | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) (match classify_vernac e with - | ( VtQuery _ | VtProofStep | VtSideff _ + | ( VtQuery _ | VtProofStep _ | VtSideff _ | VtStm _ | VtProofMode _ ), _ as x -> x - | VtQed _, _ -> VtProofStep, VtNow + | VtQed _, _ -> VtProofStep false, VtNow | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow) (* Qed *) | VernacEndProof Admitted | VernacAbort _ -> VtQed VtDrop, VtLater @@ -91,6 +92,7 @@ let rec classify_vernac e = | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _ | VernacCheckMayEval _ -> VtQuery (true,Stateid.dummy), VtLater (* ProofStep *) + | VernacSolve (SelectAllParallel,_,_) -> VtProofStep true, VtLater | VernacProof _ | VernacBullet _ | VernacFocus _ | VernacUnfocus @@ -98,7 +100,7 @@ let rec classify_vernac e = | VernacSolve _ | VernacCheckGuard | VernacUnfocused - | VernacSolveExistential _ -> VtProofStep, VtLater + | VernacSolveExistential _ -> VtProofStep false, VtLater (* Options changing parser *) | VernacUnsetOption (["Default";"Proof";"Using"]) | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow @@ -117,13 +119,15 @@ let rec classify_vernac e = let ids, open_proof = List.fold_left (fun (l,b) (((_,id),_,_,_,p),_) -> id::l, b || p = None) ([],false) l in - if open_proof then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater + if open_proof + then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater else VtSideff ids, VtLater | VernacCoFixpoint (_,l) -> let ids, open_proof = List.fold_left (fun (l,b) (((_,id),_,_,p),_) -> id::l, b || p = None) ([],false) l in - if open_proof then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater + if open_proof + then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater else VtSideff ids, VtLater (* Sideff: apply to all open branches. usually run on master only *) | VernacAssumption (_,_,l) -> |