From 168c8db946494694c5c32b9f2345c9a2830f03da Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 7 Jun 2017 21:31:40 +0200 Subject: [stm] More fixes for nested commands [bugzilla 5589] --- stm/stm.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index a79bf54267..11aca16272 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2046,7 +2046,8 @@ let collect_proof keep cur hd brkind id = | `ASync(_,pua,_,name,_) -> `Sync (name,pua,why) in let check_policy rc = if async_policy () then rc else make_sync `Policy rc in match cur, (VCS.visit id).step, brkind with - | (parent, { expr = VernacExactProof _ }), `Fork _, _ -> + | (parent, { expr = VernacExactProof _ }), `Fork _, _ + | (parent, { expr = VernacTime (_, VernacExactProof _) }), `Fork _, _ -> `Sync (no_name,None,`Immediate) | _, _, { VCS.kind = `Edit _ } -> check_policy (collect (Some cur) [] id) | _ -> -- cgit v1.2.3 From f610068823b33bdc0af752a646df05b98489d7ce Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 11 Jun 2017 06:08:02 +0200 Subject: [proof] Deprecate redundant wrappers. As we would like to reduce the role of proof_global in future versions, we start to deprecate old compatibility aliases in `Pfedit` in favor of the real functions underlying the 8.5 proof engine. We also deprecate a couple of alias types and explicitly mark the few remaining uses of `Pfedit`. --- stm/stm.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index a79bf54267..1580b451d0 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -931,7 +931,7 @@ let show_script ?proof () = try let prf = try match proof with - | None -> Some (Pfedit.get_current_proof_name ()) + | None -> Some (Proof_global.get_current_proof_name ()) | Some (p,_) -> Some (p.Proof_global.id) with Proof_global.NoCurrentProof -> None in -- cgit v1.2.3 From 9468e4b49bd2f397b5e1bd2b7994cc84929fb6ac Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 27 Apr 2017 20:16:35 +0200 Subject: Fix bugs and add an option for cumulativity --- stm/vernac_classifier.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 471e05e458..87d9e411a7 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -142,7 +142,7 @@ let rec classify_vernac e = let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> snd id) l) l) in VtSideff ids, VtLater | VernacDefinition (_,((_,id),_),DefineBody _) -> VtSideff [id], VtLater - | VernacInductive (_,_,l) -> + | VernacInductive (_, _,_,l) -> let ids = List.map (fun (((_,((_,id),_)),_,_,_,cl),_) -> id :: match cl with | Constructors l -> List.map (fun (_,((_,id),_)) -> id) l | RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @ -- cgit v1.2.3 From d8874dd855d748aaaf504890487ab15ffd7a677d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 12 Jun 2017 11:41:40 +0200 Subject: [ide] Add route_id parameter to query call. This is necessary in order for clients to identify the results of queries. This is a minor breaking change of the protocol, affecting only this particular call. This change is necessary in order to fix bug ####. --- stm/stm.ml | 23 +++++++++++++---------- stm/stm.mli | 2 +- stm/vernac_classifier.ml | 10 +++------- 3 files changed, 17 insertions(+), 18 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 8ca50e2d54..071d2edf98 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2520,23 +2520,26 @@ let process_transaction ?(newtip=Stateid.fresh ()) anomaly(str"classifier: VtBack + VtLater must imply part_of_script.") (* Query *) - | VtQuery (false,(report_id,route)), VtNow -> - (try stm_vernac_interp report_id ~route x - with e -> - let e = CErrors.push e in - Exninfo.iraise (State.exn_on ~valid:Stateid.dummy report_id e)); `Ok - | VtQuery (true,(report_id,_)), w -> - assert(Stateid.equal report_id Stateid.dummy); + | VtQuery (false, route), VtNow -> + begin + let query_sid = VCS.cur_tip () in + try stm_vernac_interp (VCS.cur_tip ()) x + with e -> + let e = CErrors.push e in + Exninfo.iraise (State.exn_on ~valid:Stateid.dummy query_sid e) + end; `Ok + | VtQuery (true, _route), w -> let id = VCS.new_node ~id:newtip () in let queue = if !Flags.async_proofs_full then `QueryQueue (ref false) else if Flags.(!compilation_mode = BuildVio) && VCS.((get_branch head).kind = `Master) && may_pierce_opaque x - then `SkipQueue + then `SkipQueue else `MainQueue in 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.") @@ -2766,7 +2769,7 @@ type focus = { tip : Stateid.t } -let query ~at ?(report_with=(Stateid.dummy,default_route)) s = +let query ~at ~route s = Future.purify (fun s -> if Stateid.equal at Stateid.dummy then finish () else Reach.known_state ~cache:`Yes at; @@ -2779,7 +2782,7 @@ let query ~at ?(report_with=(Stateid.dummy,default_route)) s = | VtStm (w,_), _ -> ignore(process_transaction aast (VtStm (w,false), VtNow)) | _ -> - ignore(process_transaction aast (VtQuery (false,report_with), VtNow))) + ignore(process_transaction aast (VtQuery (false, route), VtNow))) s let edit_at id = diff --git a/stm/stm.mli b/stm/stm.mli index b150f97489..188b176bab 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -34,7 +34,7 @@ val add : ontop:Stateid.t -> ?newtip:Stateid.t -> throwing away side effects except messages. Feedback will be sent with [report_with], which defaults to the dummy state id *) val query : - at:Stateid.t -> ?report_with:(Stateid.t * Feedback.route_id) -> Pcoq.Gram.coq_parsable -> unit + at:Stateid.t -> route:Feedback.route_id -> Pcoq.Gram.coq_parsable -> unit (* [edit_at id] is issued to change the editing zone. [`NewTip] is returned if the requested id is the new document tip hence the document portion following diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 471e05e458..d25861d5a6 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -30,9 +30,7 @@ let string_of_vernac_type = function "ProofStep " ^ string_of_parallel parallel ^ Option.default "" proof_block_detection | VtProofMode s -> "ProofMode " ^ s - | VtQuery (b,(id,route)) -> - "Query " ^ string_of_in_script b ^ " report " ^ Stateid.to_string id ^ - " route " ^ string_of_int route + | VtQuery (b, route) -> "Query " ^ string_of_in_script b ^ " route " ^ string_of_int route | VtStm ((VtJoinDocument|VtWait), b) -> "Stm " ^ string_of_in_script b | VtStm (VtBack _, b) -> "Stm Back " ^ string_of_in_script b @@ -92,8 +90,7 @@ let rec classify_vernac e = | VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater (* Query *) | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _ - | VernacCheckMayEval _ -> - VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater + | VernacCheckMayEval _ -> VtQuery (true,Feedback.default_route), VtLater (* ProofStep *) | VernacProof _ | VernacFocus _ | VernacUnfocus @@ -213,7 +210,6 @@ let rec classify_vernac e = make_polymorphic res else res -let classify_as_query = - VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater +let classify_as_query = VtQuery (true,Feedback.default_route), VtLater let classify_as_sideeff = VtSideff [], VtLater let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater -- cgit v1.2.3 From 2e99ed199cde9495bd0f7e3c1209986bcaf77947 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 20 Jun 2017 15:18:40 +0200 Subject: STM: par: report no error to UIs in non-solve mode Used to report to the UI an Error feedback message whenever a worker was non making any progress. This is wrong since no-progress is fine (as long as one does not specify "solve") --- stm/stm.ml | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 8ca50e2d54..90f977ddbb 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1672,7 +1672,7 @@ end (* }}} *) and TacTask : sig - type output = Constr.constr * Evd.evar_universe_context + type output = (Constr.constr * Evd.evar_universe_context) option type task = { t_state : Stateid.t; t_state_fb : Stateid.t; @@ -1681,13 +1681,12 @@ and TacTask : sig t_goal : Goal.goal; t_kill : unit -> unit; t_name : string } - exception NoProgress include AsyncTaskQueue.Task with type task := task end = struct (* {{{ *) - type output = Constr.constr * Evd.evar_universe_context + type output = (Constr.constr * Evd.evar_universe_context) option let forward_feedback msg = Hooks.(call forward_feedback msg) @@ -1709,10 +1708,9 @@ end = struct (* {{{ *) r_name : string } type response = - | RespBuiltSubProof of output + | RespBuiltSubProof of (Constr.constr * Evd.evar_universe_context) | RespError of Pp.std_ppcmds | RespNoProgress - exception NoProgress let name = ref "tacworker" let extra_env () = [||] @@ -1734,10 +1732,9 @@ end = struct (* {{{ *) let use_response _ { t_assign; t_state; t_state_fb; t_kill } resp = match resp with - | RespBuiltSubProof o -> t_assign (`Val o); `Stay ((),[]) + | RespBuiltSubProof o -> t_assign (`Val (Some o)); `Stay ((),[]) | RespNoProgress -> - let e = (NoProgress, Exninfo.null) in - t_assign (`Exn e); + t_assign (`Val None); t_kill (); `Stay ((),[]) | RespError msg -> @@ -1848,8 +1845,8 @@ end = struct (* {{{ *) else tclUNIT () else let open Notations in - try - let pt, uc = Future.join f in + match Future.join f with + | Some (pt, uc) -> stm_pperr_endline (fun () -> hov 0 ( str"g=" ++ int (Evar.repr gid) ++ spc () ++ str"t=" ++ (Printer.pr_constr pt) ++ spc () ++ @@ -1857,7 +1854,7 @@ end = struct (* {{{ *) (if abstract then Tactics.tclABSTRACT None else (fun x -> x)) (V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*> Tactics.exact_no_check (EConstr.of_constr pt)) - with TacTask.NoProgress -> + | None -> if solve then Tacticals.New.tclSOLVE [] else tclUNIT () end) in -- cgit v1.2.3 From 64f0a3f014e423e4f7aa4fc1dc47cb70bc0e81fa Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 20 Jun 2017 21:55:16 +0200 Subject: [stm] Fix route setting on VtQuery This is a fix for a mistake in d8874dd855d748aaaf504890487ab15ffd7a677d , where we forgot to propagate the route parameter. --- stm/stm.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 071d2edf98..a7ed84350b 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2523,11 +2523,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) | VtQuery (false, route), VtNow -> begin let query_sid = VCS.cur_tip () in - try stm_vernac_interp (VCS.cur_tip ()) x + try stm_vernac_interp ~route (VCS.cur_tip ()) x with e -> let e = CErrors.push e in Exninfo.iraise (State.exn_on ~valid:Stateid.dummy query_sid e) end; `Ok + (* Part of the script commands don't set the query route *) | VtQuery (true, _route), w -> let id = VCS.new_node ~id:newtip () in let queue = -- cgit v1.2.3 From 94e0cbc26718fe3fecc58f6f8673f5f8abb0ce31 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 21 Jun 2017 15:12:21 +0200 Subject: [vernac] Remove stale bool parameter from `VernacStartTheoremProof` `VernacStartTheoremProof` contained a stale bool parameter from 15 years ago, which is unused today. --- stm/stm.ml | 2 +- stm/vernac_classifier.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 071d2edf98..81bac6a1f0 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -476,7 +476,7 @@ end = struct (* {{{ *) let mk_branch_name { expr = x } = Branch.make (let rec aux x = match x with | VernacDefinition (_,((_,i),_),_) -> Names.string_of_id i - | VernacStartTheoremProof (_,[Some ((_,i),_),_],_) -> Names.string_of_id i + | VernacStartTheoremProof (_,[Some ((_,i),_),_]) -> Names.string_of_id i | VernacTime (_, e) | VernacTimeout (_, e) -> aux e | _ -> "branch" in aux x) diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 1234e15afc..50e68852f8 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -115,7 +115,7 @@ let rec classify_vernac e = VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity,[i]), VtLater | VernacDefinition (_,((_,i),_),ProveBody _) -> VtStartProof(default_proof_mode (),GuaranteesOpacity,[i]), VtLater - | VernacStartTheoremProof (_,l,_) -> + | VernacStartTheoremProof (_,l) -> let ids = CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater -- cgit v1.2.3