From 076efd5f8d17f1b73bcc7669641b89f86819e3c9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Mar 2018 19:20:01 +0200 Subject: stm: don't propagate side effects when editing a proof --- stm/stm.ml | 35 ++++++++++++++++++++++------------- 1 file changed, 22 insertions(+), 13 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 4b49d1998..e970a02ee 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2884,18 +2884,22 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); rc - (* Side effect on all branches *) + (* Side effect in a (still open) proof is replayed on all branches*) | VtSideff l, w -> - let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in let id = VCS.new_node ~id:newtip () in - VCS.checkout VCS.Branch.master; - VCS.commit id (mkTransCmd x l in_proof `MainQueue); - (* We can't replay a Definition since universes may be differently - * inferred. This holds in Coq >= 8.5 *) - let action = match Vernacprop.under_control x.expr with - | VernacDefinition(_, _, DefineBody _) -> CherryPickEnv - | _ -> ReplayCommand x in - VCS.propagate_sideff ~action; + begin match (VCS.get_branch head).VCS.kind with + | `Edit _ -> VCS.commit id (mkTransCmd x l true `MainQueue); + | `Master -> VCS.commit id (mkTransCmd x l false `MainQueue); + | `Proof _ -> + VCS.checkout VCS.Branch.master; + VCS.commit id (mkTransCmd x l true `MainQueue); + (* We can't replay a Definition since universes may be differently + * inferred. This holds in Coq >= 8.5 *) + let action = match Vernacprop.under_control x.expr with + | VernacDefinition(_, _, DefineBody _) -> CherryPickEnv + | _ -> ReplayCommand x in + VCS.propagate_sideff ~action; + end; VCS.checkout_shallowest_proof_branch (); Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok @@ -2924,9 +2928,14 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1)); Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"]; end else begin - VCS.commit id (mkTransCmd x [] in_proof `MainQueue); - (* We hope it can be replayed, but we can't really know *) - VCS.propagate_sideff ~action:(ReplayCommand x); + begin match (VCS.get_branch head).VCS.kind with + | `Edit _ -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue); + | `Master -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue); + | `Proof _ -> + VCS.commit id (mkTransCmd x [] in_proof `MainQueue); + (* We hope it can be replayed, but we can't really know *) + VCS.propagate_sideff ~action:(ReplayCommand x); + end; VCS.checkout_shallowest_proof_branch (); end in State.define ~safe_id:head_id ~cache:`Yes step id; -- cgit v1.2.3