diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-05-11 14:53:46 +0200 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-06 05:48:44 -0400 |
commit | 17f3346c5c42c16eed58bf2325aa996c3892a5e9 (patch) | |
tree | 632e37cb16782f02fe33ef51d88ff04952a8dd9a | |
parent | c4789644ab4d1a88f1331efb29b69011a30f5eed (diff) |
STM: invalid states are first class citizens
A state in the cache (document node) is now one of "Empty | Error | Valid".
This paves the way to commands/blocks-of-commands resilient-to/confining
errors: one can catch and "ignore" the exception obtained by reaching the
previous state and do something sensible, like running anyway the command
or skipping until the end of an error-confining block is reached.
Invalid states carry an enriched exception with the safe_id attached, so
that if one edits_at or observe them gets a safe place to land (CoqIDE
needs such piece of info).
Little API change in Stm.state_of_id now returning a `Error variant for
the new kind of state.
-rw-r--r-- | stm/stm.ml | 135 | ||||
-rw-r--r-- | stm/stm.mli | 2 |
2 files changed, 78 insertions, 59 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index e2acb1029..1dd089a26 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -187,20 +187,24 @@ let summary_pstate = [ Evarutil.meta_counter_summary_name; Evd.evar_counter_summary_name; "program-tcc-table" ] type state = { - system : States.state; - proof : Proof_global.state; - shallow : bool + system : States.state; (* summary + libstack *) + proof : Proof_global.state; (* proof state *) + shallow : bool (* is the state trimmed down (libstack) *) } +type cached_state = + | Empty + | Error of Exninfo.iexn + | Valid of state type branch = Vcs_.Branch.t * branch_type Vcs_.branch_info type backup = { mine : branch; others : branch list } -type 'vcs state_info = { (* Make private *) - mutable n_reached : int; - mutable n_goals : int; - mutable state : state option; +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 *) + mutable state : cached_state; (* state value *) mutable vcs_backup : 'vcs option * backup option; } let default_info () = - { n_reached = 0; n_goals = 0; state = None; vcs_backup = None,None } + { n_reached = 0; n_goals = 0; state = Empty; vcs_backup = None,None } (* Functions that work on a Vcs with a specific branch type *) module Vcs_aux : sig @@ -296,10 +300,10 @@ module VCS : sig val cur_tip : unit -> id val get_info : id -> vcs state_info - val reached : id -> bool -> unit + val reached : id -> unit val goals : id -> int -> unit - val set_state : id -> state -> unit - val get_state : id -> state option + val set_state : id -> cached_state -> unit + val get_state : id -> cached_state (* cuts from start -> stop, raising Expired if some nodes are not there *) val slice : start:id -> stop:id -> vcs @@ -345,11 +349,11 @@ end = struct (* {{{ *) | Qed { qast } -> string_of_ppcmds (pr_ast qast) in let is_green id = match get_info vcs id with - | Some { state = Some _ } -> true + | Some { state = Valid _ } -> true | _ -> false in let is_red id = match get_info vcs id with - | Some s -> Int.equal s.n_reached ~-1 + | Some { state = Error _ } -> true | _ -> false in let head = current_branch vcs in let heads = @@ -452,13 +456,12 @@ end = struct (* {{{ *) | Some x -> x | None -> raise Vcs_aux.Expired let set_state id s = - (get_info id).state <- Some s; + (get_info id).state <- s; if Flags.async_proofs_is_master () then Hooks.(call state_ready id) let get_state id = (get_info id).state - let reached id b = + let reached id = let info = get_info id in - if b then info.n_reached <- info.n_reached + 1 - else info.n_reached <- -1 + info.n_reached <- info.n_reached + 1 let goals id n = (get_info id).n_goals <- n let cur_tip () = get_branch_pos (current_branch ()) @@ -508,7 +511,7 @@ end = struct (* {{{ *) let l = nodes_in_slice ~start ~stop in let copy_info v id = Vcs_.set_info v id - { (get_info id) with state = None; vcs_backup = None,None } in + { (get_info id) with state = Empty; vcs_backup = None,None } in let copy_info_w_state v id = Vcs_.set_info v id { (get_info id) with vcs_backup = None,None } in let v = Vcs_.empty start in @@ -518,11 +521,12 @@ end = struct (* {{{ *) let v = copy_info v id in v) l v in (* Stm should have reached the beginning of proof *) - assert (not (Option.is_empty (get_info start).state)); + assert (match (get_info start).state with Valid _ -> true | _ -> false); (* We put in the new dag the most recent state known to master *) let rec fill id = - if (get_info id).state = None then fill (Vcs_aux.visit v id).next - else copy_info_w_state v id in + match (get_info id).state with + | Empty | Error _ -> fill (Vcs_aux.visit v id).next + | Valid _ -> copy_info_w_state v id in let v = fill stop in (* We put in the new dag the first state (since Qed shall run on it, * see check_task_aux) *) @@ -596,7 +600,10 @@ end = struct (* {{{ *) end (* }}} *) let state_of_id id = - try `Valid (VCS.get_info id).state + try match (VCS.get_info id).state with + | Valid s -> `Valid (Some s) + | Error (e,_) -> `Error e + | Empty -> `Valid None with VCS.Expired -> `Expired @@ -616,6 +623,7 @@ module State : sig val install_cached : Stateid.t -> unit val is_cached : ?cache:Summary.marshallable -> Stateid.t -> bool + val is_cached_and_valid : ?cache:Summary.marshallable -> Stateid.t -> bool val exn_on : Stateid.t -> ?valid:Stateid.t -> iexn -> iexn @@ -661,51 +669,60 @@ end = struct (* {{{ *) proof, Summary.project_summary (States.summary_of_state system) summary_pstate - let freeze marshallable id = VCS.set_state id (freeze_global_state marshallable) + let freeze marshallable id = + VCS.set_state id (Valid (freeze_global_state marshallable)) + let freeze_invalid id iexn = VCS.set_state id (Error iexn) - let is_cached ?(cache=`No) id = + let is_cached ?(cache=`No) id only_valid = if Stateid.equal id !cur_id then try match VCS.get_info id with - | { state = None } when cache = `Yes -> freeze `No id; true - | { state = None } when cache = `Shallow -> freeze `Shallow id; true + | { state = Empty } when cache = `Yes -> freeze `No id; true + | { state = Empty } when cache = `Shallow -> freeze `Shallow id; true | _ -> true with VCS.Expired -> false else try match VCS.get_info id with - | { state = Some _ } -> true - | _ -> false + | { state = Empty } -> false + | { state = Valid _ } -> true + | { state = Error _ } -> not only_valid with VCS.Expired -> false + let is_cached_and_valid ?cache id = is_cached ?cache id true + let is_cached ?cache id = is_cached ?cache id false + let install_cached id = - if Stateid.equal id !cur_id then () else (* optimization *) - let s = - match VCS.get_info id with - | { state = Some s } -> s - | _ -> anomaly (str "unfreezing a non existing state") in - unfreeze_global_state s; cur_id := id + 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 + | { state = Error ie } -> cur_id := id; Exninfo.iraise ie + | _ -> + (* coqc has a 1 slot cache and only for valid states *) + if interactive () = `No && Stateid.equal id !cur_id then () + else anomaly (str "installing a non cached state") let get_cached id = try match VCS.get_info id with - | { state = Some s } -> s + | { state = Valid s } -> s | _ -> anomaly (str "not a cached state") with VCS.Expired -> anomaly (str "not a cached state (expired)") let assign id what = - if VCS.get_state id <> None then () else + if VCS.get_state id <> Empty then () else try match what with | `Full s -> let s = try let prev = (VCS.visit id).next in - if is_cached prev + if is_cached_and_valid prev then { s with proof = Proof_global.copy_terminators ~src:(get_cached prev).proof ~tgt:s.proof } else s with VCS.Expired -> s in - VCS.set_state id s + VCS.set_state id (Valid s) | `Proof(ontop,(pstate,counters)) -> - if is_cached ontop then + if is_cached_and_valid ontop then let s = get_cached ontop in let s = { s with proof = Proof_global.copy_terminators ~src:s.proof ~tgt:pstate } in @@ -714,7 +731,7 @@ end = struct (* {{{ *) (Summary.surgery_summary (States.summary_of_state s.system) counters) } in - VCS.set_state id s + VCS.set_state id (Valid s) with VCS.Expired -> () let exn_on id ?valid (e, info) = @@ -753,20 +770,22 @@ end = struct (* {{{ *) cur_id := id; if feedback_processed then Hooks.(call state_computed id ~in_cache:false); - VCS.reached id true; + VCS.reached id; if Proof_global.there_are_pending_proofs () then VCS.goals id (Proof_global.get_open_goals ()) with e -> let (e, info) = Errors.push e in let good_id = !cur_id in - cur_id := Stateid.dummy; - VCS.reached id false; - Hooks.(call unreachable_state id (e, info)); - match Stateid.get info, safe_id with - | None, None -> iraise (exn_on id ~valid:good_id (e, info)) - | None, Some good_id -> iraise (exn_on id ~valid:good_id (e, info)) - | Some _, None -> iraise (e, info) - | Some (_,at), Some id -> iraise (e, Stateid.add info ~valid:id at) + VCS.reached id; + let ie = + match Stateid.get info, safe_id with + | None, None -> (exn_on id ~valid:good_id (e, info)) + | None, Some good_id -> (exn_on id ~valid:good_id (e, info)) + | Some _, None -> (e, info) + | Some (_,at), Some id -> (e, Stateid.add info ~valid:id at) in + if cache = `Yes || cache = `Shallow then freeze_invalid id ie; + Hooks.(call unreachable_state id ie); + Exninfo.iraise ie end (* }}} *) @@ -842,7 +861,7 @@ end = struct (* {{{ *) let back_safe () = let id = fold_until (fun n (id,_,_,_,_) -> - if n >= 0 && State.is_cached id then `Stop id else `Cont (succ n)) + if n >= 0 && State.is_cached_and_valid id then `Stop id else `Cont (succ n)) 0 (VCS.get_branch_pos (VCS.current_branch ())) in backto id @@ -1133,7 +1152,7 @@ end = struct (* {{{ *) let e_msg = iprint (e, info) in prerr_endline (fun () -> "failed with the following exception:"); prerr_endline (fun () -> string_of_ppcmds e_msg); - let e_safe_states = List.filter State.is_cached my_states in + let e_safe_states = List.filter State.is_cached_and_valid my_states in RespError { e_error_at; e_safe_id; e_msg; e_safe_states } let perform_states query = @@ -1151,12 +1170,12 @@ end = struct (* {{{ *) let prev = try let { next = prev; step } = VCS.visit id in - if State.is_cached prev && List.mem prev seen + if State.is_cached_and_valid prev && List.mem prev seen then Some (prev, State.get_cached prev, step) else None with VCS.Expired -> None in let this = - if State.is_cached id then Some (State.get_cached id) else None in + if State.is_cached_and_valid id then Some (State.get_cached id) else None in match prev, this with | _, None -> None | Some (prev, o, `Cmd { cast = { expr }}), Some n @@ -1724,7 +1743,7 @@ let collect_proof keep cur hd brkind id = let name = name ids in `ASync (parent last,proof_using_ast last,accn,name,delegate name) | `Fork((_, hd', GuaranteesOpacity, ids), _) when - has_proof_no_using last && not (State.is_cached (parent last)) && + has_proof_no_using last && not (State.is_cached_and_valid (parent last)) && !Flags.compilation_mode = Flags.BuildVio -> assert (VCS.Branch.equal hd hd'||VCS.Branch.equal hd VCS.edit_branch); (try @@ -1760,7 +1779,7 @@ let collect_proof keep cur hd brkind id = let rc = collect (Some cur) [] id in if is_empty rc then make_sync `AlreadyEvaluated rc else if (keep == VtKeep || keep == VtKeepAsAxiom) && - (not(State.is_cached id) || !Flags.async_proofs_full) + (not(State.is_cached_and_valid id) || !Flags.async_proofs_full) then check_policy rc else make_sync `AlreadyEvaluated rc @@ -1808,9 +1827,9 @@ let known_state ?(redefine_qed=false) ~cache id = and reach ?(redefine_qed=false) ?(cache=cache) id = prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id); if not redefine_qed && State.is_cached ~cache id then begin - State.install_cached id; Hooks.(call state_computed id ~in_cache:true); - prerr_endline (fun () -> "reached (cache)") + prerr_endline (fun () -> "reached (cache)"); + State.install_cached id end else let step, cache_step, feedback_processed = let view = VCS.visit id in @@ -1842,7 +1861,7 @@ let known_state ?(redefine_qed=false) ~cache id = reach view.next; vernac_interp id x; wall_clock_last_fork := Unix.gettimeofday () ), `Yes, true - | `Fork ((x,_,_,_), Some prev) -> (fun () -> + | `Fork ((x,_,_,_), Some prev) -> (fun () -> (* nested proof *) reach ~cache:`Shallow prev; reach view.next; (try vernac_interp id x; diff --git a/stm/stm.mli b/stm/stm.mli index 6ffe0beb4..d825ff33e 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -122,7 +122,7 @@ type state = { proof : Proof_global.state; shallow : bool } -val state_of_id : Stateid.t -> [ `Valid of state option | `Expired ] +val state_of_id : Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ] (** read-eval-print loop compatible interface ****************************** **) |