From ab915f905ca81018521db63cdd0f3126b35c69c6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 15 Oct 2017 19:21:00 +0200 Subject: [stm] First step to move interpretation of Undo commands out of the classifier. The vernacular classifier has a current special case for "Undo" like commands, as it needs access to the document structure in order to produce the proper "VtBack" classification, however the classifier is defined before the document is. We introduce a new delegation status `VtMeta` that allows us to interpreted such commands outside the classifier itself. --- stm/stm.ml | 7 +++++-- stm/vernac_classifier.ml | 8 +++----- stm/vernac_classifier.mli | 3 --- 3 files changed, 8 insertions(+), 10 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index d1693519dc..0cbf72c8e6 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2414,7 +2414,6 @@ let new_doc { doc_type ; require_libs } = State.restore_root_state (); let doc = VCS.init doc_type Stateid.initial in - set_undo_classifier Backtrack.undo_vernac_classifier; begin match doc_type with | Interactive ln -> @@ -2578,7 +2577,7 @@ let snapshot_vio ~doc ldir long_f_dot_vo = let reset_task_queue = Slaves.reset_task_queue (* Document building *) -let process_transaction ?(newtip=Stateid.fresh ()) +let rec process_transaction ?(newtip=Stateid.fresh ()) ({ verbose; loc; expr } as x) c = stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x); let vcs = VCS.backup () in @@ -2589,6 +2588,10 @@ let process_transaction ?(newtip=Stateid.fresh ()) stm_prerr_endline (fun () -> " classified as: " ^ string_of_vernac_classification c); match c with + (* Meta *) + | VtMeta, _ -> + let clas = Backtrack.undo_vernac_classifier expr in + process_transaction ~newtip x clas (* Back *) | VtBack (true, oid), w -> let id = VCS.new_node ~id:newtip () in diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 158ad90846..e5d197eb17 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -32,6 +32,7 @@ let string_of_vernac_type = function | VtProofMode s -> "ProofMode " ^ s | VtQuery (b, route) -> "Query " ^ string_of_in_script b ^ " route " ^ string_of_int route | VtBack (b, _) -> "Stm Back " ^ string_of_in_script b + | VtMeta -> "Meta " let string_of_vernac_when = function | VtLater -> "Later" @@ -53,9 +54,6 @@ let make_polymorphic (a, b as x) = VtStartProof (x, Doesn'tGuaranteeOpacity, ids), b | _ -> x -let undo_classifier = ref (fun _ -> assert false) -let set_undo_classifier f = undo_classifier := f - let rec classify_vernac e = let static_classifier e = match e with (* Univ poly compatibility: we run it now, so that we can just @@ -75,7 +73,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 + | VtBack _ | VtProofMode _ | VtMeta), _ as x -> x | VtQed _, _ -> VtProofStep { parallel = `No; proof_block_detection = None }, VtNow @@ -191,7 +189,7 @@ let rec classify_vernac e = | VernacBack _ | VernacAbortAll | VernacUndoTo _ | VernacUndo _ | VernacResetName _ | VernacResetInitial - | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> !undo_classifier e + | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> VtMeta, VtNow (* What are these? *) | VernacToplevelControl _ | VernacRestoreState _ diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli index 2fa1e0b8dc..fe42a03a3d 100644 --- a/stm/vernac_classifier.mli +++ b/stm/vernac_classifier.mli @@ -18,9 +18,6 @@ val classify_vernac : vernac_expr -> vernac_classification val declare_vernac_classifier : Vernacexpr.extend_name -> (raw_generic_argument list -> unit -> vernac_classification) -> unit -(** Set by Stm *) -val set_undo_classifier : (vernac_expr -> vernac_classification) -> unit - (** Standard constant classifiers *) val classify_as_query : vernac_classification val classify_as_sideeff : vernac_classification -- cgit v1.2.3 From d9704f80a4f4b565f77368dbf7c9650d301a233d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 16 Oct 2017 12:54:57 +0200 Subject: [stm] Remove VtBack from public classification. We interpret meta-commands directly, instead of going by an intermediate "classifier step". The code could still use some further refactoring, in particular, the `part_of_script` bit is a bit strange likely coming from some special treatment of `VtMeta` in the `query` call, and should go away. --- stm/stm.ml | 91 +++++++++++++++++++++++++----------------------- stm/vernac_classifier.ml | 3 +- 2 files changed, 48 insertions(+), 46 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 0cbf72c8e6..b974d319e5 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1036,8 +1036,8 @@ module Backtrack : sig (* we could navigate the dag, but this ways easy *) val branches_of : Stateid.t -> backup - (* To be installed during initialization *) - val undo_vernac_classifier : vernac_expr -> vernac_classification + (* Returns the state that the command should backtract to *) + val undo_vernac_classifier : vernac_expr -> Stateid.t * vernac_when end = struct (* {{{ *) @@ -1105,7 +1105,7 @@ end = struct (* {{{ *) try match v with | VernacResetInitial -> - VtBack (true, Stateid.initial), VtNow + Stateid.initial, VtNow | VernacResetName (_,name) -> let id = VCS.get_branch_pos (VCS.current_branch ()) in (try @@ -1113,20 +1113,20 @@ end = struct (* {{{ *) fold_until (fun b (id,_,label,_,_) -> if b then `Stop id else `Cont (List.mem name label)) false id in - VtBack (true, oid), VtNow + oid, VtNow with Not_found -> - VtBack (true, id), VtNow) + id, 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 (true, oid), VtNow + oid, 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 (true, oid), VtLater + oid, VtLater | VernacUndoTo _ | VernacRestart as e -> let m = match e with VernacUndoTo m -> m | _ -> 0 in @@ -1143,17 +1143,17 @@ 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 (true, oid), VtLater + oid, 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 (true, oid), VtLater + oid, VtLater | VernacBacktrack (id,_,_) | VernacBackTo id -> - VtBack (VCS.is_interactive () = `Yes, Stateid.of_int id), VtNow - | _ -> VtUnknown, VtNow + Stateid.of_int id, VtNow + | _ -> anomaly Pp.(str "incorrect VtMeta classification") with | Not_found -> CErrors.user_err ~hdr:"undo_vernac_classifier" @@ -2577,7 +2577,38 @@ let snapshot_vio ~doc ldir long_f_dot_vo = let reset_task_queue = Slaves.reset_task_queue (* Document building *) -let rec process_transaction ?(newtip=Stateid.fresh ()) +let process_back_meta_command ~part_of_script ~newtip ~head oid aast w = + match part_of_script, w with + | 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 + List.iter (fun branch -> + if not (List.mem_assoc branch (mine::others)) then + ignore(merge_proof_branch ~valid aast VtDrop branch)) + (VCS.branches ()); + VCS.checkout_shallowest_proof_branch (); + let head = VCS.current_branch () in + List.iter (fun b -> + if not(VCS.Branch.equal b head) then begin + VCS.checkout b; + VCS.commit (VCS.new_node ()) (Alias (oid,aast)); + end) + (VCS.branches ()); + VCS.checkout_shallowest_proof_branch (); + VCS.commit id (Alias (oid,aast)); + Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok + + | false, VtNow -> + stm_prerr_endline (fun () -> "undo to state " ^ Stateid.to_string oid); + Backtrack.backto oid; + VCS.checkout_shallowest_proof_branch (); + Reach.known_state ~cache:(VCS.is_interactive ()) oid; `Ok + + | false, VtLater -> + anomaly(str"undo classifier: VtMeta + VtLater must imply part_of_script.") + +let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) ({ verbose; loc; expr } as x) c = stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x); let vcs = VCS.backup () in @@ -2590,36 +2621,8 @@ let rec process_transaction ?(newtip=Stateid.fresh ()) match c with (* Meta *) | VtMeta, _ -> - let clas = Backtrack.undo_vernac_classifier expr in - process_transaction ~newtip x clas - (* Back *) - | VtBack (true, oid), 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 - List.iter (fun branch -> - if not (List.mem_assoc branch (mine::others)) then - ignore(merge_proof_branch ~valid x VtDrop branch)) - (VCS.branches ()); - VCS.checkout_shallowest_proof_branch (); - let head = VCS.current_branch () in - List.iter (fun b -> - if not(VCS.Branch.equal b head) then begin - VCS.checkout b; - VCS.commit (VCS.new_node ()) (Alias (oid,x)); - end) - (VCS.branches ()); - VCS.checkout_shallowest_proof_branch (); - VCS.commit id (Alias (oid,x)); - Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok - | VtBack (false, id), VtNow -> - stm_prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id); - Backtrack.backto id; - VCS.checkout_shallowest_proof_branch (); - Reach.known_state ~cache:(VCS.is_interactive ()) id; `Ok - | VtBack (false, id), VtLater -> - anomaly(str"classifier: VtBack + VtLater must imply part_of_script.") - + let id, w = Backtrack.undo_vernac_classifier expr in + process_back_meta_command ~part_of_script ~newtip ~head id x w (* Query *) | VtQuery (false, route), VtNow -> begin @@ -2881,8 +2884,8 @@ let query ~doc ~at ~route s = let clas = classify_vernac ast in let aast = { verbose = true; indentation; strlen; loc; expr = ast } in match clas with - | VtBack (_,id), _ -> (* TODO: can this still happen ? *) - ignore(process_transaction aast (VtBack (false,id), VtNow)) + | VtMeta , _ -> (* TODO: can this still happen ? *) + ignore(process_transaction ~part_of_script:false aast (VtMeta,VtNow)) | _ -> ignore(process_transaction aast (VtQuery (false, route), VtNow))) s diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index e5d197eb17..3aa2cd707e 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -31,7 +31,6 @@ let string_of_vernac_type = function Option.default "" proof_block_detection | VtProofMode s -> "ProofMode " ^ s | VtQuery (b, route) -> "Query " ^ string_of_in_script b ^ " route " ^ string_of_int route - | VtBack (b, _) -> "Stm Back " ^ string_of_in_script b | VtMeta -> "Meta " let string_of_vernac_when = function @@ -73,7 +72,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 _ | VtMeta), _ as x -> x + | VtProofMode _ | VtMeta), _ as x -> x | VtQed _, _ -> VtProofStep { parallel = `No; proof_block_detection = None }, VtNow -- cgit v1.2.3 From 19bbc3fd946555aa1fa1fc23d805a4eb3d13bc45 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 27 May 2017 23:22:04 +0200 Subject: [stm] Move interpretation state to Vernacentries We still don't thread the state there, but this is a start of the needed infrastructure. --- stm/proofBlockDelimiter.ml | 2 +- stm/stm.ml | 174 +++++++++++++++++++++++++-------------------- stm/stm.mli | 8 +-- 3 files changed, 99 insertions(+), 85 deletions(-) (limited to 'stm') diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index b46556ea67..01b75e4964 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -46,7 +46,7 @@ let simple_goal sigma g gs = let is_focused_goal_simple ~doc id = match state_of_id ~doc id with | `Expired | `Error _ | `Valid None -> `Not - | `Valid (Some { proof }) -> + | `Valid (Some { Vernacentries.proof }) -> let proof = Proof_global.proof_of_state proof in let focused, r1, r2, r3, sigma = Proof.proof proof in let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in diff --git a/stm/stm.ml b/stm/stm.ml index b974d319e5..231ec05473 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -22,7 +22,8 @@ open Pp open CErrors open Feedback open Vernacexpr -open Vernac_classifier + +let _ds = Vernacentries._dummy_interp_state let execution_error ?loc state_id msg = feedback ~id:state_id @@ -138,10 +139,12 @@ type step = | `Qed of qed_t * Stateid.t | `Sideff of seff_t * Stateid.t | `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 } @@ -152,14 +155,11 @@ let summary_pstate = [ Evarutil.meta_counter_summary_name; type cached_state = | Empty | Error of Exninfo.iexn - | Valid of state -and state = { (* TODO: inline records in OCaml 4.03 *) - system : States.state; (* summary + libstack *) - proof : Proof_global.state; (* proof state *) - shallow : bool (* is the state trimmed down (libstack) *) -} + | Valid of Vernacentries.interp_state + type branch = Vcs_.Branch.t * branch_type Vcs_.branch_info type backup = { mine : branch; others : branch list } + type 'vcs state_info = { (* TODO: Make this record private to VCS *) mutable n_reached : int; (* debug cache: how many times was computed *) mutable n_goals : int; (* open goals: indentation *) @@ -715,6 +715,7 @@ module State : sig ?safe_id:Stateid.t -> ?redefine:bool -> ?cache:Summary.marshallable -> ?feedback_processed:bool -> (unit -> unit) -> Stateid.t -> unit + val fix_exn_ref : (Exninfo.iexn -> Exninfo.iexn) ref val install_cached : Stateid.t -> unit @@ -722,16 +723,18 @@ module State : sig val is_cached_and_valid : ?cache:Summary.marshallable -> Stateid.t -> bool val exn_on : Stateid.t -> valid:Stateid.t -> Exninfo.iexn -> Exninfo.iexn + (* to send states across worker/master *) - type frozen_state - val get_cached : Stateid.t -> frozen_state - val same_env : frozen_state -> frozen_state -> bool + val get_cached : Stateid.t -> Vernacentries.interp_state + val same_env : Vernacentries.interp_state -> Vernacentries.interp_state -> bool type proof_part + type partial_state = - [ `Full of frozen_state - | `Proof of Stateid.t * proof_part ] - val proof_part_of_frozen : frozen_state -> proof_part + [ `Full of Vernacentries.interp_state + | `ProofOnly of Stateid.t * proof_part ] + + val proof_part_of_frozen : Vernacentries.interp_state -> proof_part val assign : Stateid.t -> partial_state -> unit (* Handlers for initial state, prior to document creation. *) @@ -742,39 +745,36 @@ module State : sig be removed in the state handling refactoring. *) val cur_id : Stateid.t ref - end = struct (* {{{ *) + open Vernacentries + (* cur_id holds Stateid.dummy in case the last attempt to define a state * failed, so the global state may contain garbage *) let cur_id = ref Stateid.dummy let fix_exn_ref = ref (fun x -> x) - (* helpers *) - let freeze_global_state marshallable = - { system = States.freeze ~marshallable; - proof = Proof_global.freeze ~marshallable; - shallow = (marshallable = `Shallow) } - let unfreeze_global_state { system; proof } = - States.unfreeze system; Proof_global.unfreeze proof - (* hack to make futures functional *) + (* this will be removed when we don't call it anymore as we fully + handle state functionally *) let () = Future.set_freeze - (fun () -> Obj.magic (freeze_global_state `No, !cur_id)) - (fun t -> let s,i = Obj.magic t in unfreeze_global_state s; cur_id := i) - - type frozen_state = state + (fun () -> Obj.magic (freeze_interp_state `No, !cur_id)) + (fun t -> let s,i = Obj.magic t in unfreeze_interp_state s; cur_id := i) + type proof_part = Proof_global.state * Summary.frozen_bits (* only meta counters *) + type partial_state = - [ `Full of frozen_state - | `Proof of Stateid.t * proof_part ] - let proof_part_of_frozen { proof; system } = + [ `Full of Vernacentries.interp_state + | `ProofOnly of Stateid.t * proof_part ] + + let proof_part_of_frozen { Vernacentries.proof; system } = proof, Summary.project_summary (States.summary_of_state system) summary_pstate let freeze marshallable id = - VCS.set_state id (Valid (freeze_global_state marshallable)) + VCS.set_state id (Valid (Vernacentries.freeze_interp_state marshallable)) + let freeze_invalid id iexn = VCS.set_state id (Error iexn) let is_cached ?(cache=`No) id only_valid = @@ -798,7 +798,7 @@ end = struct (* {{{ *) match VCS.get_info id with | { state = Valid s } -> if Stateid.equal id !cur_id then () (* optimization *) - else begin unfreeze_global_state s; cur_id := id end + else begin Vernacentries.unfreeze_interp_state s; cur_id := id end | { state = Error ie } -> cur_id := id; Exninfo.iraise ie | _ -> (* coqc has a 1 slot cache and only for valid states *) @@ -819,13 +819,13 @@ end = struct (* {{{ *) try let prev = (VCS.visit id).next in if is_cached_and_valid prev - then { s with proof = + then { s with Vernacentries.proof = Proof_global.copy_terminators ~src:(get_cached prev).proof ~tgt:s.proof } else s with VCS.Expired -> s in VCS.set_state id (Valid s) - | `Proof(ontop,(pstate,counters)) -> + | `ProofOnly(ontop,(pstate,counters)) -> if is_cached_and_valid ontop then let s = get_cached ontop in let s = { s with proof = @@ -895,11 +895,11 @@ end = struct (* {{{ *) let init_state = ref None let register_root_state () = - init_state := Some (freeze_global_state `No) + init_state := Some (Vernacentries.freeze_interp_state `No) let restore_root_state () = cur_id := Stateid.dummy; - unfreeze_global_state Option.(get !init_state) + Vernacentries.unfreeze_interp_state (Option.get !init_state); end (* }}} *) @@ -994,7 +994,7 @@ end (* Wrapper for Vernacentries.interp to set the feedback id *) (* It is currently called 19 times, this number should be certainly reduced... *) -let stm_vernac_interp ?proof id ?route { verbose; loc; expr } = +let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacentries.interp_state = (* The Stm will gain the capability to interpret commmads affecting the whole document state, such as backtrack, etc... so we start to design the stm command interpreter now *) @@ -1011,18 +1011,18 @@ let stm_vernac_interp ?proof id ?route { verbose; loc; expr } = | VernacTime (_,e) | VernacTimeout (_,e) | VernacRedirect (_,(_,e)) -> is_filtered_command e | _ -> false in - let aux_interp cmd = + let aux_interp st cmd = if is_filtered_command cmd then - stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr) + (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st) else match cmd with - | VernacShow ShowScript -> ShowScript.show_script () + | VernacShow ShowScript -> ShowScript.show_script (); st | expr -> stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr); - try Vernacentries.interp ?verbosely:(Some verbose) ?proof (Loc.tag ?loc expr) + try Vernacentries.interp ?verbosely:(Some verbose) ?proof st (Loc.tag ?loc expr) with e -> let e = CErrors.push e in Exninfo.iraise Hooks.(call_process_error_once e) - in aux_interp expr + in aux_interp st expr (****************************** CRUFT *****************************************) (******************************************************************************) @@ -1436,7 +1436,7 @@ end = struct (* {{{ *) let terminator = (* The one sent by master is an InvalidKey *) Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in stm_vernac_interp stop - ~proof:(pobject, terminator) + ~proof:(pobject, terminator) _ds { verbose = false; loc; indentation = 0; strlen = 0; expr = (VernacEndProof (Proved (Opaque,None))) }) in ignore(Future.join checked_proof); @@ -1457,7 +1457,7 @@ end = struct (* {{{ *) let perform_states query = if query = [] then [] else - let is_tac e = match classify_vernac e with + let is_tac e = match Vernac_classifier.classify_vernac e with | VtProofStep _, _ -> true | _ -> false in @@ -1480,7 +1480,7 @@ end = struct (* {{{ *) | _, None -> None | Some (prev, o, `Cmd { cast = { expr }}), Some n when is_tac expr && State.same_env o n -> (* A pure tactic *) - Some (id, `Proof (prev, State.proof_part_of_frozen n)) + Some (id, `ProofOnly (prev, State.proof_part_of_frozen n)) | Some _, Some s -> msg_debug (Pp.str "STM: sending back a fat state"); Some (id, `Full s) @@ -1575,9 +1575,14 @@ end = struct (* {{{ *) (* We jump at the beginning since the kernel handles side effects by also * looking at the ones that happen to be present in the current env *) Reach.known_state ~cache:`No start; - stm_vernac_interp stop ~proof + (* STATE SPEC: + * - start: First non-expired state! [This looks very fishy] + * - end : start + qed + * => takes nothing from the itermediate states. + *) + ignore(stm_vernac_interp stop ~proof _ds { verbose = false; loc; indentation = 0; strlen = 0; - expr = (VernacEndProof (Proved (Opaque,None))) }; + expr = (VernacEndProof (Proved (Opaque,None))) }); `OK proof end with e -> @@ -1826,7 +1831,14 @@ end = struct (* {{{ *) else begin let (i, ast) = r_ast in Proof_global.simple_with_current_proof (fun _ p -> Proof.focus focus_cond () i p); - stm_vernac_interp r_state_fb ast; + (* STATE SPEC: + * - start : id + * - return: id + * => captures state id in a future closure, which will + discard execution state but for the proof + univs. + *) + + ignore(stm_vernac_interp r_state_fb _ds ast); let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in match Evd.(evar_body (find sigma r_goal)) with | Evd.Evar_empty -> RespNoProgress @@ -1958,7 +1970,11 @@ end = struct (* {{{ *) VCS.print (); Reach.known_state ~cache:`No r_where; try - stm_vernac_interp r_for { r_what with verbose = true }; + (* STATE SPEC: + * - start: r_where + * - end : after execution of r_what + *) + ignore(stm_vernac_interp r_for _ds { r_what with verbose = true }); feedback ~id:r_for Processed with e when CErrors.noncritical e -> let e = CErrors.push e in @@ -2166,14 +2182,18 @@ let known_state ?(redefine_qed=false) ~cache id = Proofview.give_up else Proofview.tclUNIT () end in match (VCS.get_info base_state).state with - | Valid { proof } -> + | Valid { Vernacentries.proof } -> Proof_global.unfreeze proof; Proof_global.with_current_proof (fun _ p -> feedback ~id:id Feedback.AddedAxiom; fst (Pfedit.solve Vernacexpr.SelectAll None tac p), ()); - Option.iter (fun expr -> stm_vernac_interp id { + (* STATE SPEC: + * - start: Modifies the input state adding a proof. + * - end : maybe after recovery command. + *) + Option.iter (fun expr -> ignore(stm_vernac_interp id _ds { verbose = true; loc = None; expr; indentation = 0; - strlen = 0 }) + strlen = 0 } )) recovery_command | _ -> assert false end @@ -2247,7 +2267,8 @@ let known_state ?(redefine_qed=false) ~cache id = | `Cmd { cast = x; ceff = eff; ctac = true; cblock } -> (fun () -> resilient_tactic id cblock (fun () -> reach view.next; - stm_vernac_interp id x); + ignore(stm_vernac_interp id _ds x) + ); if eff then update_global_env () ), (if eff then `Yes else cache), true | `Cmd { cast = x; ceff = eff } -> (fun () -> @@ -2255,18 +2276,18 @@ let known_state ?(redefine_qed=false) ~cache id = | Flags.APon | Flags.APonLazy -> resilient_command reach view.next | Flags.APoff -> reach view.next); - stm_vernac_interp id x; + ignore(stm_vernac_interp id _ds x); if eff then update_global_env () ), (if eff then `Yes else cache), true | `Fork ((x,_,_,_), None) -> (fun () -> resilient_command reach view.next; - stm_vernac_interp id x; + ignore(stm_vernac_interp id _ds x); wall_clock_last_fork := Unix.gettimeofday () ), `Yes, true | `Fork ((x,_,_,_), Some prev) -> (fun () -> (* nested proof *) reach ~cache:`Shallow prev; reach view.next; - (try stm_vernac_interp id x; + (try ignore(stm_vernac_interp id _ds x); with e when CErrors.noncritical e -> let (e, info) = CErrors.push e in let info = Stateid.add info ~valid:prev id in @@ -2316,14 +2337,14 @@ let known_state ?(redefine_qed=false) ~cache id = Proof_global.close_future_proof ~feedback_id:id fp in if not delegate then ignore(Future.compute fp); reach view.next; - stm_vernac_interp id ~proof x; + ignore(stm_vernac_interp id ~proof _ds x); feedback ~id:id Incomplete | { VCS.kind = `Master }, _ -> assert false end; Proof_global.discard_all () ), (if redefine_qed then `No else `Yes), true | `Sync (name, `Immediate) -> (fun () -> - reach eop; stm_vernac_interp id x; Proof_global.discard_all () + reach eop; ignore(stm_vernac_interp id _ds x); Proof_global.discard_all () ), `Yes, true | `Sync (name, reason) -> (fun () -> log_processing_sync id name reason; @@ -2344,7 +2365,7 @@ let known_state ?(redefine_qed=false) ~cache id = if keep != VtKeepAsAxiom then reach view.next; let wall_clock2 = Unix.gettimeofday () in - stm_vernac_interp id ?proof x; + ignore(stm_vernac_interp id ?proof _ds x); let wall_clock3 = Unix.gettimeofday () in Aux_file.record_in_aux_at ?loc:x.loc "proof_check_time" (Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2)); @@ -2360,7 +2381,7 @@ let known_state ?(redefine_qed=false) ~cache id = in aux (collect_proof keep (view.next, x) brname brinfo eop) | `Sideff (ReplayCommand x,_) -> (fun () -> - reach view.next; stm_vernac_interp id x; update_global_env () + reach view.next; ignore(stm_vernac_interp id _ds x); update_global_env () ), cache, true | `Sideff (CherryPickEnv, origin) -> (fun () -> reach view.next; @@ -2544,7 +2565,7 @@ let merge_proof_branch ~valid ?id qast keep brname = VCS.rewrite_merge qed_id ~ours:(Qed (qed ofp)) ~at:master_id brname; VCS.delete_branch brname; VCS.gc (); - Reach.known_state ~redefine_qed:true ~cache:`No qed_id; + let _st = Reach.known_state ~redefine_qed:true ~cache:`No qed_id in VCS.checkout VCS.Branch.master; `Unfocus qed_id | { VCS.kind = `Master } -> @@ -2617,23 +2638,21 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) VCS.checkout head; let rc = begin stm_prerr_endline (fun () -> - " classified as: " ^ string_of_vernac_classification c); + " classified as: " ^ Vernac_classifier.string_of_vernac_classification c); match c with (* Meta *) | VtMeta, _ -> let id, w = Backtrack.undo_vernac_classifier expr in process_back_meta_command ~part_of_script ~newtip ~head id x w (* Query *) - | VtQuery (false, route), VtNow -> - begin - let query_sid = VCS.cur_tip () in - 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 -> + | VtQuery (false,route), VtNow -> + let query_sid = VCS.cur_tip () in + (try ignore(stm_vernac_interp ~route query_sid _ds x) + with e -> + let e = CErrors.push e in + Exninfo.iraise (State.exn_on ~valid:Stateid.dummy query_sid e)); + `Ok + | VtQuery (true, route), w -> let id = VCS.new_node ~id:newtip () in let queue = if !Flags.async_proofs_full then `QueryQueue (ref false) @@ -2702,7 +2721,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) (* Side effect on all branches *) | VtUnknown, _ when expr = VernacToplevelControl Drop -> - stm_vernac_interp (VCS.get_branch_pos head) x; `Ok + ignore(stm_vernac_interp (VCS.get_branch_pos head) _ds x); `Ok | VtSideff l, w -> let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in @@ -2723,12 +2742,13 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in let id = VCS.new_node ~id:newtip () in let head_id = VCS.get_branch_pos head in - Reach.known_state ~cache:`Yes head_id; (* ensure it is ok *) + let _st = Reach.known_state ~cache:`Yes head_id in (* ensure it is ok *) let step () = VCS.checkout VCS.Branch.master; let mid = VCS.get_branch_pos VCS.Branch.master in - Reach.known_state ~cache:(VCS.is_interactive ()) mid; - stm_vernac_interp id x; + let _st' = Reach.known_state ~cache:(VCS.is_interactive ()) mid in + ignore(stm_vernac_interp id _ds x); + (* Vernac x may or may not start a proof *) if not in_proof && Proof_global.there_are_pending_proofs () then begin @@ -2860,7 +2880,7 @@ let add ~doc ~ontop ?newtip verb (loc, ast) = let indentation, strlen = compute_indentation ?loc ontop in CWarnings.set_current_loc loc; (* XXX: Classifiy vernac should be moved inside process transaction *) - let clas = classify_vernac ast in + let clas = Vernac_classifier.classify_vernac ast in let aast = { verbose = verb; indentation; strlen; loc; expr = ast } in match process_transaction ?newtip aast clas with | `Ok -> doc, VCS.cur_tip (), `NewTip @@ -2881,7 +2901,7 @@ let query ~doc ~at ~route s = let loc, ast = parse_sentence ~doc at s in let indentation, strlen = compute_indentation ?loc at in CWarnings.set_current_loc loc; - let clas = classify_vernac ast in + let clas = Vernac_classifier.classify_vernac ast in let aast = { verbose = true; indentation; strlen; loc; expr = ast } in match clas with | VtMeta , _ -> (* TODO: can this still happen ? *) diff --git a/stm/stm.mli b/stm/stm.mli index c65cf6a9af..31f4599d36 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -217,16 +217,10 @@ val state_ready_hook : (Stateid.t -> unit) Hook.t (* Messages from the workers to the master *) val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t -type state = { - system : States.state; - proof : Proof_global.state; - shallow : bool -} - val get_doc : Feedback.doc_id -> doc val state_of_id : doc:doc -> - Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ] + Stateid.t -> [ `Valid of Vernacentries.interp_state option | `Expired | `Error of exn ] (* Queries for backward compatibility *) val current_proof_depth : doc:doc -> int -- cgit v1.2.3 From 280be11cb4706e039cf4e9f68a5ae38b0aef9340 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 28 May 2017 00:35:57 +0200 Subject: [stm] Remove state-handling from Futures. We make Vernacentries.interp functional wrt state, and thus remove state-handling from `Future`. Now, a future needs a closure if it wants to preserve state. Consequently, `Vernacentries.interp` takes a state, and returns the new one. We don't explicitly thread the state in the STM yet, instead, we recover the state that was used before and pass it explicitly to `interp`. I have tested the commit with the files in interactive, but we aware that some new bugs may appear or old ones be made more apparent. However, I am confident that this step will improve our understanding of bugs. In some cases, we perform a bit more summary wrapping/unwrapping. This will go away in future commits; informal timings for a full make: - master: real 2m11,027s user 8m30,904s sys 1m0,000s - no_futures: real 2m8,474s user 8m34,380s sys 0m59,156s --- stm/stm.ml | 135 ++++++++++++++++++++++++++++++++++++++++--------------------- 1 file changed, 89 insertions(+), 46 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 231ec05473..84a4c5cc52 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -23,7 +23,17 @@ open CErrors open Feedback open Vernacexpr -let _ds = Vernacentries._dummy_interp_state +(* Protect against state changes *) +let stm_purify f x = + let st = Vernacentries.freeze_interp_state `No in + try + let res = f x in + Vernacentries.unfreeze_interp_state st; + res + with e -> + let e = CErrors.push e in + Vernacentries.unfreeze_interp_state st; + Exninfo.iraise e let execution_error ?loc state_id msg = feedback ~id:state_id @@ -754,13 +764,6 @@ end = struct (* {{{ *) let cur_id = ref Stateid.dummy let fix_exn_ref = ref (fun x -> x) - (* hack to make futures functional *) - (* this will be removed when we don't call it anymore as we fully - handle state functionally *) - let () = Future.set_freeze - (fun () -> Obj.magic (freeze_interp_state `No, !cur_id)) - (fun t -> let s,i = Obj.magic t in unfreeze_interp_state s; cur_id := i) - type proof_part = Proof_global.state * Summary.frozen_bits (* only meta counters *) @@ -797,9 +800,13 @@ end = struct (* {{{ *) let install_cached id = match VCS.get_info id with | { state = Valid s } -> - if Stateid.equal id !cur_id then () (* optimization *) - else begin Vernacentries.unfreeze_interp_state s; cur_id := id end - | { state = Error ie } -> cur_id := id; Exninfo.iraise ie + Vernacentries.unfreeze_interp_state s; + cur_id := id + + | { state = Error ie } -> + cur_id := id; + Exninfo.iraise ie + | _ -> (* coqc has a 1 slot cache and only for valid states *) if VCS.is_interactive () = `No && Stateid.equal id !cur_id then () @@ -1429,18 +1436,28 @@ end = struct (* {{{ *) * the few errors tactics don't catch, like the "fix" tactic building * a bad fixpoint *) let fix_exn = Future.fix_exn_of future_proof in + (* STATE: We use the current installed imperative state *) + let st = Vernacentries.freeze_interp_state `No in if not drop then begin - let checked_proof = Future.chain ~pure:false future_proof (fun p -> + let checked_proof = Future.chain future_proof (fun p -> + + (* Unfortunately close_future_proof and friends are not pure so we need + to set the state manually here *) + Vernacentries.unfreeze_interp_state st; let pobject, _ = Proof_global.close_future_proof ~feedback_id:stop (Future.from_val ~fix_exn p) in let terminator = (* The one sent by master is an InvalidKey *) Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in + + let st = Vernacentries.freeze_interp_state `No in stm_vernac_interp stop - ~proof:(pobject, terminator) _ds + ~proof:(pobject, terminator) st { verbose = false; loc; indentation = 0; strlen = 0; expr = (VernacEndProof (Proved (Opaque,None))) }) in ignore(Future.join checked_proof); end; + (* STATE: Restore the state XXX: handle exn *) + Vernacentries.unfreeze_interp_state st; RespBuiltProof(proof,time) with | e when CErrors.noncritical e || e = Stack_overflow -> @@ -1580,7 +1597,9 @@ end = struct (* {{{ *) * - end : start + qed * => takes nothing from the itermediate states. *) - ignore(stm_vernac_interp stop ~proof _ds + (* STATE We use the state resulting from reaching start. *) + let st = Vernacentries.freeze_interp_state `No in + ignore(stm_vernac_interp stop ~proof st { verbose = false; loc; indentation = 0; strlen = 0; expr = (VernacEndProof (Proved (Opaque,None))) }); `OK proof @@ -1638,10 +1657,9 @@ end = struct (* {{{ *) let pr = Future.from_val (map (Option.get (Global.body_of_constant_body c))) in let uc = - Future.chain - ~pure:true uc Univ.hcons_universe_context_set in - let pr = Future.chain ~pure:true pr discharge in - let pr = Future.chain ~pure:true pr Constr.hcons in + Future.chain uc Univ.hcons_universe_context_set in + let pr = Future.chain pr discharge in + let pr = Future.chain pr Constr.hcons in Future.sink pr; let extra = Future.join uc in u.(bucket) <- uc; @@ -1817,7 +1835,7 @@ end = struct (* {{{ *) Option.iter VCS.restore vcs; try Reach.known_state ~cache:`No id; - Future.purify (fun () -> + stm_purify (fun () -> let _,_,_,_,sigma0 = Proof.proof (Proof_global.give_me_the_proof ()) in let g = Evd.find sigma0 r_goal in let is_ground c = Evarutil.is_ground_term sigma0 (EConstr.of_constr c) in @@ -1837,8 +1855,8 @@ end = struct (* {{{ *) * => captures state id in a future closure, which will discard execution state but for the proof + univs. *) - - ignore(stm_vernac_interp r_state_fb _ds ast); + let st = Vernacentries.freeze_interp_state `No in + ignore(stm_vernac_interp r_state_fb st ast); let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in match Evd.(evar_body (find sigma r_goal)) with | Evd.Evar_empty -> RespNoProgress @@ -1877,7 +1895,8 @@ end = struct (* {{{ *) | VernacRedirect (_,(_,e)) -> find ~time ~fail e | VernacFail e -> find ~time ~fail:true e | e -> e, time, fail in find ~time:false ~fail:false e in - Vernacentries.with_fail fail (fun () -> + let st = Vernacentries.freeze_interp_state `No in + Vernacentries.with_fail st fail (fun () -> (if time then System.with_time !Flags.time else (fun x -> x)) (fun () -> ignore(TaskQueue.with_n_workers nworkers (fun queue -> Proof_global.with_current_proof (fun _ p -> @@ -1969,12 +1988,14 @@ end = struct (* {{{ *) VCS.restore r_doc; VCS.print (); Reach.known_state ~cache:`No r_where; + (* STATE *) + let st = Vernacentries.freeze_interp_state `No in try (* STATE SPEC: * - start: r_where * - end : after execution of r_what *) - ignore(stm_vernac_interp r_for _ds { r_what with verbose = true }); + ignore(stm_vernac_interp r_for st { r_what with verbose = true }); feedback ~id:r_for Processed with e when CErrors.noncritical e -> let e = CErrors.push e in @@ -2191,7 +2212,9 @@ let known_state ?(redefine_qed=false) ~cache id = * - start: Modifies the input state adding a proof. * - end : maybe after recovery command. *) - Option.iter (fun expr -> ignore(stm_vernac_interp id _ds { + (* STATE: We use an updated state with proof *) + let st = Vernacentries.freeze_interp_state `No in + Option.iter (fun expr -> ignore(stm_vernac_interp id st { verbose = true; loc = None; expr; indentation = 0; strlen = 0 } )) recovery_command @@ -2231,10 +2254,12 @@ let known_state ?(redefine_qed=false) ~cache id = let inject_non_pstate (s,l) = Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env () in - let rec pure_cherry_pick_non_pstate safe_id id = Future.purify (fun id -> - stm_prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id); - reach ~safe_id id; - cherry_pick_non_pstate ()) id + let rec pure_cherry_pick_non_pstate safe_id id = + stm_purify (fun id -> + stm_prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id); + reach ~safe_id id; + cherry_pick_non_pstate ()) + id (* traverses the dag backward from nodes being already calculated *) and reach ?safe_id ?(redefine_qed=false) ?(cache=cache) id = @@ -2267,7 +2292,9 @@ let known_state ?(redefine_qed=false) ~cache id = | `Cmd { cast = x; ceff = eff; ctac = true; cblock } -> (fun () -> resilient_tactic id cblock (fun () -> reach view.next; - ignore(stm_vernac_interp id _ds x) + (* State resulting from reach *) + let st = Vernacentries.freeze_interp_state `No in + ignore(stm_vernac_interp id st x) ); if eff then update_global_env () ), (if eff then `Yes else cache), true @@ -2276,18 +2303,23 @@ let known_state ?(redefine_qed=false) ~cache id = | Flags.APon | Flags.APonLazy -> resilient_command reach view.next | Flags.APoff -> reach view.next); - ignore(stm_vernac_interp id _ds x); + let st = Vernacentries.freeze_interp_state `No in + ignore(stm_vernac_interp id st x); if eff then update_global_env () ), (if eff then `Yes else cache), true | `Fork ((x,_,_,_), None) -> (fun () -> resilient_command reach view.next; - ignore(stm_vernac_interp id _ds x); + let st = Vernacentries.freeze_interp_state `No in + ignore(stm_vernac_interp id st x); wall_clock_last_fork := Unix.gettimeofday () ), `Yes, true | `Fork ((x,_,_,_), Some prev) -> (fun () -> (* nested proof *) reach ~cache:`Shallow prev; reach view.next; - (try ignore(stm_vernac_interp id _ds x); + + (try + let st = Vernacentries.freeze_interp_state `No in + ignore(stm_vernac_interp id st x); with e when CErrors.noncritical e -> let (e, info) = CErrors.push e in let info = Stateid.add info ~valid:prev id in @@ -2337,14 +2369,18 @@ let known_state ?(redefine_qed=false) ~cache id = Proof_global.close_future_proof ~feedback_id:id fp in if not delegate then ignore(Future.compute fp); reach view.next; - ignore(stm_vernac_interp id ~proof _ds x); + let st = Vernacentries.freeze_interp_state `No in + ignore(stm_vernac_interp id ~proof st x); feedback ~id:id Incomplete | { VCS.kind = `Master }, _ -> assert false end; Proof_global.discard_all () ), (if redefine_qed then `No else `Yes), true | `Sync (name, `Immediate) -> (fun () -> - reach eop; ignore(stm_vernac_interp id _ds x); Proof_global.discard_all () + reach eop; + let st = Vernacentries.freeze_interp_state `No in + ignore(stm_vernac_interp id st x); + Proof_global.discard_all () ), `Yes, true | `Sync (name, reason) -> (fun () -> log_processing_sync id name reason; @@ -2365,7 +2401,8 @@ let known_state ?(redefine_qed=false) ~cache id = if keep != VtKeepAsAxiom then reach view.next; let wall_clock2 = Unix.gettimeofday () in - ignore(stm_vernac_interp id ?proof _ds x); + let st = Vernacentries.freeze_interp_state `No in + ignore(stm_vernac_interp id ?proof st x); let wall_clock3 = Unix.gettimeofday () in Aux_file.record_in_aux_at ?loc:x.loc "proof_check_time" (Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2)); @@ -2381,7 +2418,10 @@ let known_state ?(redefine_qed=false) ~cache id = in aux (collect_proof keep (view.next, x) brname brinfo eop) | `Sideff (ReplayCommand x,_) -> (fun () -> - reach view.next; ignore(stm_vernac_interp id _ds x); update_global_env () + reach view.next; + let st = Vernacentries.freeze_interp_state `No in + ignore(stm_vernac_interp id st x); + update_global_env () ), cache, true | `Sideff (CherryPickEnv, origin) -> (fun () -> reach view.next; @@ -2525,7 +2565,7 @@ let check_task name (tasks,rcbackup) i = RemoteCounter.restore rcbackup; let vcs = VCS.backup () in try - let rc = Future.purify (Slaves.check_task name tasks) i in + let rc = stm_purify (Slaves.check_task name tasks) i in VCS.restore vcs; rc with e when CErrors.noncritical e -> VCS.restore vcs; false @@ -2535,7 +2575,7 @@ let finish_tasks name u d p (t,rcbackup as tasks) = RemoteCounter.restore rcbackup; let finish_task u (_,_,i) = let vcs = VCS.backup () in - let u = Future.purify (Slaves.finish_task name u d p t) i in + let u = stm_purify (Slaves.finish_task name u d p t) i in VCS.restore vcs; u in try @@ -2647,11 +2687,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) (* Query *) | VtQuery (false,route), VtNow -> let query_sid = VCS.cur_tip () in - (try ignore(stm_vernac_interp ~route query_sid _ds x) + (try + let st = Vernacentries.freeze_interp_state `No in + ignore(stm_vernac_interp ~route query_sid st x) with e -> - let e = CErrors.push e in - Exninfo.iraise (State.exn_on ~valid:Stateid.dummy query_sid e)); - `Ok + let e = CErrors.push e in + Exninfo.iraise (State.exn_on ~valid:Stateid.dummy query_sid e)); `Ok | VtQuery (true, route), w -> let id = VCS.new_node ~id:newtip () in let queue = @@ -2721,7 +2762,9 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) (* Side effect on all branches *) | VtUnknown, _ when expr = VernacToplevelControl Drop -> - ignore(stm_vernac_interp (VCS.get_branch_pos head) _ds x); `Ok + let st = Vernacentries.freeze_interp_state `No in + ignore(stm_vernac_interp (VCS.get_branch_pos head) st x); + `Ok | VtSideff l, w -> let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in @@ -2747,8 +2790,8 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) VCS.checkout VCS.Branch.master; let mid = VCS.get_branch_pos VCS.Branch.master in let _st' = Reach.known_state ~cache:(VCS.is_interactive ()) mid in - ignore(stm_vernac_interp id _ds x); - + let st = Vernacentries.freeze_interp_state `No in + ignore(stm_vernac_interp id st x); (* Vernac x may or may not start a proof *) if not in_proof && Proof_global.there_are_pending_proofs () then begin @@ -2895,7 +2938,7 @@ type focus = { } let query ~doc ~at ~route s = - Future.purify (fun s -> + stm_purify (fun s -> if Stateid.equal at Stateid.dummy then ignore(finish ~doc:dummy_doc) else Reach.known_state ~cache:`Yes at; let loc, ast = parse_sentence ~doc at s in -- cgit v1.2.3