diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/proofBlockDelimiter.ml | 12 | ||||
| -rw-r--r-- | stm/stm.ml | 224 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 4 |
3 files changed, 140 insertions, 100 deletions
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index b8af2bcd56..230a3207a8 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -49,12 +49,12 @@ let is_focused_goal_simple ~doc id = match state_of_id ~doc id with | `Expired | `Error _ | `Valid None -> `Not | `Valid (Some { Vernacstate.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 - if List.for_all (fun x -> simple_goal sigma x rest) focused - then `Simple focused - else `Not + let proof = Proof_global.proof_of_state proof in + let Proof.{ goals=focused; stack=r1; shelf=r2; given_up=r3; sigma } = Proof.data proof in + let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in + if List.for_all (fun x -> simple_goal sigma x rest) focused + then `Simple focused + else `Not type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ] diff --git a/stm/stm.ml b/stm/stm.ml index e835bdcb1e..32c6c7d959 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -76,18 +76,6 @@ let async_proofs_is_master opt = opt.async_proofs_mode = APon && !Flags.async_proofs_worker_id = "master" -(* Protect against state changes *) -let stm_purify f x = - let st = Vernacstate.freeze_interp_state `No in - try - let res = f x in - Vernacstate.unfreeze_interp_state st; - res - with e -> - let e = CErrors.push e in - Vernacstate.unfreeze_interp_state st; - Exninfo.iraise e - let execution_error ?loc state_id msg = feedback ~id:state_id (Message (Error, loc, msg)) @@ -343,7 +331,7 @@ module VCS : sig val set_ldir : Names.DirPath.t -> unit val get_ldir : unit -> Names.DirPath.t - val is_interactive : unit -> [`Yes | `No | `Shallow] + val is_interactive : unit -> bool val is_vio_doc : unit -> bool val current_branch : unit -> Branch.t @@ -543,8 +531,8 @@ end = struct (* {{{ *) let is_interactive () = match !doc_type with - | Interactive _ -> `Yes - | _ -> `No + | Interactive _ -> true + | _ -> false let is_vio_doc () = match !doc_type with @@ -632,13 +620,20 @@ end = struct (* {{{ *) " to "^Stateid.to_string block_stop^".")) in aux block_stop + (* [slice] copies a slice of the DAG, keeping only the last known valid state. + When it copies a state, it drops the libobjects and keeps only the structure. *) let slice ~block_start ~block_stop = let l = nodes_in_slice ~block_start ~block_stop in let copy_info v id = Vcs_.set_info v id { (get_info id) with state = Empty; vcs_backup = None,None } in + let make_shallow = function + | Valid st -> Valid (Vernacstate.make_shallow st) + | x -> x + in let copy_info_w_state v id = - Vcs_.set_info v id { (get_info id) with vcs_backup = None,None } in + let info = get_info id in + Vcs_.set_info v id { info with state = make_shallow info.state; vcs_backup = None,None } in let copy_proof_blockes v = let nodes = Vcs_.Dag.all_nodes (Vcs_.dag v) in let props = @@ -750,7 +745,7 @@ end = struct (* {{{ *) end let print ?(now=false) () = - if not !Flags.debug && not now then () else NB.command ~now (print_dag !vcs) + if !Flags.debug then NB.command ~now (print_dag !vcs) let backup () = !vcs let restore v = vcs := v @@ -768,6 +763,11 @@ let state_of_id ~doc id = (****** A cache: fills in the nodes of the VCS document with their value ******) module State : sig + type t + + val freeze : unit -> t + val unfreeze : t -> unit + (** The function is from unit, so it uses the current state to define a new one. I.e. one may been to install the right state before defining a new one. @@ -776,14 +776,14 @@ module State : sig val define : doc:doc -> ?safe_id:Stateid.t -> - ?redefine:bool -> ?cache:Summary.marshallable -> + ?redefine:bool -> ?cache:bool -> ?feedback_processed:bool -> (unit -> unit) -> Stateid.t -> unit val fix_exn_ref : (Exninfo.iexn -> Exninfo.iexn) ref 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 is_cached : ?cache:bool -> Stateid.t -> bool + val is_cached_and_valid : ?cache:bool -> Stateid.t -> bool val exn_on : Stateid.t -> valid:Stateid.t -> Exninfo.iexn -> Exninfo.iexn @@ -808,13 +808,22 @@ module State : sig be removed in the state handling refactoring. *) val cur_id : Stateid.t ref + val purify : ('a -> 'b) -> 'a -> 'b + end = struct (* {{{ *) + type t = { id : Stateid.t; vernac_state : Vernacstate.t } + (* 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) + let freeze () = { id = !cur_id; vernac_state = Vernacstate.freeze_interp_state ~marshallable:false } + let unfreeze st = + Vernacstate.unfreeze_interp_state st.vernac_state; + cur_id := st.id + type proof_part = Proof_global.t * int * (* Evarutil.meta_counter_summary_tag *) @@ -832,16 +841,15 @@ end = struct (* {{{ *) Summary.project_from_summary st Util.(pi2 summary_pstate), Summary.project_from_summary st Util.(pi3 summary_pstate) - let freeze marshallable id = - VCS.set_state id (Valid (Vernacstate.freeze_interp_state marshallable)) + let cache_state ~marshallable id = + VCS.set_state id (Valid (Vernacstate.freeze_interp_state ~marshallable)) let freeze_invalid id iexn = VCS.set_state id (Error iexn) - let is_cached ?(cache=`No) id only_valid = + let is_cached ?(cache=false) id only_valid = if Stateid.equal id !cur_id then try match VCS.get_info id with - | { state = Empty } when cache = `Yes -> freeze `No id; true - | { state = Empty } when cache = `Shallow -> freeze `Shallow id; true + | { state = Empty } when cache -> cache_state ~marshallable:false id; true | _ -> true with VCS.Expired -> false else @@ -866,7 +874,7 @@ end = struct (* {{{ *) | _ -> (* coqc has a 1 slot cache and only for valid states *) - if VCS.is_interactive () = `No && Stateid.equal id !cur_id then () + if not (VCS.is_interactive ()) && Stateid.equal id !cur_id then () else anomaly Pp.(str "installing a non cached state.") let get_cached id = @@ -924,7 +932,9 @@ end = struct (* {{{ *) let e2 = Summary.project_from_summary s2 Global.global_env_summary_tag in e1 == e2 - let define ~doc ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true) + (* [define] puts the system in state [id] calling [f ()] *) + (* [safe_id] is the last known valid state before execution *) + let define ~doc ?safe_id ?(redefine=false) ?(cache=false) ?(feedback_processed=true) f id = feedback ~id:id (ProcessingIn !Flags.async_proofs_worker_id); @@ -933,13 +943,12 @@ end = struct (* {{{ *) anomaly Pp.(str"defining state "++str str_id++str" twice."); try stm_prerr_endline (fun () -> "defining "^str_id^" (cache="^ - if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)"); + if cache then "Y)" else "N)"); let good_id = match safe_id with None -> !cur_id | Some id -> id in fix_exn_ref := exn_on id ~valid:good_id; f (); fix_exn_ref := (fun x -> x); - if cache = `Yes then freeze `No id - else if cache = `Shallow then freeze `Shallow id; + if cache then cache_state ~marshallable:false id; stm_prerr_endline (fun () -> "setting cur id to "^str_id); cur_id := id; if feedback_processed then @@ -958,18 +967,32 @@ end = struct (* {{{ *) | 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; + if cache then freeze_invalid id ie; Hooks.(call unreachable_state ~doc id ie); Exninfo.iraise ie let init_state = ref None let register_root_state () = - init_state := Some (Vernacstate.freeze_interp_state `No) + init_state := Some (Vernacstate.freeze_interp_state ~marshallable:false) let restore_root_state () = cur_id := Stateid.dummy; - Vernacstate.unfreeze_interp_state (Option.get !init_state); + Vernacstate.unfreeze_interp_state (Option.get !init_state) + + (* Protect against state changes *) + let purify f x = + let st = freeze () in + try + let res = f x in + Vernacstate.invalidate_cache (); + unfreeze st; + res + with e -> + let e = CErrors.push e in + Vernacstate.invalidate_cache (); + unfreeze st; + Exninfo.iraise e end (* }}} *) @@ -1178,7 +1201,7 @@ end = struct (* {{{ *) | _ -> None let undo_vernac_classifier v ~doc = - if VCS.is_interactive () = `No && !cur_opt.async_proofs_cache <> Some Force + if not (VCS.is_interactive ()) && !cur_opt.async_proofs_cache <> Some Force then undo_costly_in_batch_mode v; try match Vernacprop.under_control v with @@ -1508,9 +1531,7 @@ end = struct (* {{{ *) let build_proof_here ~doc ?loc ~drop_pt (id,valid) eop = Future.create (State.exn_on id ~valid) (fun () -> let wall_clock1 = Unix.gettimeofday () in - if VCS.is_interactive () = `No - then Reach.known_state ~doc ~cache:`No eop - else Reach.known_state ~doc ~cache:`Shallow eop; + Reach.known_state ~doc ~cache:(VCS.is_interactive ()) eop; let wall_clock2 = Unix.gettimeofday () in Aux_file.record_in_aux_at ?loc "proof_build_time" (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); @@ -1532,20 +1553,20 @@ end = struct (* {{{ *) * a bad fixpoint *) let fix_exn = Future.fix_exn_of future_proof in (* STATE: We use the current installed imperative state *) - let st = Vernacstate.freeze_interp_state `No in + let st = State.freeze () in if not drop then begin let checked_proof = Future.chain future_proof (fun p -> let opaque = Proof_global.Opaque in (* Unfortunately close_future_proof and friends are not pure so we need to set the state manually here *) - Vernacstate.unfreeze_interp_state st; + State.unfreeze st; let pobject, _ = Proof_global.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in let terminator = (* The one sent by master is an InvalidKey *) Lemmas.(standard_proof_terminator []) in - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in stm_vernac_interp stop ~proof:(pobject, terminator) st { verbose = false; loc; indentation = 0; strlen = 0; @@ -1553,7 +1574,7 @@ end = struct (* {{{ *) ignore(Future.join checked_proof); end; (* STATE: Restore the state XXX: handle exn *) - Vernacstate.unfreeze_interp_state st; + State.unfreeze st; RespBuiltProof(proof,time) with | e when CErrors.noncritical e || e = Stack_overflow -> @@ -1676,7 +1697,7 @@ end = struct (* {{{ *) with VCS.Expired -> cur in aux stop in try - Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:`No stop; + Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:false stop; if drop then let _proof = Proof_global.return_proof ~allow_partial:true () in `OK_ADMITTED @@ -1689,14 +1710,14 @@ end = struct (* {{{ *) Proof_global.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in (* 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 ~doc:dummy_doc (* XXX should be document *) ~cache:`No start; + Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:false start; (* STATE SPEC: * - start: First non-expired state! [This looks very fishy] * - end : start + qed * => takes nothing from the itermediate states. *) (* STATE We use the state resulting from reaching start. *) - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp stop ~proof st { verbose = false; loc; indentation = 0; strlen = 0; expr = VernacExpr ([], VernacEndProof (Proved (opaque,None))) }); @@ -1934,9 +1955,9 @@ end = struct (* {{{ *) let perform { r_state = id; r_state_fb; r_document = vcs; r_ast; r_goal } = Option.iter VCS.restore vcs; try - Reach.known_state ~doc:dummy_doc (* XXX should be vcs *) ~cache:`No id; - stm_purify (fun () -> - let _,_,_,_,sigma0 = Proof.proof (Proof_global.give_me_the_proof ()) in + Reach.known_state ~doc:dummy_doc (* XXX should be vcs *) ~cache:false id; + State.purify (fun () -> + let Proof.{sigma=sigma0} = Proof.data (Proof_global.give_me_the_proof ()) in let g = Evd.find sigma0 r_goal in let is_ground c = Evarutil.is_ground_term sigma0 c in if not ( @@ -1955,9 +1976,9 @@ end = struct (* {{{ *) * => captures state id in a future closure, which will discard execution state but for the proof + univs. *) - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp r_state_fb st ast); - let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in + let Proof.{sigma} = Proof.data (Proof_global.give_me_the_proof ()) in match Evd.(evar_body (find sigma r_goal)) with | Evd.Evar_empty -> RespNoProgress | Evd.Evar_defined t -> @@ -1994,12 +2015,12 @@ end = struct (* {{{ *) | VernacFail e -> find ~time ~batch ~fail:true e | e -> e, time, batch, fail in find ~time:false ~batch:false ~fail:false e in - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in Vernacentries.with_fail st fail (fun () -> (if time then System.with_time ~batch else (fun x -> x)) (fun () -> ignore(TaskQueue.with_n_workers nworkers (fun queue -> Proof_global.with_current_proof (fun _ p -> - let goals, _, _, _, _ = Proof.proof p in + let Proof.{goals} = Proof.data p in let open TacTask in let res = CList.map_i (fun i g -> let f, assign = @@ -2089,9 +2110,9 @@ end = struct (* {{{ *) let perform { r_where; r_doc; r_what; r_for } = VCS.restore r_doc; VCS.print (); - Reach.known_state ~doc:dummy_doc (* XXX should be r_doc *) ~cache:`No r_where; + Reach.known_state ~doc:dummy_doc (* XXX should be r_doc *) ~cache:false r_where; (* STATE *) - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in try (* STATE SPEC: * - start: r_where @@ -2133,14 +2154,14 @@ end (* }}} *) and Reach : sig val known_state : - doc:doc -> ?redefine_qed:bool -> cache:Summary.marshallable -> + doc:doc -> ?redefine_qed:bool -> cache:bool -> Stateid.t -> unit end = struct (* {{{ *) let async_policy () = - if Attributes.is_universe_polymorphism () then false - else if VCS.is_interactive () = `Yes then + if Attributes.is_universe_polymorphism () then false (* FIXME this makes no sense, it is the default value of the attribute *) + else if VCS.is_interactive () then (async_proofs_is_master !cur_opt || !cur_opt.async_proofs_mode = APonLazy) else (VCS.is_vio_doc () || !cur_opt.async_proofs_mode <> APoff) @@ -2322,7 +2343,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = * - end : maybe after recovery command. *) (* STATE: We use an updated state with proof *) - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in Option.iter (fun expr -> ignore(stm_vernac_interp id st { verbose = true; loc = None; expr; indentation = 0; strlen = 0 } )) @@ -2358,17 +2379,17 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = (* ugly functions to process nested lemmas, i.e. hard to reproduce * side effects *) let cherry_pick_non_pstate () = - let st = Summary.freeze_summaries ~marshallable:`No in + let st = Summary.freeze_summaries ~marshallable:false in let st = Summary.remove_from_summary st Util.(pi1 summary_pstate) in let st = Summary.remove_from_summary st Util.(pi2 summary_pstate) in let st = Summary.remove_from_summary st Util.(pi3 summary_pstate) in - st, Lib.freeze ~marshallable:`No in + st, Lib.freeze ~marshallable:false in let inject_non_pstate (s,l) = Summary.unfreeze_summaries ~partial:true s; Lib.unfreeze l; update_global_env () in let rec pure_cherry_pick_non_pstate safe_id id = - stm_purify (fun id -> + State.purify (fun id -> stm_prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id); reach ~safe_id id; cherry_pick_non_pstate ()) @@ -2393,7 +2414,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = | `Cmd { cast = x; cqueue = `TacQueue (solve,abstract,cancel_switch); cblock } -> (fun () -> resilient_tactic id cblock (fun () -> - reach ~cache:`Shallow view.next; + reach ~cache:true view.next; Partac.vernac_interp ~solve ~abstract ~cancel_switch !cur_opt.async_proofs_n_tacworkers view.next id x) ), cache, true @@ -2406,39 +2427,39 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = resilient_tactic id cblock (fun () -> reach view.next; (* State resulting from reach *) - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp id st x) ); if eff then update_global_env () - ), (if eff then `Yes else cache), true + ), eff || cache, true | `Cmd { cast = x; ceff = eff } -> (fun () -> (match !cur_opt.async_proofs_mode with | APon | APonLazy -> resilient_command reach view.next | APoff -> reach view.next); - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp id st x); if eff then update_global_env () - ), (if eff then `Yes else cache), true + ), eff || cache, true | `Fork ((x,_,_,_), None) -> (fun () -> resilient_command reach view.next; - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp id st x); wall_clock_last_fork := Unix.gettimeofday () - ), `Yes, true + ), true, true | `Fork ((x,_,_,_), Some prev) -> (fun () -> (* nested proof *) - reach ~cache:`Shallow prev; + reach ~cache:true prev; reach view.next; (try - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false 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 Exninfo.iraise (e, info)); wall_clock_last_fork := Unix.gettimeofday () - ), `Yes, true + ), true, true | `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) -> let rec aux = function | `ASync (block_start, nodes, name, delegate) -> (fun () -> @@ -2468,7 +2489,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = State.install_cached id | { VCS.kind = `Proof _ }, Some _ -> assert false | { VCS.kind = `Proof _ }, None -> - reach ~cache:`Shallow block_start; + reach ~cache:true block_start; let fp, cancel = if delegate then Slaves.build_proof ~doc @@ -2487,19 +2508,19 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = Proof_global.close_future_proof ~opaque ~feedback_id:id fp in if not delegate then ignore(Future.compute fp); reach view.next; - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false 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 + ), not redefine_qed, true | `Sync (name, `Immediate) -> (fun () -> reach eop; - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp id st x); Proof_global.discard_all () - ), `Yes, true + ), true, true | `Sync (name, reason) -> (fun () -> log_processing_sync id name reason; reach eop; @@ -2523,25 +2544,25 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = if keep <> VtKeep VtKeepAxiom then reach view.next; let wall_clock2 = Unix.gettimeofday () in - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false 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)); Proof_global.discard_all () - ), `Yes, true + ), true, true | `MaybeASync (start, nodes, name, delegate) -> (fun () -> - reach ~cache:`Shallow start; + reach ~cache:true start; (* no sections *) if CList.is_empty (Environ.named_context (Global.env ())) then Util.pi1 (aux (`ASync (start, nodes, name, delegate))) () else Util.pi1 (aux (`Sync (name, `NoPU_NoHint_NoES))) () - ), (if redefine_qed then `No else `Yes), true + ), not redefine_qed, true in aux (collect_proof keep (view.next, x) brname brinfo eop) | `Sideff (ReplayCommand x,_) -> (fun () -> reach view.next; - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in ignore(stm_vernac_interp id st x); update_global_env () ), cache, true @@ -2551,8 +2572,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = ), cache, true in let cache_step = - if !cur_opt.async_proofs_cache = Some Force then `Yes - else cache_step in + !cur_opt.async_proofs_cache = Some Force || cache_step + in State.define ~doc ?safe_id ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id; stm_prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in @@ -2671,7 +2692,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = load_objs require_libs; (* We record the state at this point! *) - State.define ~doc ~cache:`Yes ~redefine:true (fun () -> ()) Stateid.initial; + State.define ~doc ~cache:true ~redefine:true (fun () -> ()) Stateid.initial; Backtrack.record (); Slaves.init (); if async_proofs_is_master !cur_opt then begin @@ -2715,7 +2736,7 @@ let finish ~doc = ); doc let wait ~doc = - let doc = finish ~doc in + let doc = observe ~doc (VCS.get_branch_pos VCS.Branch.master) in Slaves.wait_all_done (); VCS.print (); doc @@ -2729,12 +2750,29 @@ let rec join_admitted_proofs id = join_admitted_proofs view.next | _ -> join_admitted_proofs view.next +(* Error resiliency may have tolerated some broken commands *) +let rec check_no_err_states ~doc visited id = + let open Stateid in + if Set.mem id visited then visited else + match state_of_id ~doc id with + | `Error e -> raise e + | _ -> + let view = VCS.visit id in + match view.step with + | `Qed(_,id) -> + let visited = check_no_err_states ~doc (Set.add id visited) id in + check_no_err_states ~doc visited view.next + | _ -> check_no_err_states ~doc (Set.add id visited) view.next + let join ~doc = let doc = wait ~doc in stm_prerr_endline (fun () -> "Joining the environment"); Global.join_safe_environment (); stm_prerr_endline (fun () -> "Joining Admitted proofs"); - join_admitted_proofs (VCS.get_branch_pos (VCS.current_branch ())); + join_admitted_proofs (VCS.get_branch_pos VCS.Branch.master); + stm_prerr_endline (fun () -> "Checking no error states"); + ignore(check_no_err_states ~doc (Stateid.Set.singleton Stateid.initial) + (VCS.get_branch_pos VCS.Branch.master)); VCS.print (); doc @@ -2745,7 +2783,7 @@ let check_task name (tasks,rcbackup) i = RemoteCounter.restore rcbackup; let vcs = VCS.backup () in try - let rc = stm_purify (Slaves.check_task name tasks) i in + let rc = State.purify (Slaves.check_task name tasks) i in VCS.restore vcs; rc with e when CErrors.noncritical e -> VCS.restore vcs; false @@ -2755,7 +2793,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 = stm_purify (Slaves.finish_task name u d p t) i in + let u = State.purify (Slaves.finish_task name u d p t) i in VCS.restore vcs; u in try @@ -2785,7 +2823,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 (); - let _st : unit = Reach.known_state ~doc:dummy_doc (* XXX should be taken in input *) ~redefine_qed:true ~cache:`No qed_id in + let _st : unit = Reach.known_state ~doc:dummy_doc (* XXX should be taken in input *) ~redefine_qed:true ~cache:false qed_id in VCS.checkout VCS.Branch.master; `Unfocus qed_id | { VCS.kind = `Master } -> @@ -2957,12 +2995,12 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) 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 - let _st : unit = Reach.known_state ~doc ~cache:`Yes head_id in (* ensure it is ok *) + let _st : unit = Reach.known_state ~doc ~cache:true head_id in (* ensure it is ok *) let step () = VCS.checkout VCS.Branch.master; let mid = VCS.get_branch_pos VCS.Branch.master in let _st' : unit = Reach.known_state ~doc ~cache:(VCS.is_interactive ()) mid in - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false 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 @@ -2987,7 +3025,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) end; VCS.checkout_shallowest_proof_branch (); end in - State.define ~doc ~safe_id:head_id ~cache:`Yes step id; + State.define ~doc ~safe_id:head_id ~cache:true step id; Backtrack.record (); `Ok | VtUnknown, VtLater -> @@ -3114,9 +3152,9 @@ type focus = { } let query ~doc ~at ~route s = - stm_purify (fun s -> + State.purify (fun s -> if Stateid.equal at Stateid.dummy then ignore(finish ~doc:dummy_doc) - else Reach.known_state ~doc ~cache:`Yes at; + else Reach.known_state ~doc ~cache:true at; try while true do let { CAst.loc; v=ast } = parse_sentence ~doc at s in diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 44d07279fc..f40b3e901b 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -56,7 +56,9 @@ let stm_allow_nested_proofs_option_name = ["Nested";"Proofs";"Allowed"] let options_affecting_stm_scheduling = [ Attributes.universe_polymorphism_option_name; - stm_allow_nested_proofs_option_name ] + stm_allow_nested_proofs_option_name; + Proof_global.proof_mode_opt_name; + ] let classify_vernac e = let static_classifier ~poly e = match e with |