diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-06 05:50:07 -0400 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-06 14:04:33 -0400 |
commit | e4d66a03148243f7611f4d7c164e775877184e03 (patch) | |
tree | 0a2581fd31dc3603db6e333de365f230354544a2 | |
parent | 0307140281395e8ffa16f2af9f946cc53d540b17 (diff) |
Error box detection run only on error
Advantage: 0 cost if no error occurs
Disadvantage: a box *must* end with the error absorbing command
-rw-r--r-- | stm/proofBlockDelimiter.ml | 3 | ||||
-rw-r--r-- | stm/stm.ml | 87 | ||||
-rw-r--r-- | test-suite/interactive/proof_block.v | 12 |
3 files changed, 64 insertions, 38 deletions
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index 7dec43d1a..ed8553d4b 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -23,6 +23,8 @@ val crawl : val unit_val : Stm.DynBlockData.t val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet +val of_vernac_expr_val : Vernacexpr.vernac_expr -> Stm.DynBlockData.t +val to_vernac_expr_val : Stm.DynBlockData.t -> Vernacexpr.vernac_expr end = struct @@ -30,6 +32,7 @@ let unit_tag = DynBlockData.create "unit" let unit_val = DynBlockData.Easy.inj () unit_tag let of_bullet_val, to_bullet_val = DynBlockData.Easy.make_dyn "bullet" +let of_vernac_expr_val, to_vernac_expr_val = DynBlockData.Easy.make_dyn "vernac_expr" let simple_goal sigma g gs = let open Evar in diff --git a/stm/stm.ml b/stm/stm.ml index 89d384fdd..0e33bea3b 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -170,11 +170,13 @@ type branch_type = | `Proof of proof_mode * depth | `Edit of proof_mode * Stateid.t * Stateid.t * vernac_qed_type * Vcs_.Branch.t ] +(* TODO 8.7 : split commands and tactics, since this type is too messy now *) type cmd_t = { ctac : bool; (* is a tactic *) ceff : bool; (* is a side-effecting command in the middle of a proof *) cast : aast; cids : Id.t list; + cblock : proof_block_name option; cqueue : [ `MainQueue | `TacQueue of cancel_switch | `QueryQueue of cancel_switch @@ -204,6 +206,10 @@ type step = | `Alias of alias_t ] type visit = { step : step; next : Stateid.t } +let mkTransTac cast cblock cqueue = + Cmd { ctac = true; cast; cblock; cqueue; cids = []; ceff = false } +let mkTransCmd cast cids ceff cqueue = + Cmd { ctac = false; cast; cblock = None; cqueue; cids; ceff } (* Parts of the system state that are morally part of the proof state *) let summary_pstate = [ Evarutil.meta_counter_summary_name; @@ -591,7 +597,6 @@ end = struct (* {{{ *) let props = Stateid.Set.fold (fun n pl -> Vcs_.property_of !vcs n @ pl) nodes [] in let props = CList.sort_uniquize Vcs_.Dag.Property.compare props in - (* XXX check if par: works here, since we copy a single node *) List.fold_left (fun v p -> Vcs_.create_property v (Stateid.Set.elements (Vcs_.Dag.Property.having_it p)) @@ -1110,22 +1115,24 @@ let prev_node { id } = mk_doc_node id (VCS.visit id) let cur_node id = mk_doc_node id (VCS.visit id) -let detect_proof_block id = function - | Some name when !Flags.async_proofs_tac_error_resilience && - !Flags.async_proofs_mode != Flags.APoff -> - begin match cur_node id with +let detect_proof_block id name = + let name = match name with None -> "indent" | Some x -> x in + if !Flags.async_proofs_tac_error_resilience && + (if Flags.async_proofs_is_master () then + !Flags.async_proofs_mode != Flags.APoff else true) + then + match cur_node id with + | None -> () + | Some entry_point -> try + let static, _ = List.assoc name !proof_block_delimiters in + begin match static { prev_node; entry_point } with | None -> () - | Some entry_point -> try - let static, _ = List.assoc name !proof_block_delimiters in - begin match static { prev_node; entry_point } with - | None -> () - | Some ({ start; stop } as decl) -> - VCS.create_error_bound_box decl name - end - with Not_found -> - Errors.errorlabstrm "STM" - (str "Unknown proof block delimiter " ++ str name) end - | _ -> () + | Some ({ start; stop } as decl) -> + VCS.create_error_bound_box decl name + end + with Not_found -> + Errors.errorlabstrm "STM" + (str "Unknown proof block delimiter " ++ str name) (****************************** THE SCHEDULER *********************************) (******************************************************************************) @@ -1978,7 +1985,12 @@ let wall_clock_last_fork = ref 0.0 let known_state ?(redefine_qed=false) ~cache id = - let error_absorbing_tactic id exn = + let error_absorbing_tactic id blockname exn = + (* We keep the static/dynamic part of block detection separate, since + the static part could be performed earlier. As of today there is + no advantage in doing so since no UI can exploit such piece of info *) + detect_proof_block id blockname; + let boxes = VCS.box_of id in let valid_boxes = CList.map_filter (function | ErrorBound ({ stop } as decl, name) when Stateid.equal stop id -> @@ -1995,8 +2007,11 @@ let known_state ?(redefine_qed=false) ~cache id = | `ValidBlock { base_state; goals_to_admit; recovery_command } -> begin let tac = let open Proofview.Notations in - Proofview.Unsafe.tclSETGOALS goals_to_admit <*> - Proofview.give_up in + Proofview.Goal.nf_enter { enter = fun gl -> + if CList.mem_f Evar.equal + (Proofview.Goal.goal gl) goals_to_admit then + Proofview.give_up else Proofview.tclUNIT () + } in match (VCS.get_info base_state).state with | Valid { proof } -> Proof_global.unfreeze proof; @@ -2015,7 +2030,7 @@ let known_state ?(redefine_qed=false) ~cache id = in (* Absorb tactic errors from f () *) - let resilient_tactic id f = + let resilient_tactic id blockname f = if not !Flags.async_proofs_tac_error_resilience || (Flags.async_proofs_is_master () && !Flags.async_proofs_mode = Flags.APoff) @@ -2024,7 +2039,7 @@ let known_state ?(redefine_qed=false) ~cache id = try f () with e when Errors.noncritical e -> let ie = Errors.push e in - error_absorbing_tactic id ie in + error_absorbing_tactic id blockname ie in (* Absorb errors from f x *) let resilient_command f x = if not !Flags.async_proofs_cmd_error_resilience || @@ -2064,8 +2079,8 @@ let known_state ?(redefine_qed=false) ~cache id = ), cache, true | `Cmd { cast = x; cqueue = `SkipQueue } -> (fun () -> reach view.next), cache, true - | `Cmd { cast = x; cqueue = `TacQueue cancel } -> (fun () -> - resilient_tactic id (fun () -> + | `Cmd { cast = x; cqueue = `TacQueue cancel; cblock } -> (fun () -> + resilient_tactic id cblock (fun () -> reach ~cache:`Shallow view.next; Hooks.(call tactic_being_run true); Partac.vernac_interp @@ -2077,8 +2092,8 @@ let known_state ?(redefine_qed=false) ~cache id = reach view.next; Query.vernac_interp cancel view.next id x ), cache, false - | `Cmd { cast = x; ceff = eff; ctac = true } -> (fun () -> - resilient_tactic id (fun () -> + | `Cmd { cast = x; ceff = eff; ctac = true; cblock } -> (fun () -> + resilient_tactic id cblock (fun () -> reach view.next; Hooks.(call tactic_being_run true); vernac_interp id x; @@ -2443,8 +2458,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty may_pierce_opaque x then `SkipQueue else `MainQueue in - VCS.commit id (Cmd { - ctac=false;ceff=false;cast = x; cids = []; cqueue = queue }); + VCS.commit id (mkTransCmd x [] false queue); Backtrack.record (); if w == VtNow then finish (); `Ok | VtQuery (false,_), VtLater -> anomaly(str"classifier: VtQuery + VtLater must imply part_of_script") @@ -2467,8 +2481,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty anomaly(str"VtProofMode must be executed VtNow") | VtProofMode mode, VtNow -> let id = VCS.new_node ~id:newtip () in - VCS.commit id (Cmd { - ctac=false;ceff=false;cast = x;cids=[];cqueue = `MainQueue}); + VCS.commit id (mkTransCmd x [] false `MainQueue); List.iter (fun bn -> match VCS.get_branch bn with | { VCS.root; kind = `Master; pos } -> () @@ -2483,12 +2496,14 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty Backtrack.record (); finish (); `Ok - | VtProofStep { parallel; proof_block_detection }, w -> + | VtProofStep { parallel; proof_block_detection = cblock }, w -> let id = VCS.new_node ~id:newtip () in let queue = if parallel then `TacQueue (ref false) else `MainQueue in - VCS.commit id (Cmd { - ctac = true;ceff = false;cast = x;cids = [];cqueue = queue }); - detect_proof_block id proof_block_detection; + VCS.commit id (mkTransTac x cblock queue); + (* Static proof block detection delayed until an error really occurs. + If/when and UI will make something useful with this piece of info, + detection should occur here. + detect_proof_block id cblock; *) Backtrack.record (); if w == VtNow then finish (); `Ok | VtQed keep, w -> let valid = if tty then Some(VCS.get_branch_pos head) else None in @@ -2505,8 +2520,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty 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 (Cmd { - ctac=false;ceff=in_proof;cast=x;cids=l;cqueue=`MainQueue }); + 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 replay = match x.expr with @@ -2541,8 +2555,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1)); Proof_global.activate_proof_mode proof_mode; end else begin - VCS.commit id (Cmd { - ctac=false;ceff=in_proof;cast=x;cids=[];cqueue=`MainQueue }); + VCS.commit id (mkTransCmd x [] in_proof `MainQueue); (* We hope it can be replayed, but we can't really know *) VCS.propagate_sideff ~replay:(Some x); VCS.checkout_shallowest_proof_branch (); diff --git a/test-suite/interactive/proof_block.v b/test-suite/interactive/proof_block.v index ff920b671..31e349376 100644 --- a/test-suite/interactive/proof_block.v +++ b/test-suite/interactive/proof_block.v @@ -1,3 +1,13 @@ +Goal False /\ True. +Proof. +split. + idtac. + idtac. + exact I. +idtac. +idtac. +exact I. +Qed. Lemma baz : (exists n, n = 3 /\ n = 3) /\ True. Proof. @@ -26,7 +36,7 @@ Qed. Lemma foo1 : False /\ True. Proof. split. - exact I. + { exact I. } { exact I. } Qed. |