|
(************************************************************************)
(* * 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_string id) ++ str " }}}");
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 ~marshallable:false }
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:false id; true
| _ -> 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 document" ^
" is not efficient in batch mode due to Coq not caching previous states for memory optimization reasons." ^
" 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.proof
| _ -> 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_info stop in
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_msg);
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 the same doc that was used to generate the task *) ?loc:t_loc ~drop_pt t_exn_info t_stop));
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
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen1.56Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
