| products/sources/formale Sprachen/Coq/stm/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Sprache: SMLOriginal von: Coq© |
|
||||||
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *) (* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) (* enable in case of stm problems *) (* let stm_debug () = !Flags.debug *) let stm_debug = ref false let stm_pr_err s = Format.eprintf "%s] %s\n%!" (Spawned.process_id ()) s let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n%!" (Spawned.process_id ()) Pp.pp_with pp let stm_prerr_endline s = if !stm_debug then begin stm_pr_err (s ()) end else () let stm_pperr_endline s = if !stm_debug then begin stm_pp_err (s ()) end else () let stm_prerr_debug s = if !Flags.debug then begin stm_pr_err (s ()) end else () open Pp open CErrors open Names open Feedback open Vernacexpr open Vernacextend module PG_compat = Vernacstate.Proof_global [@@ocaml.warning "-3"] let is_vtkeep = function VtKeep _ -> true | _ -> false let get_vtkeep = function VtKeep x -> x | _ -> assert false module AsyncOpts = struct type cache = Force type async_proofs = APoff | APonLazy | APon type tac_error_filter = [ `None | `Only of string list | `All ] type stm_opt = { async_proofs_n_workers : int; async_proofs_n_tacworkers : int; async_proofs_cache : cache option; async_proofs_mode : async_proofs; async_proofs_private_flags : string option; async_proofs_never_reopen_branch : bool; async_proofs_tac_error_resilience : tac_error_filter; async_proofs_cmd_error_resilience : bool; async_proofs_delegation_threshold : float; } let default_opts = { async_proofs_n_workers = 1; async_proofs_n_tacworkers = 2; async_proofs_cache = None; async_proofs_mode = APoff; async_proofs_private_flags = None; async_proofs_never_reopen_branch = false; async_proofs_tac_error_resilience = `Only [ "curly" ]; async_proofs_cmd_error_resilience = true; async_proofs_delegation_threshold = 0.03; } let cur_opt = ref default_opts end open AsyncOpts let async_proofs_is_master opt = opt.async_proofs_mode = APon && !Flags.async_proofs_worker_id = "master" let execution_error ?loc state_id msg = feedback ~id:state_id (Message (Error, loc, msg)) module Hooks = struct let state_computed, state_computed_hook = Hook.make ~default:(fun ~doc:_ state_id ~in_cache -> feedback ~id:state_id Processed) () let state_ready, state_ready_hook = Hook.make ~default:(fun ~doc:_ state_id -> ()) () let forward_feedback, forward_feedback_hook = let m = Mutex.create () in Hook.make ~default:(function | { doc_id = did; span_id = id; route; contents } -> try Mutex.lock m; feedback ~did ~id ~route contents; Mutex.unlock m with e -> Mutex.unlock m; raise e) () let unreachable_state, unreachable_state_hook = Hook.make ~default:(fun ~doc:_ _ _ -> ()) () let document_add, document_add_hook = Hook.make ~default:(fun _ _ -> ()) () let document_edit, document_edit_hook = Hook.make ~default:(fun _ -> ()) () let sentence_exec, sentence_exec_hook = Hook.make ~default:(fun _ -> ()) () include Hook (* enables: Hooks.(call foo args) *) let call = get let call_process_error_once = let processed : unit Exninfo.t = Exninfo.make () in fun (_, info as ei) -> match Exninfo.get info processed with | Some _ -> ei | None -> let e, info = ExplainErr.process_vernac_interp_error ei in let info = Exninfo.add info processed () in e, info end let async_proofs_workers_extra_env = ref [||] type aast = { verbose : bool; loc : Loc.t option; indentation : int; strlen : int; mutable expr : vernac_control; (* mutable: Proof using hinted by aux file *) } let pr_ast { expr; indentation } = Pp.(int indentation ++ str " " ++ Ppvernac.pr_vernac expr) (* Commands piercing opaque *) let may_pierce_opaque = function | VernacPrint _ | VernacExtend (("Extraction",_), _) | VernacExtend (("SeparateExtraction",_), _) | VernacExtend (("ExtractionLibrary",_), _) | VernacExtend (("RecursiveExtractionLibrary",_), _) | VernacExtend (("ExtractionConstant",_), _) | VernacExtend (("ExtractionInlinedConstant",_), _) | VernacExtend (("ExtractionInductive",_), _) -> true | _ -> false let update_global_env () = if PG_compat.there_are_pending_proofs () then PG_compat.update_global_env () module Vcs_ = Vcs.Make(Stateid.Self) type future_proof = Proof_global.closed_proof_output Future.computation type depth = int type branch_type = [ `Master | `Proof of depth | `Edit of Stateid.t * Stateid.t * Vernacextend.vernac_qed_type * Vcs_.Branch.t ] (* TODO 8.7 : split commands and tactics, since this type is too messy now *) type cmd_t = { ctac : bool; (* is a tactic *) ceff : bool; (* is a side-effecting command in the middle of a proof *) cast : aast; cids : Names.Id.t list; cblock : proof_block_name option; cqueue : [ `MainQueue | `TacQueue of solving_tac * anon_abstracting_tac * AsyncTaskQueue.cancel_switch | `QueryQueue of AsyncTaskQueue.cancel_switch | `SkipQueue ] } type fork_t = aast * Vcs_.Branch.t * opacity_guarantee * Names.Id.t list type qed_t = { qast : aast; keep : vernac_qed_type; mutable fproof : (future_proof * AsyncTaskQueue.cancel_switch) option; brname : Vcs_.Branch.t; brinfo : branch_type Vcs_.branch_info } type seff_t = ReplayCommand of aast | CherryPickEnv type alias_t = Stateid.t * aast type transaction = | Cmd of cmd_t | Fork of fork_t | Qed of qed_t | Sideff of seff_t | Alias of alias_t | Noop type step = [ `Cmd of cmd_t | `Fork of fork_t * Stateid.t option | `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 } (* Parts of the system state that are morally part of the proof state *) let summary_pstate = Evarutil.meta_counter_summary_tag, Evd.evar_counter_summary_tag, Obligations.program_tcc_summary_tag type cached_state = | EmptyState | ParsingState of Vernacstate.Parser.state | FullState of Vernacstate.t | ErrorState of Vernacstate.Parser.state option * Exninfo.iexn 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 *) mutable state : cached_state; (* state value *) mutable proof_mode : Pvernac.proof_mode option; mutable vcs_backup : 'vcs option * backup option; } let default_info proof_mode = { n_reached = 0; n_goals = 0; state = EmptyState; proof_mode; vcs_backup = (None,None); } module DynBlockData : Dyn.S = Dyn.Make () (* Clusters of nodes implemented as Dag properties. While Dag and Vcs impose * no constraint on properties, here we impose boxes to be non overlapping. * Such invariant makes sense for the current kinds of boxes (proof blocks and * entire proofs) but may make no sense and dropped/refined in the future. * Such invariant is useful to detect broken proof block detection code *) type box = | ProofTask of pt | ProofBlock of static_block_declaration * proof_block_name and pt = { (* TODO: inline records in OCaml 4.03 *) lemma : Stateid.t; qed : Stateid.t; } and static_block_declaration = { block_start : Stateid.t; block_stop : Stateid.t; dynamic_switch : Stateid.t; carry_on_data : DynBlockData.t; } (* Functions that work on a Vcs with a specific branch type *) module Vcs_aux : sig val proof_nesting : (branch_type, 't,'i,'c) Vcs_.t -> int val find_proof_at_depth : (branch_type, 't, 'i,'c) Vcs_.t -> int -> Vcs_.Branch.t * branch_type Vcs_.branch_info exception Expired val visit : (branch_type, transaction,'i,'c) Vcs_.t -> Vcs_.Dag.node -> visit end = struct (* {{{ *) let proof_nesting vcs = List.fold_left max 0 (CList.map_filter (function | { Vcs_.kind = `Proof n } -> Some n | { Vcs_.kind = `Edit _ } -> Some 1 | _ -> None) (List.map (Vcs_.get_branch vcs) (Vcs_.branches vcs))) let find_proof_at_depth vcs pl = try List.find (function | _, { Vcs_.kind = `Proof n } -> Int.equal n pl | _, { Vcs_.kind = `Edit _ } -> anomaly(Pp.str "find_proof_at_depth") | _ -> false) (List.map (fun h -> h, Vcs_.get_branch vcs h) (Vcs_.branches vcs)) with Not_found -> failwith "find_proof_at_depth" exception Expired let visit vcs id = if Stateid.equal id Stateid.initial then anomaly(Pp.str "Visiting the initial state id.") else if Stateid.equal id Stateid.dummy then anomaly(Pp.str "Visiting the dummy state id.") else try match Vcs_.Dag.from_node (Vcs_.dag vcs) id with | [n, Cmd x] -> { step = `Cmd x; next = n } | [n, Alias x] -> { step = `Alias x; next = n } | [n, Fork x] -> { step = `Fork (x,None); next = n } | [n, Fork x; p, Noop] -> { step = `Fork (x,Some p); next = n } | [p, Noop; n, Fork x] -> { step = `Fork (x,Some p); next = n } | [n, Qed x; p, Noop] | [p, Noop; n, Qed x] -> { step = `Qed (x,p); next = n } | [n, Sideff CherryPickEnv; p, Noop] | [p, Noop; n, Sideff CherryPickEnv]-> { step = `Sideff (CherryPickEnv, p); next = n } | [n, Sideff (ReplayCommand x); p, Noop] | [p, Noop; n, Sideff (ReplayCommand x)]-> { step = `Sideff(ReplayCommand x,p); next = n } | [n, Sideff (ReplayCommand x)]-> {step = `Sideff(ReplayCommand x, Stateid.dummy); next=n} | _ -> anomaly (Pp.str ("Malformed VCS at node "^Stateid.to_string id^".")) with Not_found -> raise Expired end (* }}} *) (*************************** THE DOCUMENT *************************************) (******************************************************************************) type interactive_top = TopLogical of DirPath.t | TopPhysical of string (* The main document type associated to a VCS *) type stm_doc_type = | VoDoc of string | VioDoc of string | Interactive of interactive_top (* Dummy until we land the functional interp patch + fixed start_library *) type doc = int let dummy_doc : doc = 0 (* Imperative wrap around VCS to obtain _the_ VCS that is the * representation of the document Coq is currently processing *) module VCS : sig exception Expired module Branch : (module type of Vcs_.Branch with type t = Vcs_.Branch.t) type id = Stateid.t type 'branch_type branch_info = 'branch_type Vcs_.branch_info = { kind : [> `Master] as 'branch_type; root : id; pos : id; } type vcs = (branch_type, transaction, vcs state_info, box) Vcs_.t val init : stm_doc_type -> id -> Vernacstate.Parser.state -> doc (* val get_type : unit -> stm_doc_type *) val set_ldir : Names.DirPath.t -> unit val get_ldir : unit -> Names.DirPath.t val is_interactive : unit -> bool val is_vio_doc : unit -> bool val current_branch : unit -> Branch.t val checkout : Branch.t -> unit val branches : unit -> Branch.t list val get_branch : Branch.t -> branch_type branch_info val get_branch_pos : Branch.t -> id val new_node : ?id:Stateid.t -> Pvernac.proof_mode option -> unit -> id val merge : id -> ours:transaction -> ?into:Branch.t -> Branch.t -> unit val rewrite_merge : id -> ours:transaction -> at:id -> Branch.t -> unit val delete_branch : Branch.t -> unit val commit : id -> transaction -> unit val mk_branch_name : aast -> Branch.t val edit_branch : Branch.t val branch : ?root:id -> ?pos:id -> Branch.t -> branch_type -> unit val reset_branch : Branch.t -> id -> unit val reachable : id -> Stateid.Set.t val cur_tip : unit -> id val get_info : id -> vcs state_info val reached : id -> unit val goals : id -> int -> unit val set_state : id -> cached_state -> unit val get_state : id -> cached_state val set_parsing_state : id -> Vernacstate.Parser.state -> unit val get_parsing_state : id -> Vernacstate.Parser.state option val get_proof_mode : id -> Pvernac.proof_mode option val set_proof_mode : id -> Pvernac.proof_mode option -> unit (* cuts from start -> stop, raising Expired if some nodes are not there *) val slice : block_start:id -> block_stop:id -> vcs val nodes_in_slice : block_start:id -> block_stop:id -> Stateid.t list val create_proof_task_box : id list -> qed:id -> block_start:id -> unit val create_proof_block : static_block_declaration -> string -> unit val box_of : id -> box list val delete_boxes_of : id -> unit val proof_task_box_of : id -> pt option val proof_nesting : unit -> int val checkout_shallowest_proof_branch : unit -> unit val propagate_sideff : action:seff_t -> Stateid.t list val propagate_qed : unit -> unit val gc : unit -> unit val visit : id -> visit val print : ?now:bool -> unit -> unit val backup : unit -> vcs val restore : vcs -> unit end = struct (* {{{ *) include Vcs_ exception Expired = Vcs_aux.Expired open Printf let print_dag vcs () = (* Due to threading, be wary that this will be called from the toplevel with we_are_parsing set to true, as indeed, the toplevel is waiting for input . What a race! XD In case you are hitting the race enable stm_debug. *) if !stm_debug then Flags.we_are_parsing := false; let fname = "stm_" ^ Str.global_replace (Str.regexp " ") "_" (Spawned.process_id ()) in let string_of_transaction = function | Cmd { cast = t } | Fork (t, _,_,_) -> (try Pp.string_of_ppcmds (pr_ast t) with _ -> "ERR") | Sideff (ReplayCommand t) -> sprintf "Sideff(%s)" (try Pp.string_of_ppcmds (pr_ast t) with _ -> "ERR") | Sideff CherryPickEnv -> "EnvChange" | Noop -> " " | Alias (id,_) -> sprintf "Alias(%s)" (Stateid.to_string id) | Qed { qast } -> Pp.string_of_ppcmds (pr_ast qast) in let is_green id = match get_info vcs id with | Some { state = FullState _ } -> true | _ -> false in let is_red id = match get_info vcs id with | Some { state = ErrorState _ } -> true | _ -> false in let head = current_branch vcs in let heads = List.map (fun x -> x, (get_branch vcs x).pos) (branches vcs) in let graph = dag vcs in let quote s = Str.global_replace (Str.regexp "\n") " " (Str.global_replace (Str.regexp "<") "<" (Str.global_replace (Str.regexp ">") ">" (Str.global_replace (Str.regexp "\"") """ (Str.global_replace (Str.regexp "&") "&" (String.sub s 0 (min (String.length s) 20)))))) in let fname_dot, fname_ps = let f = "/tmp/" ^ Filename.basename fname in f ^ ".dot", f ^ ".pdf" in let node id = "s" ^ Stateid.to_string id in let edge tr = sprintf "<12\" FACE=\"sans\">%s>" (quote (string_of_transaction tr)) in let node_info id = match get_info vcs id with | None -> "" | Some info -> sprintf "<12\">%s" (Stateid.to_string id) ^ sprintf " 11\">r:%d g:%d>" info.n_reached info.n_goals in let color id = if is_red id then "red" else if is_green id then "green" else "white" in let nodefmt oc id = fprintf oc "%s [label=%s,style=filled,fillcolor=%s];\n" (node id) (node_info id) (color id) in let ids = ref Stateid.Set.empty in let boxes = ref [] in (* Fill in *) Dag.iter graph (fun from _ _ l -> ids := Stateid.Set.add from !ids; List.iter (fun box -> boxes := box :: !boxes) (Dag.property_of graph from); List.iter (fun (dest, _) -> ids := Stateid.Set.add dest !ids; List.iter (fun box -> boxes := box :: !boxes) (Dag.property_of graph dest)) l); boxes := CList.sort_uniquize Dag.Property.compare !boxes; let oc = open_out fname_dot in output_string oc "digraph states {\n"; Dag.iter graph (fun from cf _ l -> List.iter (fun (dest, trans) -> fprintf oc "%s -> %s [xlabel=%s,labelfloat=true];\n" (node from) (node dest) (edge trans)) l ); let contains b1 b2 = Stateid.Set.subset (Dag.Property.having_it b2) (Dag.Property.having_it b1) in let same_box = Dag.Property.equal in let outerboxes boxes = List.filter (fun b -> not (List.exists (fun b1 -> not (same_box b1 b) && contains b1 b) boxes) ) boxes in let rec rec_print b = boxes := CList.remove same_box b !boxes; let sub_boxes = List.filter (contains b) (outerboxes !boxes) in fprintf oc "subgraph cluster_%s {\n" (Dag.Property.to_string b); List.iter rec_print sub_boxes; Stateid.Set.iter (fun id -> if Stateid.Set.mem id !ids then begin ids := Stateid.Set.remove id !ids; nodefmt oc id end) (Dag.Property.having_it b); match Dag.Property.data b with | ProofBlock ({ dynamic_switch = id }, lbl) -> fprintf oc "label=\"%s (test:%s)\";\n" lbl (Stateid.to_string id); fprintf oc "color=red; }\n" | ProofTask _ -> fprintf oc "color=blue; }\n" in List.iter rec_print (outerboxes !boxes); Stateid.Set.iter (nodefmt oc) !ids; List.iteri (fun i (b,id) -> let shape = if Branch.equal head b then "box3d" else "box" in fprintf oc "b%d -> %s;\n" i (node id); fprintf oc "b%d [shape=%s,label=\"%s\"];\n" i shape (Branch.to_string b); ) heads; output_string oc "}\n"; close_out oc; ignore(Sys.command ("dot -Tpdf -Gcharset=latin1 " ^ fname_dot ^ " -o" ^ fname_ps)) type vcs = (branch_type, transaction, vcs state_info, box) t let vcs : vcs ref = ref (empty Stateid.dummy) let doc_type = ref (Interactive (TopLogical (Names.DirPath.make []))) let ldir = ref Names.DirPath.empty let init dt id ps = doc_type := dt; vcs := empty id; let info = { (default_info None) with state = ParsingState ps } in vcs := set_info !vcs id info; dummy_doc let set_ldir ld = ldir := ld let get_ldir () = !ldir (* let get_type () = !doc_type *) let is_interactive () = match !doc_type with | Interactive _ -> true | _ -> false let is_vio_doc () = match !doc_type with | VioDoc _ -> true | _ -> false let current_branch () = current_branch !vcs let checkout head = vcs := checkout !vcs head let branches () = branches !vcs let get_branch head = get_branch !vcs head let get_branch_pos head = (get_branch head).pos let new_node ?(id=Stateid.fresh ()) proof_mode () = assert(Vcs_.get_info !vcs id = None); vcs := set_info !vcs id (default_info proof_mode); id let merge id ~ours ?into branch = vcs := merge !vcs id ~ours ~theirs:Noop ?into branch let delete_branch branch = vcs := delete_branch !vcs branch let reset_branch branch id = vcs := reset_branch !vcs branch id let commit id t = vcs := commit !vcs id t let rewrite_merge id ~ours ~at branch = vcs := rewrite_merge !vcs id ~ours ~theirs:Noop ~at branch let reachable id = reachable !vcs id let mk_branch_name { expr = x } = Branch.make (match Vernacprop.under_control x with | VernacDefinition (_,({CAst.v=Name i},_),_) -> Id.to_string i | VernacStartTheoremProof (_,[({CAst.v=i},_),_]) -> Id.to_string i | _ -> "branch") let edit_branch = Branch.make "edit" let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind let get_info id = match get_info !vcs id with | Some x -> x | None -> raise Vcs_aux.Expired let set_state id s = let info = get_info id in info.state <- s; let is_full_state_valid = match s with | FullState _ -> true | EmptyState | ErrorState _ | ParsingState _ -> false in if async_proofs_is_master !cur_opt && is_full_state_valid then Hooks.(call state_ready ~doc:dummy_doc (* XXX should be taken in input *) id) let get_state id = (get_info id).state let get_parsing_state id = stm_pperr_endline (fun () -> str "retrieve parsing state state " ++ str (Stateid.to_strin match (get_info id).state with | FullState s -> Some s.Vernacstate.parsing | ParsingState s -> Some s | ErrorState (s,_) -> s | EmptyState -> None let set_parsing_state id ps = let info = get_info id in let new_state = match info.state with | FullState s -> assert false | ParsingState s -> assert false | ErrorState _ -> assert false | EmptyState -> ParsingState ps in info.state <- new_state let get_proof_mode id = (get_info id).proof_mode let set_proof_mode id pm = (get_info id).proof_mode <- pm let reached id = let info = get_info id in 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 ()) let proof_nesting () = Vcs_aux.proof_nesting !vcs let checkout_shallowest_proof_branch () = if List.mem edit_branch (Vcs_.branches !vcs) then begin checkout edit_branch end else let pl = proof_nesting () in try let branch = fst @@ Vcs_aux.find_proof_at_depth !vcs pl in checkout branch with Failure _ -> checkout Branch.master (* copies the transaction on every open branch *) let propagate_sideff ~action = List.map (fun b -> checkout b; let proof_mode = get_proof_mode @@ get_branch_pos b in let id = new_node proof_mode () in merge id ~ours:(Sideff action) ~into:b Branch.master; id) (List.filter (fun b -> not (Branch.equal b Branch.master)) (branches ())) let propagate_qed () = List.iter (fun b -> checkout b; let proof_mode = get_proof_mode @@ get_branch_pos b in let id = new_node proof_mode () in let parsing = Option.get @@ get_parsing_state (get_branch_pos b) in merge id ~ours:(Sideff CherryPickEnv) ~into:b Branch.master; set_parsing_state id parsing) (List.filter (fun b -> not (Branch.equal b Branch.master)) (branches ())) let visit id = Vcs_aux.visit !vcs id let nodes_in_slice ~block_start ~block_stop = let rec aux id = if Stateid.equal id block_start then [] else match visit id with | { next = n; step = `Cmd x } -> (id,Cmd x) :: aux n | { next = n; step = `Alias x } -> (id,Alias x) :: aux n | { next = n; step = `Sideff (ReplayCommand x,_) } -> (id,Sideff (ReplayCommand x)) :: aux n | _ -> anomaly Pp.(str("Cannot slice from "^ Stateid.to_string block_start ^ " 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 = let info = get_info id in Vcs_.set_info v id { info with state = EmptyState; vcs_backup = None,None } in let make_shallow = function | FullState st -> FullState (Vernacstate.make_shallow st) | x -> x in let copy_info_w_state v id = 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 = Stateid.Set.fold (fun n pl -> Vcs_.property_of !vcs n @ pl) nodes [] in let props = CList.sort_uniquize Vcs_.Dag.Property.compare props in List.fold_left (fun v p -> Vcs_.create_property v (Stateid.Set.elements (Vcs_.Dag.Property.having_it p)) (Vcs_.Dag.Property.data p)) v props in let v = Vcs_.empty block_start in let v = copy_info v block_start in let v = List.fold_right (fun (id,tr) v -> let v = Vcs_.commit v id tr in let v = copy_info v id in v) l v in (* Stm should have reached the beginning of proof *) assert (match get_state block_start with FullState _ -> true | _ -> false); (* We put in the new dag the most recent state known to master *) let rec fill id = match get_state id with | EmptyState | ErrorState _ | ParsingState _ -> fill (Vcs_aux.visit v id).next | FullState _ -> copy_info_w_state v id in let v = fill block_stop in (* We put in the new dag the first state (since Qed shall run on it, * see check_task_aux) *) let v = copy_info_w_state v block_start in copy_proof_blockes v let nodes_in_slice ~block_start ~block_stop = List.rev (List.map fst (nodes_in_slice ~block_start ~block_stop)) let topo_invariant l = let all = List.fold_right Stateid.Set.add l Stateid.Set.empty in List.for_all (fun x -> let props = property_of !vcs x in let sets = List.map Dag.Property.having_it props in List.for_all (fun s -> Stateid.Set.(subset s all || subset all s)) sets) l let create_proof_task_box l ~qed ~block_start:lemma = if not (topo_invariant l) then anomaly Pp.(str "overlapping boxes."); vcs := create_property !vcs l (ProofTask { qed; lemma }) let create_proof_block ({ block_start; block_stop} as decl) name = let l = nodes_in_slice ~block_start ~block_stop in if not (topo_invariant l) then anomaly Pp.(str "overlapping boxes."); vcs := create_property !vcs l (ProofBlock (decl, name)) let box_of id = List.map Dag.Property.data (property_of !vcs id) let delete_boxes_of id = List.iter (fun x -> vcs := delete_property !vcs x) (property_of !vcs id) let proof_task_box_of id = match CList.map_filter (function ProofTask x -> Some x | _ -> None) (box_of id) with | [] -> None | [x] -> Some x | _ -> anomaly Pp.(str "node with more than 1 proof task box.") let gc () = let old_vcs = !vcs in let new_vcs, erased_nodes = gc old_vcs in Stateid.Set.iter (fun id -> match (Vcs_aux.visit old_vcs id).step with | `Qed ({ fproof = Some (_, cancel_switch) }, _) | `Cmd { cqueue = `TacQueue (_,_,cancel_switch) } | `Cmd { cqueue = `QueryQueue cancel_switch } -> cancel_switch := true | _ -> ()) erased_nodes; vcs := new_vcs module NB : sig (* Non blocking Sys.command *) val command : now:bool -> (unit -> unit) -> unit end = struct let m = Mutex.create () let c = Condition.create () let job = ref None let worker = ref None let set_last_job j = Mutex.lock m; job := Some j; Condition.signal c; Mutex.unlock m let get_last_job () = Mutex.lock m; while Option.is_empty !job do Condition.wait c m; done; match !job with | None -> assert false | Some x -> job := None; Mutex.unlock m; x let run_command () = try while true do get_last_job () () done with e -> () (* No failure *) let command ~now job = if now then job () else begin set_last_job job; if Option.is_empty !worker then worker := Some (CThread.create run_command ()) end end let print ?(now=false) () = if !Flags.debug then NB.command ~now (print_dag !vcs) let backup () = !vcs let restore v = vcs := v end (* }}} *) let state_of_id ~doc id = try match VCS.get_state id with | FullState s -> `Valid (Some s) | ErrorState (_,(e,_)) -> `Error e | EmptyState | ParsingState _ -> `Valid None with VCS.Expired -> `Expired (****** 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. Warning: an optimization in installed_cached requires that state modifying functions are always executed using this wrapper. *) val define : doc:doc -> ?safe_id:Stateid.t -> ?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 install_parsing_state : Stateid.t -> unit *) 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 (* to send states across worker/master *) val get_cached : Stateid.t -> Vernacstate.t val same_env : Vernacstate.t -> Vernacstate.t -> bool type proof_part type partial_state = [ `Full of Vernacstate.t | `ProofOnly of Stateid.t * proof_part ] val proof_part_of_frozen : Vernacstate.t -> proof_part val assign : Stateid.t -> partial_state -> unit (* Handlers for initial state, prior to document creation. *) val register_root_state : unit -> unit val restore_root_state : unit -> unit 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 ~marshallabl let unfreeze st = Vernacstate.unfreeze_interp_state st.vernac_state; cur_id := st.id let invalidate_cur_state () = cur_id := Stateid.dummy type proof_part = Proof_global.t option * int * (* Evarutil.meta_counter_summary_tag *) int * (* Evd.evar_counter_summary_tag *) Obligations.program_info Names.Id.Map.t (* Obligations.program_tcc_summary_tag *) type partial_state = [ `Full of Vernacstate.t | `ProofOnly of Stateid.t * proof_part ] let proof_part_of_frozen { Vernacstate.proof; system } = let st = States.summary_of_state system in proof, Summary.project_from_summary st Util.(pi1 summary_pstate), Summary.project_from_summary st Util.(pi2 summary_pstate), Summary.project_from_summary st Util.(pi3 summary_pstate) let cache_state ~marshallable id = VCS.set_state id (FullState (Vernacstate.freeze_interp_state ~marshallable)) let freeze_invalid id iexn = let ps = VCS.get_parsing_state id in VCS.set_state id (ErrorState (ps,iexn)) let is_cached ?(cache=false) id only_valid = if Stateid.equal id !cur_id then try match VCS.get_info id with | ({ state = EmptyState } | { state = ParsingState _ }) when cache -> cache_state ~marshallable:fa | _ -> true with VCS.Expired -> false else try match VCS.get_state id with | EmptyState | ParsingState _ -> false | FullState _ -> true | ErrorState _ -> 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 = match VCS.get_state id with | FullState s -> Vernacstate.unfreeze_interp_state s; cur_id := id | ErrorState (_,ie) -> Exninfo.iraise ie | EmptyState | ParsingState _ -> (* coqc has a 1 slot cache and only for valid states *) if (VCS.is_interactive ()) || not (Stateid.equal id !cur_id) then anomaly Pp.(str "installing a non cached state.") (* let install_parsing_state id = if not (Stateid.equal id !cur_id) then begin Vernacstate.Parser.install @@ VCS.get_parsing_state id end *) let get_cached id = try match VCS.get_state id with | FullState s -> s | _ -> anomaly Pp.(str "not a cached state.") with VCS.Expired -> anomaly Pp.(str "not a cached state (expired).") let assign id what = let open Vernacstate in if VCS.get_state id <> EmptyState then () else try match what with | `Full s -> let s = try let prev = (VCS.visit id).next in if is_cached_and_valid prev then { s with proof = PG_compat.copy_terminators ~src:((get_cached prev).proof) ~tgt:s.proof } else s with VCS.Expired -> s in VCS.set_state id (FullState s) | `ProofOnly(ontop,(pstate,c1,c2,c3)) -> if is_cached_and_valid ontop then let s = get_cached ontop in let s = { s with proof = PG_compat.copy_terminators ~src:s.proof ~tgt:pstate } in let s = { s with system = States.replace_summary s.system begin let st = States.summary_of_state s.system in let st = Summary.modify_summary st Util.(pi1 summary_pstate) c1 in let st = Summary.modify_summary st Util.(pi2 summary_pstate) c2 in let st = Summary.modify_summary st Util.(pi3 summary_pstate) c3 in st end } in VCS.set_state id (FullState s) with VCS.Expired -> () let exn_on id ~valid (e, info) = match Stateid.get info with | Some _ -> (e, info) | None -> let loc = Loc.get_loc info in let (e, info) = Hooks.(call_process_error_once (e, info)) in execution_error ?loc id (iprint (e, info)); (e, Stateid.add info ~valid id) let same_env { Vernacstate.system = s1 } { Vernacstate.system = s2 } = let s1 = States.summary_of_state s1 in let e1 = Summary.project_from_summary s1 Global.global_env_summary_tag in let s2 = States.summary_of_state s2 in let e2 = Summary.project_from_summary s2 Global.global_env_summary_tag in e1 == e2 (* [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); let str_id = Stateid.to_string id in if is_cached id && not redefine then anomaly Pp.(str"defining state "++str str_id++str" twice."); try stm_prerr_endline (fun () -> "defining "^str_id^" (cache="^ 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 then cache_state ~marshallable:false id; stm_prerr_endline (fun () -> "setting cur id to "^str_id); cur_id := id; if feedback_processed then Hooks.(call state_computed ~doc id ~in_cache:false); VCS.reached id; if PG_compat.there_are_pending_proofs () then VCS.goals id (PG_compat.get_open_goals ()) with e -> let (e, info) = CErrors.push e in let good_id = !cur_id in invalidate_cur_state (); 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 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 ~marshallable:false) let restore_root_state () = cur_id := Stateid.dummy; 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 (* }}} *) (* indentation code for Show Script, initially contributed * by D. de Rauglaudre. Should be moved away. *) module ShowScript = struct let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) = (* ng1 : number of goals remaining at the current level (before cmd) ngl1 : stack of previous levels with their remaining goals ng : number of goals after the execution of cmd beginend : special indentation stack for { } *) let ngprev = List.fold_left (+) ng1 ngl1 in let new_ngl = if ng > ngprev then (* We've branched *) (ng - ngprev + 1, ng1 - 1 :: ngl1) else if ng < ngprev then (* A subgoal have been solved. Let's compute the new current level by discarding all levels with 0 remaining goals. *) let rec loop = function | (0, ng2::ngl2) -> loop (ng2,ngl2) | p -> p in loop (ng1-1, ngl1) else (* Standard case, same goal number as before *) (ng1, ngl1) in (* When a subgoal have been solved, separate this block by an empty line *) let new_nl = (ng < ngprev) in (* Indentation depth *) let ind = List.length ngl1 in (* Some special handling of bullets and { }, to get a nicer display *) let pred n = max 0 (n-1) in let ind, nl, new_beginend = match Vernacprop.under_control cmd with | VernacSubproof _ -> pred ind, nl, (pred ind)::beginend | VernacEndSubproof -> List.hd beginend, false, List.tl beginend | VernacBullet _ -> pred ind, nl, beginend | _ -> ind, nl, beginend in let pp = Pp.( (if nl then fnl () else mt ()) ++ (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd))) in (new_ngl, new_nl, new_beginend, pp :: ppl) let get_script prf = let branch, test = match prf with | None -> VCS.Branch.master, fun _ -> true | Some name -> VCS.current_branch (),fun nl -> nl=[] || List.mem name nl in let rec find acc id = if Stateid.equal id Stateid.initial || Stateid.equal id Stateid.dummy then acc else let view = VCS.visit id in match view.step with | `Fork((_,_,_,ns), _) when test ns -> acc | `Qed (qed, proof) -> find [qed.qast.expr, (VCS.get_info id).n_goals] proof | `Sideff (ReplayCommand x,_) -> find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next | `Sideff (CherryPickEnv, id) -> find acc id | `Cmd {cast = x; ctac} when ctac -> (* skip non-tactics *) find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next | `Cmd _ -> find acc view.next | `Alias (id,_) -> find acc id | `Fork _ -> find acc view.next in find [] (VCS.get_branch_pos branch) let warn_show_script_deprecated = CWarnings.create ~name:"deprecated-show-script" ~category:"deprecated" (fun () -> Pp.str "The “Show Script” command is deprecated.") let show_script ?proof () = warn_show_script_deprecated (); try let prf = try match proof with | None -> Some (PG_compat.get_current_proof_name ()) | Some (p,_) -> Some (p.Proof_global.id) with PG_compat.NoCurrentProof -> None in let cmds = get_script prf in let _,_,_,indented_cmds = List.fold_left indent_script_item ((1,[]),false,[],[]) cmds in let indented_cmds = List.rev (indented_cmds) in msg_notice Pp.(v 0 (prlist_with_sep fnl (fun x -> x) indented_cmds)) with Vcs_aux.Expired -> () 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 ?route id st { verbose; loc; expr } : Vernacstate.t = (* 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 *) set_id_for_feedback ?route dummy_doc id; Aux_file.record_in_aux_set_at ?loc (); (* We need to check if a command should be filtered from * vernac_entries, as it cannot handle it. This should go away in * future refactorings. *) let is_filtered_command = function | VernacResetName _ | VernacResetInitial | VernacBack _ | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _ | VernacAbortAll | VernacAbort _ -> true | _ -> false in let aux_interp st expr = (* XXX unsupported attributes *) let cmd = Vernacprop.under_control expr in if is_filtered_command cmd then (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st) else match cmd with | VernacShow ShowScript -> ShowScript.show_script (); st (* XX we are ignoring control here *) | _ -> stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr); try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st (CAst.make ?loc expr) with e -> let e = CErrors.push e in Exninfo.iraise Hooks.(call_process_error_once e) in aux_interp st expr (****************************** CRUFT *****************************************) (******************************************************************************) (* The backtrack module simulates the classic behavior of a linear document *) module Backtrack : sig val record : unit -> unit (* we could navigate the dag, but this ways easy *) val branches_of : Stateid.t -> backup (* Returns the state that the command should backtract to *) val undo_vernac_classifier : vernac_control -> doc:doc -> Stateid.t val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option end = struct (* {{{ *) let record () = List.iter (fun current_branch -> let mine = current_branch, VCS.get_branch current_branch in let info = VCS.get_info (VCS.get_branch_pos current_branch) in let others = CList.map_filter (fun b -> if Vcs_.Branch.equal b current_branch then None else Some(b, VCS.get_branch b)) (VCS.branches ()) in let backup = if fst info.vcs_backup <> None then fst info.vcs_backup else Some (VCS.backup ()) in let branches = if snd info.vcs_backup <> None then snd info.vcs_backup else Some { mine; others } in info.vcs_backup <- backup, branches) [VCS.current_branch (); VCS.Branch.master] let branches_of id = let info = VCS.get_info id in match info.vcs_backup with | _, None -> anomaly Pp.(str"Backtrack.branches_of "++str(Stateid.to_string id)++ str": a state with no vcs_backup.") | _, Some x -> x let rec fold_until f acc id = let next acc = if id = Stateid.initial then raise Not_found else fold_until f acc (VCS.visit id).next in let info = VCS.get_info id in match info.vcs_backup with | None, _ -> next acc | Some vcs, _ -> let ids, tactic, undo = if id = Stateid.initial || id = Stateid.dummy then [],false,0 else match VCS.visit id with | { step = `Fork ((_,_,_,l),_) } -> l, false,0 | { step = `Cmd { cids = l; ctac } } -> l, ctac,0 | { step = `Alias (_,{ expr }) } when not (Vernacprop.has_Fail expr) -> begin match Vernacprop.under_control expr with | VernacUndo n -> [], false, n | _ -> [],false,0 end | _ -> [],false,0 in match f acc (id, vcs, ids, tactic, undo) with | `Stop x -> x | `Cont acc -> next acc let undo_costly_in_batch_mode = CWarnings.create ~name:"undo-batch-mode" ~category:"non-interactive" Pp.(fun v -> str "Command " ++ Ppvernac.pr_vernac v ++ str (" is not recommended in batch mode. In particular, going back in the documen " is not efficient in batch mode due to Coq not caching previous states for memo " If your use is intentional, you may want to disable this warning and pass" ^ " the \"-async-proofs-cache force\" option to Coq.")) let back_tactic 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) let get_proof ~doc id = match state_of_id ~doc id with | `Valid (Some vstate) -> Option.map Proof_global.give_me_the_proof vstate.Vernacstate.p | _ -> None let undo_vernac_classifier v ~doc = 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 | VernacResetInitial -> Stateid.initial | VernacResetName {CAst.v=name} -> let id = VCS.cur_tip () in (try let oid = fold_until (fun b (id,_,label,_,_) -> if b then `Stop id else `Cont (List.mem name label)) false id in oid with Not_found -> id) | VernacBack n -> let id = VCS.cur_tip () in let oid = fold_until (fun n (id,_,_,_,_) -> if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in oid | VernacUndo n -> let id = VCS.cur_tip () in let oid = fold_until back_tactic n id in oid | VernacUndoTo _ | VernacRestart as e -> let m = match e with VernacUndoTo m -> m | _ -> 0 in let id = VCS.cur_tip () in let vcs = match (VCS.get_info id).vcs_backup with | None, _ -> anomaly Pp.(str"Backtrack: tip with no vcs_backup.") | Some vcs, _ -> vcs in let cb, _ = try Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs) with Failure _ -> raise PG_compat.NoCurrentProof in let n = fold_until (fun n (_,vcs,_,_,_) -> if List.mem cb (Vcs_.branches vcs) then `Cont (n+1) else `Stop n) 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 oid | VernacAbortAll -> let id = VCS.cur_tip () in let oid = fold_until (fun () (id,vcs,_,_,_) -> match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ()) () id in oid | VernacBackTo id -> Stateid.of_int id | _ -> anomaly Pp.(str "incorrect VtMeta classification") with | Not_found -> CErrors.user_err ~hdr:"undo_vernac_classifier" Pp.(str "Cannot undo") let get_prev_proof ~doc id = try let np = get_proof ~doc id in match np with | None -> None | Some cp -> let did = ref id in let rv = ref np in let done_ = ref false in while not !done_ do did := fold_until back_tactic 1 !did; rv := get_proof ~doc !did; done_ := match !rv with | Some rv -> not (Goal.Set.equal (Proof.all_goals rv) (Proof.all_goals cp)) | None -> true done; !rv with Not_found | PG_compat.NoCurrentProof -> None end (* }}} *) let get_prev_proof = Backtrack.get_prev_proof let hints = ref Aux_file.empty_aux_file let set_compilation_hints file = hints := Aux_file.load_aux_file_for file let get_hint_ctx loc = let s = Aux_file.get ?loc !hints "context_used" in let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") s) in let ids = List.map (fun id -> CAst.make id) ids in match ids with | [] -> SsEmpty | x :: xs -> List.fold_left (fun a x -> SsUnion (SsSingl x,a)) (SsSingl x) xs let get_hint_bp_time proof_name = try float_of_string (Aux_file.get !hints proof_name) with Not_found -> 1.0 let record_pb_time ?loc proof_name time = let proof_build_time = Printf.sprintf "%.3f" time in Aux_file.record_in_aux_at ?loc "proof_build_time" proof_build_time; if proof_name <> "" then begin Aux_file.record_in_aux_at proof_name proof_build_time; hints := Aux_file.set !hints proof_name proof_build_time end exception RemoteException of Pp.t let _ = CErrors.register_handler (function | RemoteException ppcmd -> ppcmd | _ -> raise Unhandled) (****************** proof structure for error recovery ************************) (******************************************************************************) type document_node = { indentation : int; ast : Vernacexpr.vernac_control; id : Stateid.t; } type document_view = { entry_point : document_node; prev_node : document_node -> document_node option; } type static_block_detection = document_view -> static_block_declaration option type recovery_action = { base_state : Stateid.t; goals_to_admit : Goal.goal list; recovery_command : Vernacexpr.vernac_control option; } type dynamic_block_error_recovery = doc -> static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ] let proof_block_delimiters = ref [] let register_proof_block_delimiter name static dynamic = if List.mem_assoc name !proof_block_delimiters then CErrors.user_err ~hdr:"STM" Pp.(str "Duplicate block delimiter " ++ str name); proof_block_delimiters := (name, (static,dynamic)) :: !proof_block_delimiters let mk_doc_node id = function | { step = `Cmd { ctac; cast = { indentation; expr }}; next } when ctac -> Some { indentation; ast = expr; id } | { step = `Sideff (ReplayCommand { indentation; expr }, _); next } -> Some { indentation; ast = expr; id } | _ -> None let prev_node { id } = let id = (VCS.visit id).next in mk_doc_node id (VCS.visit id) let cur_node id = mk_doc_node id (VCS.visit id) let is_block_name_enabled name = match !cur_opt.async_proofs_tac_error_resilience with | `None -> false | `All -> true | `Only l -> List.mem name l let detect_proof_block id name = let name = match name with None -> "indent" | Some x -> x in if is_block_name_enabled name && (async_proofs_is_master !cur_opt || Flags.async_proofs_is_worker ()) then ( match cur_node id with | None -> () | Some entry_point -> try let static, _ = List.assoc name !proof_block_delimiters in begin match static { prev_node; entry_point } with | None -> () | Some ({ block_start; block_stop } as decl) -> VCS.create_proof_block decl name end with Not_found -> CErrors.user_err ~hdr:"STM" Pp.(str "Unknown proof block delimiter " ++ str name) ) (****************************** THE SCHEDULER *********************************) (******************************************************************************) (* Unused module warning doesn't understand [module rec] *) [@@@ocaml.warning "-60"] module rec ProofTask : sig type competence = Stateid.t list type task_build_proof = { t_exn_info : Stateid.t * Stateid.t; t_start : Stateid.t; t_stop : Stateid.t; t_drop : bool; t_states : competence; t_assign : Proof_global.closed_proof_output Future.assignment -> unit; t_loc : Loc.t option; t_uuid : Future.UUID.t; t_name : string } type task = | BuildProof of task_build_proof | States of Stateid.t list type request = | ReqBuildProof of (Future.UUID.t,VCS.vcs) Stateid.request * bool * competence | ReqStates of Stateid.t list include AsyncTaskQueue.Task with type task := task and type competence := competence and type request := request val build_proof_here : doc:doc -> ?loc:Loc.t -> drop_pt:bool -> Stateid.t * Stateid.t -> Stateid.t -> Proof_global.closed_proof_output Future.computation (* If set, only tasks overlapping with this list are processed *) val set_perspective : Stateid.t list -> unit end = struct (* {{{ *) let forward_feedback msg = Hooks.(call forward_feedback msg) type competence = Stateid.t list type task_build_proof = { t_exn_info : Stateid.t * Stateid.t; t_start : Stateid.t; t_stop : Stateid.t; t_drop : bool; t_states : competence; t_assign : Proof_global.closed_proof_output Future.assignment -> unit; t_loc : Loc.t option; t_uuid : Future.UUID.t; t_name : string } type task = | BuildProof of task_build_proof | States of Stateid.t list type worker_status = Fresh | Old of competence type request = | ReqBuildProof of (Future.UUID.t,VCS.vcs) Stateid.request * bool * competence | ReqStates of Stateid.t list type error = { e_error_at : Stateid.t; e_safe_id : Stateid.t; e_msg : Pp.t; e_safe_states : Stateid.t list } type response = | RespBuiltProof of Proof_global.closed_proof_output * float | RespError of error | RespStates of (Stateid.t * State.partial_state) list let name = ref "proofworker" let extra_env () = !async_proofs_workers_extra_env let perspective = ref [] let set_perspective l = perspective := l let is_inside_perspective st = true (* This code is now disabled. If an IDE needs this feature, make it accessible again. List.exists (fun x -> CList.mem_f Stateid.equal x !perspective) st *) let task_match age t = match age, t with | Fresh, BuildProof { t_states } -> is_inside_perspective t_states | Old my_states, States l -> List.for_all (fun x -> CList.mem_f Stateid.equal x my_states) l | _ -> false let name_of_task = function | BuildProof t -> "proof: " ^ t.t_name | States l -> "states: " ^ String.concat "," (List.map Stateid.to_string l) let name_of_request = function | ReqBuildProof(r,_,_) -> "proof: " ^ r.Stateid.name | ReqStates l -> "states: "^String.concat "," (List.map Stateid.to_string l) let request_of_task age = function | States l -> Some (ReqStates l) | BuildProof { t_exn_info;t_start;t_stop;t_loc;t_uuid;t_name;t_states;t_drop } -> assert(age = Fresh); try Some (ReqBuildProof ({ Stateid.exn_info = t_exn_info; stop = t_stop; document = VCS.slice ~block_start:t_start ~block_stop:t_stop; loc = t_loc; uuid = t_uuid; name = t_name }, t_drop, t_states)) with VCS.Expired -> None let use_response (s : worker_status) t r = match s, t, r with | Old c, States _, RespStates l -> List.iter (fun (id,s) -> State.assign id s) l; `End | Fresh, BuildProof { t_assign; t_loc; t_name; t_states; t_drop }, RespBuiltProof (pl, time) -> feedback (InProgress ~-1); t_assign (`Val pl); record_pb_time ?loc:t_loc t_name time; if t_drop then `Stay(t_states,[States t_states]) else `End | Fresh, BuildProof { t_assign; t_loc; t_name; t_states }, RespError { e_error_at; e_safe_id = valid; e_msg; e_safe_states } -> feedback (InProgress ~-1); let info = Stateid.add ~valid Exninfo.null e_error_at in let e = (RemoteException e_msg, info) in t_assign (`Exn e); `Stay(t_states,[States e_safe_states]) | _ -> assert false let on_task_cancellation_or_expiration_or_slave_death = function | None -> () | Some (States _) -> () | Some (BuildProof { t_start = start; t_assign }) -> let s = "Worker dies or task expired" in let info = Stateid.add ~valid:start Exninfo.null start in let e = (RemoteException (Pp.strbrk s), info) in t_assign (`Exn e); execution_error start (Pp.strbrk s); feedback (InProgress ~-1) 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 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)); let p = PG_compat.return_proof ~allow_partial:drop_pt () in if drop_pt then feedback ~id Complete; p) let perform_buildp { Stateid.exn_info; stop; document; loc } drop my_states = try VCS.restore document; VCS.print (); let proof, future_proof, time = let wall_clock = Unix.gettimeofday () in let fp = build_proof_here ~doc:dummy_doc (* XXX should be document *) ?loc ~drop_pt:drop exn_ let proof = Future.force fp in proof, fp, Unix.gettimeofday () -. wall_clock in (* We typecheck the proof with the kernel (in the worker) to spot * 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 = 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 *) State.unfreeze st; let pobject, _ = PG_compat.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 ~marshallable:false in stm_vernac_interp stop ~proof:(pobject, terminator) st { verbose = false; loc; indentation = 0; strlen = 0; expr = VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in ignore(Future.join checked_proof); end; (* STATE: Restore the state XXX: handle exn *) State.unfreeze st; RespBuiltProof(proof,time) with | e when CErrors.noncritical e || e = Stack_overflow -> let (e, info) = CErrors.push e in (* This can happen if the proof is broken. The error has also been * signalled as a feedback, hence we can silently recover *) let e_error_at, e_safe_id = match Stateid.get info with | Some (safe, err) -> err, safe | None -> Stateid.dummy, Stateid.dummy in let e_msg = iprint (e, info) in stm_pperr_endline Pp.(fun () -> str "failed with the following exception: " ++ fnl () ++ e_ 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 = if query = [] then [] else let is_tac e = match Vernac_classifier.classify_vernac e with | VtProofStep _, _ -> true | _ -> false in let initial = let rec aux id = try match VCS.visit id with { next } -> aux next with VCS.Expired -> id in aux (List.hd query) in let get_state seen id = let prev = try let { next = prev; step } = VCS.visit id in 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_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 when is_tac expr && State.same_env o n -> (* A pure tactic *) Some (id, `ProofOnly (prev, State.proof_part_of_frozen n)) | Some _, Some s -> if !Flags.debug then msg_debug (Pp.str "STM: sending back a fat state"); Some (id, `Full s) | _, Some s -> Some (id, `Full s) in let rec aux seen = function | [] -> [] | id :: rest -> match get_state seen id with | None -> aux seen rest | Some stuff -> stuff :: aux (id :: seen) rest in aux [initial] query let perform = function | ReqBuildProof (bp,drop,states) -> perform_buildp bp drop states | ReqStates sl -> RespStates (perform_states sl) let on_marshal_error s = function | States _ -> msg_warning Pp.(strbrk("Marshalling error: "^s^". "^ "The system state could not be sent to the master process.")) | BuildProof { t_exn_info; t_stop; t_assign; t_loc; t_drop = drop_pt } -> msg_warning Pp.(strbrk("Marshalling error: "^s^". "^ "The system state could not be sent to the worker process. "^ "Falling back to local, lazy, evaluation.")); t_assign(`Comp(build_proof_here ~doc:dummy_doc (* XXX should be stored in a closure, it is t feedback (InProgress ~-1) end (* }}} *) (* Slave processes (if initialized, otherwise local lazy evaluation) *) and Slaves : sig (* (eventually) remote calls *) val build_proof : doc:doc -> ?loc:Loc.t -> drop_pt:bool -> exn_info:(Stateid.t * Stateid.t) -> block_start:Stateid.t -> block_stop:Stateid.t -> name:string -> future_proof * AsyncTaskQueue.cancel_switch (* blocking function that waits for the task queue to be empty *) val wait_all_done : unit -> unit (* initialize the whole machinery (optional) *) val init : unit -> unit type 'a tasks = (('a,VCS.vcs) Stateid.request * bool) list val dump_snapshot : unit -> Future.UUID.t tasks val check_task : string -> int tasks -> int -> bool val info_tasks : 'a tasks -> (string * float * int) list val finish_task : string -> Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs -> int tasks -> int -> Library.seg_univ val cancel_worker : WorkerPool.worker_id -> unit val reset_task_queue : unit -> unit val set_perspective : Stateid.t list -> unit end = struct (* {{{ *) module TaskQueue = AsyncTaskQueue.MakeQueue(ProofTask) () let queue = ref None let init () = if async_proofs_is_master !cur_opt then queue := Some (TaskQueue.create !cur_opt.async_proofs_n_workers) else queue := Some (TaskQueue.create 0) let check_task_aux extra name l i = let { Stateid.stop; document; loc; name = r_name }, drop = List.nth l i in Flags.if_verbose msg_info Pp.(str(Printf.sprintf "Checking task %d (%s%s) of %s" i r_name extra name)); VCS.restore document; let start = let rec aux cur = try aux (VCS.visit cur).next with VCS.Expired -> cur in aux stop in try Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:false stop; if drop then let _proof = PG_compat.return_proof ~allow_partial:true () in `OK_ADMITTED else begin (* The original terminator, a hook, has not been saved in the .vio*) PG_compat.set_terminator (Lemmas.standard_proof_terminator []); let opaque = Proof_global.Opaque in let proof = PG_compat.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: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 ~marshallable:false in ignore(stm_vernac_interp stop ~proof st { verbose = false; loc; indentation = 0; strlen = 0; expr = VernacExpr ([], VernacEndProof (Proved (opaque,None))) }); `OK proof end with e -> let (e, info) = CErrors.push e in (try match Stateid.get info with | None -> msg_warning Pp.( str"File " ++ str name ++ str ": proof of " ++ str r_name ++ spc () ++ iprint (e, info)) | Some (_, cur) -> match VCS.visit cur with | { step = `Cmd { cast = { loc } } } | { step = `Fork (( { loc }, _, _, _), _) } | { step = `Qed ( { qast = { loc } }, _) } | { step = `Sideff (ReplayCommand { loc }, _) } -> let start, stop = Option.cata Loc.unloc (0,0) loc in msg_warning Pp.( str"File " ++ str name ++ str ": proof of " ++ str r_name ++ --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 1.76 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
