From c352873936db93c251c544383853474736f128d6 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 25 Jan 2019 00:48:36 +0100 Subject: Remove VtUnknown classification This clean-up removes the dependency of the current proof mode (and hence the parsing state) on unification. The current proof mode can now be known simply by parsing and elaborating attributes. We give access to attributes from the classifier for this purpose. We remove the infamous `VtUnknown` code path in the STM which is known to be buggy. Fixes #3632 #3890 #4638. --- stm/stm.ml | 51 +----------------------------------------------- stm/vernac_classifier.ml | 36 ++++++++++++++++++++-------------- 2 files changed, 22 insertions(+), 65 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 21618bc044..6f7cefb582 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -364,7 +364,6 @@ module VCS : sig val set_parsing_state : id -> Vernacstate.Parser.state -> unit val get_parsing_state : id -> Vernacstate.Parser.state option val get_proof_mode : id -> Pvernac.proof_mode option - val set_proof_mode : id -> Pvernac.proof_mode option -> unit (* cuts from start -> stop, raising Expired if some nodes are not there *) val slice : block_start:id -> block_stop:id -> vcs @@ -572,6 +571,7 @@ end = struct (* {{{ *) (match Vernacprop.under_control x with | VernacDefinition (_,({CAst.v=Name i},_),_) -> Id.to_string i | VernacStartTheoremProof (_,[({CAst.v=i},_),_]) -> Id.to_string i + | VernacInstance (_,(({CAst.v=Name i},_),_,_),_,_) -> Id.to_string i | _ -> "branch") let edit_branch = Branch.make "edit" let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind @@ -611,7 +611,6 @@ end = struct (* {{{ *) info.state <- new_state let get_proof_mode id = (get_info id).proof_mode - let set_proof_mode id pm = (get_info id).proof_mode <- pm let reached id = let info = get_info id in @@ -3050,53 +3049,6 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) VCS.set_parsing_state id parsing_state) new_ids; `Ok - (* Unknown: we execute it, check for open goals and propagate sideeff *) - | VtUnknown, VtNow -> - let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in - if not (get_allow_nested_proofs ()) && in_proof then - "Commands which may open proofs are not allowed in a proof unless you turn option Nested Proofs Allowed on." - |> Pp.str - |> (fun s -> (UserError (None, s), Exninfo.null)) - |> State.exn_on ~valid:Stateid.dummy newtip - |> Exninfo.iraise - else - let id = VCS.new_node ~id:newtip proof_mode () in - let head_id = VCS.get_branch_pos head in - let _st : unit = Reach.known_state ~doc ~cache:true head_id in (* ensure it is ok *) - let step () = - VCS.checkout VCS.Branch.master; - let mid = VCS.get_branch_pos VCS.Branch.master in - let _st' : unit = Reach.known_state ~doc ~cache:(VCS.is_interactive ()) mid in - let st = Vernacstate.freeze_interp_state ~marshallable:false in - ignore(stm_vernac_interp id st x); - (* Vernac x may or may not start a proof *) - if not in_proof && PG_compat.there_are_pending_proofs () then - begin - let bname = VCS.mk_branch_name x in - let opacity_of_produced_term = function - (* This AST is ambiguous, hence we check it dynamically *) - | VernacInstance (_,_ , None, _) -> GuaranteesOpacity - | _ -> Doesn'tGuaranteeOpacity in - VCS.commit id (Fork (x,bname,opacity_of_produced_term (Vernacprop.under_control x.expr),[])); - VCS.set_proof_mode id (Some (Vernacentries.get_default_proof_mode ())); - VCS.branch bname (`Proof (VCS.proof_nesting () + 1)); - end else begin - 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 *) - ignore(VCS.propagate_sideff ~action:(ReplayCommand x)); - end; - VCS.checkout_shallowest_proof_branch (); - end in - State.define ~doc ~safe_id:head_id ~cache:true step id; - Backtrack.record (); `Ok - - | VtUnknown, VtLater -> - anomaly(str"classifier: VtUnknown must imply VtNow.") - | VtProofMode pm, VtNow -> let proof_mode = Pvernac.lookup_proof_mode pm in let id = VCS.new_node ~id:newtip proof_mode () in @@ -3106,7 +3058,6 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) | VtProofMode _, VtLater -> anomaly(str"classifier: VtProofMode must imply VtNow.") - end in let pr_rc rc = match rc with | `Ok -> Pp.(seq [str "newtip ("; str (Stateid.to_string (VCS.cur_tip ())); str ")"]) diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 4a4c5c94e9..7cecd801e4 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -21,7 +21,6 @@ let string_of_parallel = function | `No -> "" let string_of_vernac_type = function - | VtUnknown -> "Unknown" | VtStartProof _ -> "StartProof" | VtSideff _ -> "Sideff" | VtQed (VtKeep VtKeepAxiom) -> "Qed(admitted)" @@ -61,7 +60,7 @@ let options_affecting_stm_scheduling = ] let classify_vernac e = - let static_classifier ~poly e = match e with + let static_classifier ~atts e = match e with (* Univ poly compatibility: we run it now, so that we can just * look at Flags in stm.ml. Would be nicer to have the stm * look at the entire dag to detect this option. *) @@ -97,15 +96,18 @@ let classify_vernac e = VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i), VtLater | VernacDefinition (_,({v=i},_),ProveBody _) -> - let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in - VtStartProof(guarantee, idents_of_name i), VtLater + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in + let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in + VtStartProof(guarantee, idents_of_name i), VtLater | VernacStartTheoremProof (_,l) -> - let ids = List.map (fun (({v=i}, _), _) -> i) l in - let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in - VtStartProof (guarantee,ids), VtLater + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in + let ids = List.map (fun (({v=i}, _), _) -> i) l in + let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in + VtStartProof (guarantee,ids), VtLater | VernacFixpoint (discharge,l) -> + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in let guarantee = - if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity + if discharge = Decl_kinds.DoDischarge || polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in let ids, open_proof = @@ -115,8 +117,9 @@ let classify_vernac e = then VtStartProof (guarantee,ids), VtLater else VtSideff ids, VtLater | VernacCoFixpoint (discharge,l) -> + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in let guarantee = - if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity + if discharge = Decl_kinds.DoDischarge || polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in let ids, open_proof = @@ -185,8 +188,12 @@ let classify_vernac e = | VernacDeclareMLModule _ | VernacContext _ (* TASSI: unsure *) -> VtSideff [], VtNow | VernacProofMode pm -> VtProofMode pm, VtNow - (* These are ambiguous *) - | VernacInstance _ -> VtUnknown, VtNow + | VernacInstance (_,((name,_),_,_),None,_) when not (Attributes.parse_drop_extra Attributes.program atts) -> + let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in + let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in + VtStartProof (guarantee, idents_of_name name.CAst.v), VtLater + | VernacInstance (_,((name,_),_,_),_,_) -> + VtSideff (idents_of_name name.CAst.v), VtLater (* Stm will install a new classifier to handle these *) | VernacBack _ | VernacAbortAll | VernacUndoTo _ | VernacUndo _ @@ -201,9 +208,8 @@ let classify_vernac e = with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".") in let rec static_control_classifier v = v |> CAst.with_val (function - | VernacExpr (f, e) -> - let poly = Attributes.(parse_drop_extra polymorphic_nowarn f) in - static_classifier ~poly e + | VernacExpr (atts, e) -> + static_classifier ~atts e | VernacTimeout (_,e) -> static_control_classifier e | VernacTime (_,e) | VernacRedirect (_, e) -> static_control_classifier e @@ -214,6 +220,6 @@ let classify_vernac e = | VtQed _, _ -> VtProofStep { parallel = `No; proof_block_detection = None }, VtLater - | (VtStartProof _ | VtUnknown | VtProofMode _), _ -> VtQuery, VtLater)) + | (VtStartProof _ | VtProofMode _), _ -> VtQuery, VtLater)) in static_control_classifier e -- cgit v1.2.3