From 26d180fa0b27edc773fd07c73906e4ed56475200 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 16 Nov 2016 10:51:39 +0100 Subject: [stm] Remove STM-related vernaculars I think these commands never make a lot of sense on scripts other than debugging and we have better methods now. The last remaining command, used for the tty emulation has been renamed to VtBack, but it should go away at some point too once the legacy interfaces are removed. --- stm/stm.ml | 51 +++++++++++++----------------------------------- stm/vernac_classifier.ml | 22 ++++----------------- 2 files changed, 18 insertions(+), 55 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index e387e6322f..0ddaf604ad 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -989,7 +989,7 @@ end = struct (* {{{ *) try match v with | VernacResetInitial -> - VtStm (VtBack Stateid.initial, true), VtNow + VtBack (Stateid.initial, true), VtNow | VernacResetName (_,name) -> let id = VCS.get_branch_pos (VCS.current_branch ()) in (try @@ -997,20 +997,20 @@ end = struct (* {{{ *) fold_until (fun b (id,_,label,_,_) -> if b then `Stop id else `Cont (List.mem name label)) false id in - VtStm (VtBack oid, true), VtNow + VtBack (oid, true), VtNow with Not_found -> - VtStm (VtBack id, true), VtNow) + VtBack (id, true), VtNow) | VernacBack n -> let id = VCS.get_branch_pos (VCS.current_branch ()) in let oid = fold_until (fun n (id,_,_,_,_) -> if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in - VtStm (VtBack oid, true), VtNow + VtBack (oid, true), VtNow | VernacUndo n -> let id = VCS.get_branch_pos (VCS.current_branch ()) in let oid = fold_until (fun n (id,_,_,tactic,undo) -> let value = (if tactic then 1 else 0) - undo in if Int.equal n 0 then `Stop id else `Cont (n-value)) n id in - VtStm (VtBack oid, true), VtLater + VtBack (oid, true), VtLater | VernacUndoTo _ | VernacRestart as e -> let m = match e with VernacUndoTo m -> m | _ -> 0 in @@ -1027,16 +1027,16 @@ end = struct (* {{{ *) 0 id in let oid = fold_until (fun n (id,_,_,_,_) -> if Int.equal n 0 then `Stop id else `Cont (n-1)) (n-m-1) id in - VtStm (VtBack oid, true), VtLater + VtBack (oid, true), VtLater | VernacAbortAll -> let id = VCS.get_branch_pos (VCS.current_branch ()) in let oid = fold_until (fun () (id,vcs,_,_,_) -> match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ()) () id in - VtStm (VtBack oid, true), VtLater + VtBack (oid, true), VtLater | VernacBacktrack (id,_,_) | VernacBackTo id -> - VtStm (VtBack (Stateid.of_int id), not !Flags.print_emacs), VtNow + VtBack (Stateid.of_int id, not !Flags.print_emacs), VtNow | _ -> VtUnknown, VtNow with | Not_found -> @@ -2428,22 +2428,8 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty prerr_endline (fun () -> " classified as: " ^ string_of_vernac_classification c); match c with - (* PG stuff *) - | VtStm(VtPG,false), VtNow -> 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 -> - anomaly(str"classifier: join actions cannot be classified as VtLater") - (* Back *) - | VtStm (VtBack oid, true), w -> + | VtBack(oid, true), w -> let id = VCS.new_node ~id:newtip () in let { mine; others } = Backtrack.branches_of oid in let valid = VCS.get_branch_pos head in @@ -2462,12 +2448,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty VCS.checkout_shallowest_proof_branch (); VCS.commit id (Alias (oid,x)); Backtrack.record (); if w == VtNow then finish (); `Ok - | VtStm (VtBack id, false), VtNow -> + | VtBack (id, false), VtNow -> prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id); Backtrack.backto id; VCS.checkout_shallowest_proof_branch (); Reach.known_state ~cache:(interactive ()) id; `Ok - | VtStm (VtBack id, false), VtLater -> + | VtBack (id, false), VtLater -> anomaly(str"classifier: VtBack + VtLater must imply part_of_script") (* Query *) @@ -2604,15 +2590,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 - vernac_interp Stateid.dummy - { verbose = true; loc = Loc.ghost; indentation = 0; strlen = 0; - expr = VernacShow (ShowGoal OpenSubgoals) } - | _ -> () - end; prerr_endline (fun () -> "processed }}}"); VCS.print (); rc @@ -2674,8 +2651,8 @@ let query ~at ?(report_with=(Stateid.dummy,default_route)) s = let clas = classify_vernac ast in let aast = { verbose = true; indentation; strlen; loc; expr = ast } in match clas with - | VtStm (w,_), _ -> - ignore(process_transaction ~tty:false aast (VtStm (w,false), VtNow)) + | VtBack (w,_), _ -> + ignore(process_transaction ~tty:false aast (VtBack (w,false), VtNow)) | _ -> ignore(process_transaction ~tty:false aast (VtQuery (false,report_with), VtNow))) @@ -2822,7 +2799,7 @@ let interp verb (loc,e) = let print_goals = verb && match clas with | VtQuery _, _ -> false - | (VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _), _ -> true + | (VtProofStep _ | VtBack (_, _) | VtStartProof _), _ -> true | _ -> not !Flags.coqtop_ui in try finish ~print_goals () with e -> diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index dc5be08a37..f9bf9653fd 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -33,10 +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 (VtBack _, b) -> "Stm Back " ^ string_of_in_script b + | VtBack(_, b) -> "Stm Back " ^ string_of_in_script b let string_of_vernac_when = function | VtLater -> "Later" @@ -55,7 +52,7 @@ let declare_vernac_classifier let elide_part_of_script_and_now (a, _) = match a with | VtQuery (_,id) -> VtQuery (false,id), VtNow - | VtStm (x, _) -> VtStm (x, false), VtNow + | VtBack (x, _) -> VtBack (x, false), VtNow | x -> x, VtNow let make_polymorphic (a, b as x) = @@ -69,23 +66,12 @@ 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 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 @@ -98,7 +84,7 @@ let rec classify_vernac e = | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) (match classify_vernac e with | ( VtQuery _ | VtProofStep _ | VtSideff _ - | VtStm _ | VtProofMode _ ), _ as x -> x + | VtBack _ | VtProofMode _ ), _ as x -> x | VtQed _, _ -> VtProofStep { parallel = `No; proof_block_detection = None }, VtNow -- cgit v1.2.3 From bdcf5b040b975a179fe9b2889fea0d38ae4689df Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 18 Nov 2016 08:38:30 +0100 Subject: Revert "Merge remote-tracking branch 'github/pr/360' into v8.6" This reverts commit b00e039b957b8428c21faec5c76f3a3484cde2cf, reversing changes made to ca9e00ff9b2a8ee17430398a5e0bef2345c39341. It turns out that calling from fake_ide the STM commands that were removed by this PR requires an extension of the XML protocol. So postponing the integration. --- stm/stm.ml | 51 +++++++++++++++++++++++++++++++++++------------- stm/vernac_classifier.ml | 22 +++++++++++++++++---- 2 files changed, 55 insertions(+), 18 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 0ddaf604ad..e387e6322f 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -989,7 +989,7 @@ end = struct (* {{{ *) try match v with | VernacResetInitial -> - VtBack (Stateid.initial, true), VtNow + VtStm (VtBack Stateid.initial, true), VtNow | VernacResetName (_,name) -> let id = VCS.get_branch_pos (VCS.current_branch ()) in (try @@ -997,20 +997,20 @@ end = struct (* {{{ *) fold_until (fun b (id,_,label,_,_) -> if b then `Stop id else `Cont (List.mem name label)) false id in - VtBack (oid, true), VtNow + VtStm (VtBack oid, true), VtNow with Not_found -> - VtBack (id, true), VtNow) + VtStm (VtBack id, true), VtNow) | VernacBack n -> let id = VCS.get_branch_pos (VCS.current_branch ()) in let oid = fold_until (fun n (id,_,_,_,_) -> if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in - VtBack (oid, true), VtNow + VtStm (VtBack oid, true), VtNow | VernacUndo n -> let id = VCS.get_branch_pos (VCS.current_branch ()) in let oid = fold_until (fun n (id,_,_,tactic,undo) -> let value = (if tactic then 1 else 0) - undo in if Int.equal n 0 then `Stop id else `Cont (n-value)) n id in - VtBack (oid, true), VtLater + VtStm (VtBack oid, true), VtLater | VernacUndoTo _ | VernacRestart as e -> let m = match e with VernacUndoTo m -> m | _ -> 0 in @@ -1027,16 +1027,16 @@ end = struct (* {{{ *) 0 id in let oid = fold_until (fun n (id,_,_,_,_) -> if Int.equal n 0 then `Stop id else `Cont (n-1)) (n-m-1) id in - VtBack (oid, true), VtLater + VtStm (VtBack oid, true), VtLater | VernacAbortAll -> let id = VCS.get_branch_pos (VCS.current_branch ()) in let oid = fold_until (fun () (id,vcs,_,_,_) -> match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ()) () id in - VtBack (oid, true), VtLater + VtStm (VtBack oid, true), VtLater | VernacBacktrack (id,_,_) | VernacBackTo id -> - VtBack (Stateid.of_int id, not !Flags.print_emacs), VtNow + VtStm (VtBack (Stateid.of_int id), not !Flags.print_emacs), VtNow | _ -> VtUnknown, VtNow with | Not_found -> @@ -2428,8 +2428,22 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty prerr_endline (fun () -> " classified as: " ^ string_of_vernac_classification c); match c with + (* PG stuff *) + | VtStm(VtPG,false), VtNow -> 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 -> + anomaly(str"classifier: join actions cannot be classified as VtLater") + (* Back *) - | VtBack(oid, true), w -> + | VtStm (VtBack oid, true), w -> let id = VCS.new_node ~id:newtip () in let { mine; others } = Backtrack.branches_of oid in let valid = VCS.get_branch_pos head in @@ -2448,12 +2462,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty VCS.checkout_shallowest_proof_branch (); VCS.commit id (Alias (oid,x)); Backtrack.record (); if w == VtNow then finish (); `Ok - | VtBack (id, false), VtNow -> + | VtStm (VtBack id, false), VtNow -> prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id); Backtrack.backto id; VCS.checkout_shallowest_proof_branch (); Reach.known_state ~cache:(interactive ()) id; `Ok - | VtBack (id, false), VtLater -> + | VtStm (VtBack id, false), VtLater -> anomaly(str"classifier: VtBack + VtLater must imply part_of_script") (* Query *) @@ -2590,6 +2604,15 @@ 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 + vernac_interp Stateid.dummy + { verbose = true; loc = Loc.ghost; indentation = 0; strlen = 0; + expr = VernacShow (ShowGoal OpenSubgoals) } + | _ -> () + end; prerr_endline (fun () -> "processed }}}"); VCS.print (); rc @@ -2651,8 +2674,8 @@ let query ~at ?(report_with=(Stateid.dummy,default_route)) s = let clas = classify_vernac ast in let aast = { verbose = true; indentation; strlen; loc; expr = ast } in match clas with - | VtBack (w,_), _ -> - ignore(process_transaction ~tty:false aast (VtBack (w,false), VtNow)) + | VtStm (w,_), _ -> + ignore(process_transaction ~tty:false aast (VtStm (w,false), VtNow)) | _ -> ignore(process_transaction ~tty:false aast (VtQuery (false,report_with), VtNow))) @@ -2799,7 +2822,7 @@ let interp verb (loc,e) = let print_goals = verb && match clas with | VtQuery _, _ -> false - | (VtProofStep _ | VtBack (_, _) | VtStartProof _), _ -> true + | (VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _), _ -> true | _ -> not !Flags.coqtop_ui in try finish ~print_goals () with e -> diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index f9bf9653fd..dc5be08a37 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -33,7 +33,10 @@ 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 - | VtBack(_, b) -> "Stm Back " ^ string_of_in_script b + | VtStm ((VtFinish|VtJoinDocument|VtObserve _|VtPrintDag|VtWait), b) -> + "Stm " ^ string_of_in_script b + | VtStm (VtPG, b) -> "Stm PG " ^ string_of_in_script b + | VtStm (VtBack _, b) -> "Stm Back " ^ string_of_in_script b let string_of_vernac_when = function | VtLater -> "Later" @@ -52,7 +55,7 @@ let declare_vernac_classifier let elide_part_of_script_and_now (a, _) = match a with | VtQuery (_,id) -> VtQuery (false,id), VtNow - | VtBack (x, _) -> VtBack (x, false), VtNow + | VtStm (x, _) -> VtStm (x, false), VtNow | x -> x, VtNow let make_polymorphic (a, b as x) = @@ -66,12 +69,23 @@ 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 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 @@ -84,7 +98,7 @@ let rec classify_vernac e = | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) (match classify_vernac e with | ( VtQuery _ | VtProofStep _ | VtSideff _ - | VtBack _ | VtProofMode _ ), _ as x -> x + | VtStm _ | VtProofMode _ ), _ as x -> x | VtQed _, _ -> VtProofStep { parallel = `No; proof_block_detection = None }, VtNow -- cgit v1.2.3 From 3642314974b3aca6eb522c37e7e4efd226e6ebc8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 29 Nov 2016 17:50:11 +0100 Subject: STM: cur_id must be invalid if an error occurs (fix #5191) Line erroneously removed in 17f3346c --- stm/stm.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index e387e6322f..b4331dc460 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -896,6 +896,7 @@ end = struct (* {{{ *) with e -> let (e, info) = CErrors.push e in let good_id = !cur_id in + cur_id := Stateid.dummy; VCS.reached id; let ie = match Stateid.get info, safe_id with -- cgit v1.2.3 From 23ffecc39a064775724ad524bd97f30fb8e763cd Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 17 Jan 2017 10:47:34 +0100 Subject: STM: fix run-time classification of VernacInstance (fix #5313) --- stm/stm.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index b4331dc460..f577994ffa 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2584,12 +2584,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty if not in_proof && Proof_global.there_are_pending_proofs () then begin let bname = VCS.mk_branch_name x in - let opacity_of_produced_term = - match x.expr with + let rec opacity_of_produced_term = function (* This AST is ambiguous, hence we check it dynamically *) | VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity + | VernacLocal (_,e) -> opacity_of_produced_term e | _ -> Doesn'tGuaranteeOpacity in - VCS.commit id (Fork (x,bname,opacity_of_produced_term,[])); + VCS.commit id (Fork (x,bname,opacity_of_produced_term x.expr,[])); let proof_mode = default_proof_mode () in VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1)); Proof_global.activate_proof_mode proof_mode; -- cgit v1.2.3 From a54dccb53fa8d6c12745b5f7b2c3c993a915b5bd Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 2 Dec 2016 12:23:14 +0100 Subject: Fix a typo in STM universe communications. --- stm/asyncTaskQueue.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index fa6422cdc5..8acc3c233a 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -170,7 +170,7 @@ module Make(T : Task) = struct | Unix.WSIGNALED sno -> Printf.sprintf "signalled(%d)" sno | Unix.WSTOPPED sno -> Printf.sprintf "stopped(%d)" sno) in let more_univs n = - CList.init 10 (fun _ -> + CList.init n (fun _ -> Universes.new_univ_level (Global.current_dirpath ())) in let rec kill_if () = -- cgit v1.2.3