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 b46556ea6..01b75e496 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 b974d319e..231ec0547 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 c65cf6a9a..31f4599d3 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