From 584a832d4f681d34c7cbdd87d9ceb7a742b39959 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 22 Feb 2017 00:23:10 +0100 Subject: [stm] Remove some obsolete vernacs/classification. This is the good parts of PR #360. IIUC, these vernacular were meant mostly for debugging and they are not supposed to be of any use these days. Back and join are still there not to break the testing infrastructure, but some day they should go away. --- stm/stm.ml | 23 +++-------------------- stm/vernac_classifier.ml | 21 ++------------------- 2 files changed, 5 insertions(+), 39 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index b9dbb78917..b592aab0da 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2525,20 +2525,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty stm_prerr_endline (fun () -> " classified as: " ^ string_of_vernac_classification c); match c with - (* PG stuff *) - | VtStm(VtPG,false), VtNow -> stm_vernac_interp Stateid.dummy x; `Ok - | VtStm(VtPG,_), _ -> anomaly(str "PG command in script or VtLater") (* Joining various parts of the document *) | VtStm (VtJoinDocument, b), VtNow -> join (); `Ok - | VtStm (VtFinish, b), VtNow -> finish (); `Ok - | VtStm (VtWait, b), VtNow -> finish (); wait (); `Ok - | VtStm (VtPrintDag, b), VtNow -> - VCS.print ~now:true (); `Ok - | VtStm (VtObserve id, b), VtNow -> observe id; `Ok - | VtStm ((VtObserve _ | VtFinish | VtJoinDocument - |VtPrintDag |VtWait),_), VtLater -> + | VtStm (VtWait, b), VtNow -> finish (); wait (); `Ok + | VtStm ((VtJoinDocument|VtWait),_), VtLater -> anomaly(str"classifier: join actions cannot be classified as VtLater") - + (* Back *) | VtStm (VtBack oid, true), w -> let id = VCS.new_node ~id:newtip () in @@ -2701,15 +2693,6 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty | VtUnknown, VtLater -> anomaly(str"classifier: VtUnknown must imply VtNow") end in - (* Proof General *) - begin match expr with - | VernacStm (PGLast _) -> - if not (VCS.Branch.equal head VCS.Branch.master) then - stm_vernac_interp Stateid.dummy - { verbose = true; loc = Loc.ghost; indentation = 0; strlen = 0; - expr = VernacShow (ShowGoal OpenSubgoals) } - | _ -> () - end; stm_prerr_endline (fun () -> "processed }}}"); VCS.print (); rc diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index dc5be08a37..5908c09d08 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -33,9 +33,7 @@ let string_of_vernac_type = function | VtQuery (b,(id,route)) -> "Query " ^ string_of_in_script b ^ " report " ^ Stateid.to_string id ^ " route " ^ string_of_int route - | VtStm ((VtFinish|VtJoinDocument|VtObserve _|VtPrintDag|VtWait), b) -> - "Stm " ^ string_of_in_script b - | VtStm (VtPG, b) -> "Stm PG " ^ string_of_in_script b + | VtStm ((VtJoinDocument|VtWait), b) -> "Stm " ^ string_of_in_script b | VtStm (VtBack _, b) -> "Stm Back " ^ string_of_in_script b let string_of_vernac_when = function @@ -52,12 +50,6 @@ let declare_vernac_classifier = classifiers := !classifiers @ [s,f] -let elide_part_of_script_and_now (a, _) = - match a with - | VtQuery (_,id) -> VtQuery (false,id), VtNow - | VtStm (x, _) -> VtStm (x, false), VtNow - | x -> x, VtNow - let make_polymorphic (a, b as x) = match a with | VtStartProof (x, _, ids) -> @@ -69,23 +61,14 @@ let set_undo_classifier f = undo_classifier := f let rec classify_vernac e = let static_classifier e = match e with - (* PG compatibility *) - | VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"]) - | VernacSetOption ((["Silent"]|["Undo"]|["Printing";"Depth"]),_) - when !Flags.print_emacs -> VtStm(VtPG,false), VtNow (* 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. *) | VernacSetOption (["Universe"; "Polymorphism"],_) | VernacUnsetOption (["Universe"; "Polymorphism"]) -> VtSideff [], VtNow (* Stm *) - | VernacStm Finish -> VtStm (VtFinish, true), VtNow - | VernacStm Wait -> VtStm (VtWait, true), VtNow + | VernacStm Wait -> VtStm (VtWait, true), VtNow | VernacStm JoinDocument -> VtStm (VtJoinDocument, true), VtNow - | VernacStm PrintDag -> VtStm (VtPrintDag, true), VtNow - | VernacStm (Observe id) -> VtStm (VtObserve id, true), VtNow - | VernacStm (Command x) -> elide_part_of_script_and_now (classify_vernac x) - | VernacStm (PGLast x) -> fst (classify_vernac x), VtNow (* Nested vernac exprs *) | VernacProgram e -> classify_vernac e | VernacLocal (_,e) -> classify_vernac e -- cgit v1.2.3 From c5e6f5ee545ee24541836233a18c0c772077fbdf Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Wed, 8 Mar 2017 14:57:16 -0500 Subject: Run non-tactic comands without resilient_command --- stm/stm.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index f577994ffa..56243b76f9 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2136,10 +2136,13 @@ let known_state ?(redefine_qed=false) ~cache id = if eff then update_global_env () ), (if eff then `Yes else cache), true | `Cmd { cast = x; ceff = eff } -> (fun () -> - resilient_command reach view.next; - vernac_interp id x; - if eff then update_global_env () - ), (if eff then `Yes else cache), true + (match !Flags.async_proofs_mode with + | Flags.APon | Flags.APonLazy -> + resilient_command reach view.next + | Flags.APoff -> reach view.next); + vernac_interp id x; + if eff then update_global_env () + ), (if eff then `Yes else cache), true | `Fork ((x,_,_,_), None) -> (fun () -> resilient_command reach view.next; vernac_interp id x; -- cgit v1.2.3