From 8330f5cfd6a332df10fc806b0c0bdab6e0abe8e7 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 25 Apr 2014 19:46:30 +0200 Subject: Adding a stm/ folder, as asked during last workgroup. It was essentially moving files around. A bunch of files from lib/ that were only used in the STM were moved, as well as part of toplevel/ related to the STM. --- Makefile.build | 3 +- Makefile.common | 8 +- lib/dag.ml | 134 --- lib/dag.mli | 52 - lib/lib.mllib | 5 - lib/spawned.ml | 84 -- lib/spawned.mli | 22 - lib/tQueue.ml | 64 -- lib/tQueue.mli | 17 - lib/vcs.ml | 193 ---- lib/vcs.mli | 90 -- lib/workerPool.ml | 73 -- lib/workerPool.mli | 30 - myocamlbuild.ml | 3 +- stm/dag.ml | 134 +++ stm/dag.mli | 52 + stm/lemmas.ml | 431 +++++++++ stm/lemmas.mli | 50 + stm/spawned.ml | 84 ++ stm/spawned.mli | 22 + stm/stm.ml | 2075 ++++++++++++++++++++++++++++++++++++++++ stm/stm.mli | 85 ++ stm/stm.mllib | 9 + stm/tQueue.ml | 64 ++ stm/tQueue.mli | 17 + stm/vcs.ml | 193 ++++ stm/vcs.mli | 90 ++ stm/vernac_classifier.ml | 189 ++++ stm/vernac_classifier.mli | 27 + stm/vi_checking.ml | 152 +++ stm/vi_checking.mli | 13 + stm/workerPool.ml | 73 ++ stm/workerPool.mli | 30 + toplevel/lemmas.ml | 431 --------- toplevel/lemmas.mli | 50 - toplevel/stm.ml | 2072 --------------------------------------- toplevel/stm.mli | 80 -- toplevel/toplevel.mllib | 4 - toplevel/vernac_classifier.ml | 189 ---- toplevel/vernac_classifier.mli | 27 - toplevel/vernacentries.ml | 7 +- toplevel/vernacentries.mli | 1 - toplevel/vi_checking.ml | 152 --- toplevel/vi_checking.mli | 13 - 44 files changed, 3802 insertions(+), 3792 deletions(-) delete mode 100644 lib/dag.ml delete mode 100644 lib/dag.mli delete mode 100644 lib/spawned.ml delete mode 100644 lib/spawned.mli delete mode 100644 lib/tQueue.ml delete mode 100644 lib/tQueue.mli delete mode 100644 lib/vcs.ml delete mode 100644 lib/vcs.mli delete mode 100644 lib/workerPool.ml delete mode 100644 lib/workerPool.mli create mode 100644 stm/dag.ml create mode 100644 stm/dag.mli create mode 100644 stm/lemmas.ml create mode 100644 stm/lemmas.mli create mode 100644 stm/spawned.ml create mode 100644 stm/spawned.mli create mode 100644 stm/stm.ml create mode 100644 stm/stm.mli create mode 100644 stm/stm.mllib create mode 100644 stm/tQueue.ml create mode 100644 stm/tQueue.mli create mode 100644 stm/vcs.ml create mode 100644 stm/vcs.mli create mode 100644 stm/vernac_classifier.ml create mode 100644 stm/vernac_classifier.mli create mode 100644 stm/vi_checking.ml create mode 100644 stm/vi_checking.mli create mode 100644 stm/workerPool.ml create mode 100644 stm/workerPool.mli delete mode 100644 toplevel/lemmas.ml delete mode 100644 toplevel/lemmas.mli delete mode 100644 toplevel/stm.ml delete mode 100644 toplevel/stm.mli delete mode 100644 toplevel/vernac_classifier.ml delete mode 100644 toplevel/vernac_classifier.mli delete mode 100644 toplevel/vi_checking.ml delete mode 100644 toplevel/vi_checking.mli diff --git a/Makefile.build b/Makefile.build index 91817a94a7..dd7b20f0fe 100644 --- a/Makefile.build +++ b/Makefile.build @@ -388,7 +388,7 @@ test-suite: world $(ALLSTDLIB).v ################################################################## .PHONY: lib kernel byterun library proofs tactics interp parsing pretyping -.PHONY: highparsing toplevel hightactics +.PHONY: highparsing stm toplevel hightactics lib: lib/clib.cma lib/lib.cma kernel: kernel/kernel.cma @@ -400,6 +400,7 @@ interp: interp/interp.cma parsing: parsing/parsing.cma pretyping: pretyping/pretyping.cma highparsing: parsing/highparsing.cma +stm: stm/stm.cma toplevel: toplevel/toplevel.cma hightactics: tactics/hightactics.cma diff --git a/Makefile.common b/Makefile.common index 7425d99af8..d45c1d5614 100644 --- a/Makefile.common +++ b/Makefile.common @@ -61,8 +61,8 @@ CSDPCERT:=plugins/micromega/csdpcert$(EXE) CORESRCDIRS:=\ config lib kernel kernel/byterun library \ - proofs tactics pretyping interp toplevel \ - parsing printing grammar intf + proofs tactics pretyping interp stm \ + toplevel parsing printing grammar intf PLUGINS:=\ omega romega micromega quote \ @@ -157,7 +157,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \ CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ parsing/parsing.cma printing/printing.cma tactics/tactics.cma \ - toplevel/toplevel.cma parsing/highparsing.cma tactics/hightactics.cma + stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma tactics/hightactics.cma GRAMMARCMA:=tools/compat5.cmo grammar/grammar.cma @@ -354,7 +354,7 @@ OCAMLDOCDIR=dev/ocamldoc DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \ ./pretyping/*.mli ./interp/*.mli printing/*.mli \ ./parsing/*.mli ./proofs/*.mli \ - ./tactics/*.mli ./toplevel/*.mli) + ./tactics/*.mli ./stm/*.mli ./toplevel/*.mli) # Defining options to generate dependencies graphs DOT=dot diff --git a/lib/dag.ml b/lib/dag.ml deleted file mode 100644 index 9622f4c1fa..0000000000 --- a/lib/dag.ml +++ /dev/null @@ -1,134 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 'd t -> bool - val compare : 'd t -> 'd t -> int - val to_string : 'd t -> string - val data : 'd t -> 'd - end - - type node - module NodeSet : Set.S with type elt = node - - type ('edge,'info,'cdata) t - - val empty : ('e,'i,'d) t - - val add_edge : ('e,'i,'d) t -> node -> 'e -> node -> ('e,'i,'d) t - val from_node : ('e,'i,'d) t -> node -> (node * 'e) list - val mem : ('e,'i,'d) t -> node -> bool - val del_edge : ('e,'i,'d) t -> node -> node -> ('e,'i,'d) t - val del_nodes : ('e,'i,'d) t -> NodeSet.t -> ('e,'i,'d) t - val all_nodes : ('e,'i,'d) t -> NodeSet.t - - val iter : ('e,'i,'d) t -> - (node -> 'd Cluster.t option -> 'i option -> - (node * 'e) list -> unit) -> unit - - val create_cluster : ('e,'i,'d) t -> node list -> 'd -> ('e,'i,'d) t - val cluster_of : ('e,'i,'d) t -> node -> 'd Cluster.t option - val del_cluster : ('e,'i,'d) t -> 'd Cluster.t -> ('e,'i,'d) t - - val get_info : ('e,'i,'d) t -> node -> 'i option - val set_info : ('e,'i,'d) t -> node -> 'i -> ('e,'i,'d) t - val clear_info : ('e,'i,'d) t -> node -> ('e,'i,'d) t - -end - -module Make(OT : Map.OrderedType) = struct - -module Cluster = -struct - type 'd t = 'd * int - let equal (_,i1) (_,i2) = Int.equal i1 i2 - let compare (_,i1) (_,i2) = Int.compare i1 i2 - let to_string (_,i) = string_of_int i - let data (d,_) = d -end - -type node = OT.t - -module NodeMap = CMap.Make(OT) -module NodeSet = Set.Make(OT) - -type ('edge,'info,'data) t = { - graph : (node * 'edge) list NodeMap.t; - clusters : 'data Cluster.t NodeMap.t; - infos : 'info NodeMap.t; -} - -let empty = { - graph = NodeMap.empty; - clusters = NodeMap.empty; - infos = NodeMap.empty; -} - -let mem { graph } id = NodeMap.mem id graph - -let add_edge dag from trans dest = { dag with - graph = - try NodeMap.modify from (fun _ arcs -> (dest, trans) :: arcs) dag.graph - with Not_found -> NodeMap.add from [dest, trans] dag.graph } - -let from_node { graph } id = NodeMap.find id graph - -let del_edge dag id tgt = { dag with - graph = - try - let modify _ arcs = - let filter (d, _) = OT.compare d tgt <> 0 in - List.filter filter arcs - in - NodeMap.modify id modify dag.graph - with Not_found -> dag.graph } - -let del_nodes dag s = { - infos = NodeMap.filter (fun n _ -> not(NodeSet.mem n s)) dag.infos; - clusters = NodeMap.filter (fun n _ -> not(NodeSet.mem n s)) dag.clusters; - graph = NodeMap.filter (fun n l -> - let drop = NodeSet.mem n s in - if not drop then - assert(List.for_all (fun (n',_) -> not(NodeSet.mem n' s)) l); - not drop) - dag.graph } - -let clid = ref 1 -let create_cluster dag l data = - incr clid; - { dag with clusters = - List.fold_right (fun x clusters -> - NodeMap.add x (data, !clid) clusters) l dag.clusters } - -let cluster_of dag id = - try Some (NodeMap.find id dag.clusters) - with Not_found -> None - -let del_cluster dag c = - { dag with clusters = - NodeMap.filter (fun _ c' -> not (Cluster.equal c' c)) dag.clusters } - -let get_info dag id = - try Some (NodeMap.find id dag.infos) - with Not_found -> None - -let set_info dag id info = { dag with infos = NodeMap.add id info dag.infos } - -let clear_info dag id = { dag with infos = NodeMap.remove id dag.infos } - -let iter dag f = - NodeMap.iter (fun k v -> f k (cluster_of dag k) (get_info dag k) v) dag.graph - -let all_nodes dag = NodeMap.domain dag.graph - -end - diff --git a/lib/dag.mli b/lib/dag.mli deleted file mode 100644 index 702ccd80f8..0000000000 --- a/lib/dag.mli +++ /dev/null @@ -1,52 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 'd t -> bool - val compare : 'd t -> 'd t -> int - val to_string : 'd t -> string - val data : 'd t -> 'd - end - - type node - module NodeSet : Set.S with type elt = node - - type ('edge,'info,'cdata) t - - val empty : ('e,'i,'d) t - - val add_edge : ('e,'i,'d) t -> node -> 'e -> node -> ('e,'i,'d) t - val from_node : ('e,'i,'d) t -> node -> (node * 'e) list - val mem : ('e,'i,'d) t -> node -> bool - val del_edge : ('e,'i,'d) t -> node -> node -> ('e,'i,'d) t - val del_nodes : ('e,'i,'d) t -> NodeSet.t -> ('e,'i,'d) t - val all_nodes : ('e,'i,'d) t -> NodeSet.t - - val iter : ('e,'i,'d) t -> - (node -> 'd Cluster.t option -> 'i option -> - (node * 'e) list -> unit) -> unit - - val create_cluster : ('e,'i,'d) t -> node list -> 'd -> ('e,'i,'d) t - val cluster_of : ('e,'i,'d) t -> node -> 'd Cluster.t option - val del_cluster : ('e,'i,'d) t -> 'd Cluster.t -> ('e,'i,'d) t - - val get_info : ('e,'i,'d) t -> node -> 'i option - val set_info : ('e,'i,'d) t -> node -> 'i -> ('e,'i,'d) t - val clear_info : ('e,'i,'d) t -> node -> ('e,'i,'d) t - -end - -module Make(OT : Map.OrderedType) : S with type node = OT.t - diff --git a/lib/lib.mllib b/lib/lib.mllib index 50621df20d..edef3da037 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -10,7 +10,6 @@ Unicode System CThread Spawn -Spawned Trie Profile Explore @@ -23,7 +22,3 @@ Genarg Ephemeron Future RemoteCounter -Dag -Vcs -TQueue -WorkerPool diff --git a/lib/spawned.ml b/lib/spawned.ml deleted file mode 100644 index d025945690..0000000000 --- a/lib/spawned.ml +++ /dev/null @@ -1,84 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - prerr_endline (Printf.sprintf "Handshake with %d OK" pid); - output_value cout (Hello (proto_version,Unix.getpid ())); flush cout - | _ -> raise (Failure "handshake protocol") - with - | Failure s | Invalid_argument s | Sys_error s -> - pr_err ("Handshake failed: " ^ s); raise (Failure "handshake") - | End_of_file -> - pr_err "Handshake failed: End_of_file"; raise (Failure "handshake") - -let open_bin_connection h p = - let open Unix in - let cin, cout = open_connection (ADDR_INET (inet_addr_of_string h,p)) in - set_binary_mode_in cin true; - set_binary_mode_out cout true; - cin, cout - -let controller h p = - prerr_endline "starting controller thread"; - let main () = - let ic, oc = open_bin_connection h p in - let rec loop () = - try - match input_value ic with - | Hello _ -> prerr_endline "internal protocol error"; exit 1 - | ReqDie -> prerr_endline "death sentence received"; exit 0 - | ReqStats -> - output_value oc (RespStats (Gc.stat ())); flush oc; loop () - with - | e -> - prerr_endline ("control channel broken: " ^ Printexc.to_string e); - exit 1 in - loop () in - ignore(Thread.create main ()) - -let main_channel = ref None -let control_channel = ref None - -let channels = ref None - -let init_channels () = - if !channels <> None then Errors.anomaly(Pp.str "init_channels called twice"); - let () = match !main_channel with - | None -> () - | Some (Socket(mh,mp)) -> - channels := Some (open_bin_connection mh mp); - | Some AnonPipe -> - let stdin = Unix.in_channel_of_descr (Unix.dup Unix.stdin) in - let stdout = Unix.out_channel_of_descr (Unix.dup Unix.stdout) in - Unix.dup2 Unix.stderr Unix.stdout; - set_binary_mode_in stdin true; - set_binary_mode_out stdout true; - channels := Some (stdin, stdout); - in - match !control_channel with - | None -> () - | Some (Socket (ch, cp)) -> - controller ch cp - | Some AnonPipe -> - Errors.anomaly (Pp.str "control channel cannot be a pipe") - -let get_channels () = - match !channels with - | None -> Errors.anomaly(Pp.str "init_channels not called") - | Some(ic, oc) -> ic, oc - diff --git a/lib/spawned.mli b/lib/spawned.mli deleted file mode 100644 index 18b88dc64b..0000000000 --- a/lib/spawned.mli +++ /dev/null @@ -1,22 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit - -(* Once initialized, these are the channels to talk with our master *) -val get_channels : unit -> in_channel * out_channel - diff --git a/lib/tQueue.ml b/lib/tQueue.ml deleted file mode 100644 index 783c545fd0..0000000000 --- a/lib/tQueue.ml +++ /dev/null @@ -1,64 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Queue.push x tq.queue) (List.sort rel !l); - Mutex.unlock tq.lock diff --git a/lib/tQueue.mli b/lib/tQueue.mli deleted file mode 100644 index a3ea5532fc..0000000000 --- a/lib/tQueue.mli +++ /dev/null @@ -1,17 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 'a t -val pop : 'a t -> 'a -val push : 'a t -> 'a -> unit -val reorder : 'a t -> ('a -> 'a -> int) -> unit -val wait_until_n_are_waiting_and_queue_empty : int -> 'a t -> unit -val dump : 'a t -> 'a list diff --git a/lib/vcs.ml b/lib/vcs.ml deleted file mode 100644 index e2513b1c1e..0000000000 --- a/lib/vcs.ml +++ /dev/null @@ -1,193 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* t - val equal : t -> t -> bool - val compare : t -> t -> int - val to_string : t -> string - val master : t - end - - type id - - (* Branches have [branch_info] attached to them. *) - type ('kind) branch_info = { - kind : [> `Master] as 'kind; - root : id; - pos : id; - } - - type ('kind,'diff,'info) t constraint 'kind = [> `Master ] - - val empty : id -> ('kind,'diff,'info) t - - val current_branch : ('k,'e,'i) t -> Branch.t - val branches : ('k,'e,'i) t -> Branch.t list - - val get_branch : ('k,'e,'i) t -> Branch.t -> 'k branch_info - val reset_branch : ('k,'e,'i) t -> Branch.t -> id -> ('k,'e,'i) t - val branch : - ('kind,'e,'i) t -> ?root:id -> ?pos:id -> - Branch.t -> 'kind -> ('kind,'e,'i) t - val delete_branch : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t - val merge : - ('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> ?into:Branch.t -> - Branch.t -> ('k,'diff,'i) t - val commit : ('k,'diff,'i) t -> id -> 'diff -> ('k,'diff,'i) t - val rewrite_merge : - ('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> at:id -> - Branch.t -> ('k,'diff,'i) t - val checkout : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t - - val set_info : ('k,'e,'info) t -> id -> 'info -> ('k,'e,'info) t - val get_info : ('k,'e,'info) t -> id -> 'info option - - module NodeSet : Set.S with type elt = id - - val gc : ('k,'e,'info) t -> ('k,'e,'info) t * NodeSet.t - - val reachable : ('k,'e,'info) t -> id -> NodeSet.t - - module Dag : Dag.S with type node = id - val dag : ('kind,'diff,'info) t -> ('diff,'info,id) Dag.t - - val create_cluster : ('k,'e,'i) t -> id list -> id -> ('k,'e,'i) t - val cluster_of : ('k,'e,'i) t -> id -> id Dag.Cluster.t option - val delete_cluster : ('k,'e,'i) t -> id Dag.Cluster.t -> ('k,'e,'i) t - -end - -module Make(OT : Map.OrderedType) = struct - -module Dag = Dag.Make(OT) - -type id = OT.t - -module NodeSet = Dag.NodeSet - - -module Branch = -struct - type t = string - let make = - let bid = ref 0 in - fun s -> incr bid; string_of_int !bid ^ "_" ^ s - let equal = CString.equal - let compare = CString.compare - let to_string s = s - let master = "master" -end - -module BranchMap = Map.Make(Branch) - -type 'kind branch_info = { - kind : [> `Master] as 'kind; - root : id; - pos : id; -} - -type ('kind,'edge,'info) t = { - cur_branch : Branch.t; - heads : 'kind branch_info BranchMap.t; - dag : ('edge,'info,id) Dag.t; -} - -let empty root = { - cur_branch = Branch.master; - heads = BranchMap.singleton Branch.master { root = root; pos = root; kind = `Master }; - dag = Dag.empty; -} - -let add_node vcs id edges = - assert (not (CList.is_empty edges)); - { vcs with dag = - List.fold_left (fun g (t,tgt) -> Dag.add_edge g id t tgt) vcs.dag edges } - -let get_branch vcs head = - try BranchMap.find head vcs.heads - with Not_found -> anomaly (str"head " ++ str head ++ str" not found") - -let reset_branch vcs head id = - let map name h = - if Branch.equal name head then { h with pos = id } else h - in - { vcs with heads = BranchMap.mapi map vcs.heads; } - -let current_branch vcs = vcs.cur_branch - -let branch - vcs ?(root=(get_branch vcs vcs.cur_branch).pos) ?(pos=root) name kind -= - { vcs with - heads = BranchMap.add name { kind; root; pos } vcs.heads; - cur_branch = name } - -let delete_branch vcs name = - if Branch.equal Branch.master name then vcs else - let filter n _ = not (Branch.equal n name) in - { vcs with heads = BranchMap.filter filter vcs.heads } - -let merge vcs id ~ours:tr1 ~theirs:tr2 ?(into = vcs.cur_branch) name = - assert (not (Branch.equal name into)); - let br_id = (get_branch vcs name).pos in - let cur_id = (get_branch vcs into).pos in - let vcs = add_node vcs id [tr1,cur_id; tr2,br_id] in - let vcs = reset_branch vcs into id in - vcs - -let del_edge id vcs tgt = { vcs with dag = Dag.del_edge vcs.dag id tgt } - -let rewrite_merge vcs id ~ours:tr1 ~theirs:tr2 ~at:cur_id name = - let br_id = (get_branch vcs name).pos in - let old_edges = List.map fst (Dag.from_node vcs.dag id) in - let vcs = List.fold_left (del_edge id) vcs old_edges in - let vcs = add_node vcs id [tr1,cur_id; tr2,br_id] in - vcs - -let commit vcs id tr = - let vcs = add_node vcs id [tr, (get_branch vcs vcs.cur_branch).pos] in - let vcs = reset_branch vcs vcs.cur_branch id in - vcs - -let checkout vcs name = { vcs with cur_branch = name } - -let set_info vcs id info = { vcs with dag = Dag.set_info vcs.dag id info } -let get_info vcs id = Dag.get_info vcs.dag id - -let create_cluster vcs l i = { vcs with dag = Dag.create_cluster vcs.dag l i } -let cluster_of vcs i = Dag.cluster_of vcs.dag i -let delete_cluster vcs c = { vcs with dag = Dag.del_cluster vcs.dag c } - -let branches vcs = BranchMap.fold (fun x _ accu -> x :: accu) vcs.heads [] -let dag vcs = vcs.dag - -let rec closure s d n = - let l = try Dag.from_node d n with Not_found -> [] in - List.fold_left (fun s (n',_) -> - if Dag.NodeSet.mem n' s then s - else closure s d n') - (Dag.NodeSet.add n s) l - -let reachable vcs i = closure Dag.NodeSet.empty vcs.dag i - -let gc vcs = - let alive = - BranchMap.fold (fun b { pos } s -> closure s vcs.dag pos) - vcs.heads Dag.NodeSet.empty in - let dead = Dag.NodeSet.diff (Dag.all_nodes vcs.dag) alive in - { vcs with dag = Dag.del_nodes vcs.dag dead }, dead - -end diff --git a/lib/vcs.mli b/lib/vcs.mli deleted file mode 100644 index 6c3571a082..0000000000 --- a/lib/vcs.mli +++ /dev/null @@ -1,90 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* t - val equal : t -> t -> bool - val compare : t -> t -> int - val to_string : t -> string - val master : t - end - - type id - - type ('kind) branch_info = { - kind : [> `Master] as 'kind; - root : id; - pos : id; - } - - type ('kind,'diff,'info) t constraint 'kind = [> `Master ] - - val empty : id -> ('kind,'diff,'info) t - - val current_branch : ('k,'e,'i) t -> Branch.t - val branches : ('k,'e,'i) t -> Branch.t list - - val get_branch : ('k,'e,'i) t -> Branch.t -> 'k branch_info - val reset_branch : ('k,'e,'i) t -> Branch.t -> id -> ('k,'e,'i) t - val branch : - ('kind,'e,'i) t -> ?root:id -> ?pos:id -> - Branch.t -> 'kind -> ('kind,'e,'i) t - val delete_branch : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t - val merge : - ('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> ?into:Branch.t -> - Branch.t -> ('k,'diff,'i) t - val commit : ('k,'diff,'i) t -> id -> 'diff -> ('k,'diff,'i) t - val rewrite_merge : - ('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> at:id -> - Branch.t -> ('k,'diff,'i) t - val checkout : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t - - val set_info : ('k,'e,'info) t -> id -> 'info -> ('k,'e,'info) t - val get_info : ('k,'e,'info) t -> id -> 'info option - - module NodeSet : Set.S with type elt = id - - (* Removes all unreachable nodes and returns them *) - val gc : ('k,'e,'info) t -> ('k,'e,'info) t * NodeSet.t - - val reachable : ('k,'e,'info) t -> id -> NodeSet.t - - (* read only dag *) - module Dag : Dag.S with type node = id - val dag : ('kind,'diff,'info) t -> ('diff,'info,id) Dag.t - - val create_cluster : ('k,'e,'i) t -> id list -> id -> ('k,'e,'i) t - val cluster_of : ('k,'e,'i) t -> id -> id Dag.Cluster.t option - val delete_cluster : ('k,'e,'i) t -> id Dag.Cluster.t -> ('k,'e,'i) t - -end - -module Make(OT : Map.OrderedType) : S with type id = OT.t diff --git a/lib/workerPool.ml b/lib/workerPool.ml deleted file mode 100644 index fcae4f20d6..0000000000 --- a/lib/workerPool.ml +++ /dev/null @@ -1,73 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* ?env:string array -> string -> string array -> - process * in_channel * out_channel -end) = struct - -type worker_id = int -type spawn = - args:string array -> env:string array -> unit -> - in_channel * out_channel * Worker.process - -let slave_managers = ref None - -let n_workers () = match !slave_managers with - | None -> 0 - | Some managers -> Array.length managers -let is_empty () = !slave_managers = None - -let magic_no = 17 - -let master_handshake worker_id ic oc = - try - Marshal.to_channel oc magic_no []; flush oc; - let n = (Marshal.from_channel ic : int) in - if n <> magic_no then begin - Printf.eprintf "Handshake with %d failed: protocol mismatch\n" worker_id; - exit 1; - end - with e when Errors.noncritical e -> - Printf.eprintf "Handshake with %d failed: %s\n" - worker_id (Printexc.to_string e); - exit 1 - -let respawn n ~args ~env () = - let proc, ic, oc = Worker.spawn ~env Sys.argv.(0) args in - master_handshake n ic oc; - ic, oc, proc - -let init ~size:n ~manager:manage_slave = - slave_managers := Some - (Array.init n (fun x -> - let cancel = ref false in - cancel, Thread.create (manage_slave ~cancel (x+1)) (respawn (x+1)))) - -let cancel n = - match !slave_managers with - | None -> () - | Some a -> - let switch, _ = a.(n) in - switch := true - -let worker_handshake slave_ic slave_oc = - try - let v = (Marshal.from_channel slave_ic : int) in - if v <> magic_no then begin - prerr_endline "Handshake failed: protocol mismatch\n"; - exit 1; - end; - Marshal.to_channel slave_oc v []; flush slave_oc; - with e when Errors.noncritical e -> - prerr_endline ("Handshake failed: " ^ Printexc.to_string e); - exit 1 - -end diff --git a/lib/workerPool.mli b/lib/workerPool.mli deleted file mode 100644 index d7a546929f..0000000000 --- a/lib/workerPool.mli +++ /dev/null @@ -1,30 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* ?env:string array -> string -> string array -> - process * in_channel * out_channel -end) : sig - -type worker_id = int -type spawn = - args:string array -> env:string array -> unit -> - in_channel * out_channel * Worker.process - -val init : - size:int -> manager:(cancel:bool ref -> worker_id -> spawn -> unit) -> unit -val is_empty : unit -> bool -val n_workers : unit -> int -val cancel : worker_id -> unit - -(* The worker should call this function *) -val worker_handshake : in_channel -> out_channel -> unit - -end diff --git a/myocamlbuild.ml b/myocamlbuild.ml index 6d3a243062..097a104259 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -106,7 +106,8 @@ let core_libs = ["lib/clib"; "lib/lib"; "kernel/kernel"; "library/library"; "pretyping/pretyping"; "interp/interp"; "proofs/proofs"; "parsing/parsing"; "printing/printing"; "tactics/tactics"; - "toplevel/toplevel"; "parsing/highparsing"; "tactics/hightactics"] + "stm/stm"; "toplevel/toplevel"; "parsing/highparsing"; + "tactics/hightactics"] let core_cma = List.map (fun s -> s^".cma") core_libs let core_cmxa = List.map (fun s -> s^".cmxa") core_libs let core_mllib = List.map (fun s -> s^".mllib") core_libs diff --git a/stm/dag.ml b/stm/dag.ml new file mode 100644 index 0000000000..9622f4c1fa --- /dev/null +++ b/stm/dag.ml @@ -0,0 +1,134 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'd t -> bool + val compare : 'd t -> 'd t -> int + val to_string : 'd t -> string + val data : 'd t -> 'd + end + + type node + module NodeSet : Set.S with type elt = node + + type ('edge,'info,'cdata) t + + val empty : ('e,'i,'d) t + + val add_edge : ('e,'i,'d) t -> node -> 'e -> node -> ('e,'i,'d) t + val from_node : ('e,'i,'d) t -> node -> (node * 'e) list + val mem : ('e,'i,'d) t -> node -> bool + val del_edge : ('e,'i,'d) t -> node -> node -> ('e,'i,'d) t + val del_nodes : ('e,'i,'d) t -> NodeSet.t -> ('e,'i,'d) t + val all_nodes : ('e,'i,'d) t -> NodeSet.t + + val iter : ('e,'i,'d) t -> + (node -> 'd Cluster.t option -> 'i option -> + (node * 'e) list -> unit) -> unit + + val create_cluster : ('e,'i,'d) t -> node list -> 'd -> ('e,'i,'d) t + val cluster_of : ('e,'i,'d) t -> node -> 'd Cluster.t option + val del_cluster : ('e,'i,'d) t -> 'd Cluster.t -> ('e,'i,'d) t + + val get_info : ('e,'i,'d) t -> node -> 'i option + val set_info : ('e,'i,'d) t -> node -> 'i -> ('e,'i,'d) t + val clear_info : ('e,'i,'d) t -> node -> ('e,'i,'d) t + +end + +module Make(OT : Map.OrderedType) = struct + +module Cluster = +struct + type 'd t = 'd * int + let equal (_,i1) (_,i2) = Int.equal i1 i2 + let compare (_,i1) (_,i2) = Int.compare i1 i2 + let to_string (_,i) = string_of_int i + let data (d,_) = d +end + +type node = OT.t + +module NodeMap = CMap.Make(OT) +module NodeSet = Set.Make(OT) + +type ('edge,'info,'data) t = { + graph : (node * 'edge) list NodeMap.t; + clusters : 'data Cluster.t NodeMap.t; + infos : 'info NodeMap.t; +} + +let empty = { + graph = NodeMap.empty; + clusters = NodeMap.empty; + infos = NodeMap.empty; +} + +let mem { graph } id = NodeMap.mem id graph + +let add_edge dag from trans dest = { dag with + graph = + try NodeMap.modify from (fun _ arcs -> (dest, trans) :: arcs) dag.graph + with Not_found -> NodeMap.add from [dest, trans] dag.graph } + +let from_node { graph } id = NodeMap.find id graph + +let del_edge dag id tgt = { dag with + graph = + try + let modify _ arcs = + let filter (d, _) = OT.compare d tgt <> 0 in + List.filter filter arcs + in + NodeMap.modify id modify dag.graph + with Not_found -> dag.graph } + +let del_nodes dag s = { + infos = NodeMap.filter (fun n _ -> not(NodeSet.mem n s)) dag.infos; + clusters = NodeMap.filter (fun n _ -> not(NodeSet.mem n s)) dag.clusters; + graph = NodeMap.filter (fun n l -> + let drop = NodeSet.mem n s in + if not drop then + assert(List.for_all (fun (n',_) -> not(NodeSet.mem n' s)) l); + not drop) + dag.graph } + +let clid = ref 1 +let create_cluster dag l data = + incr clid; + { dag with clusters = + List.fold_right (fun x clusters -> + NodeMap.add x (data, !clid) clusters) l dag.clusters } + +let cluster_of dag id = + try Some (NodeMap.find id dag.clusters) + with Not_found -> None + +let del_cluster dag c = + { dag with clusters = + NodeMap.filter (fun _ c' -> not (Cluster.equal c' c)) dag.clusters } + +let get_info dag id = + try Some (NodeMap.find id dag.infos) + with Not_found -> None + +let set_info dag id info = { dag with infos = NodeMap.add id info dag.infos } + +let clear_info dag id = { dag with infos = NodeMap.remove id dag.infos } + +let iter dag f = + NodeMap.iter (fun k v -> f k (cluster_of dag k) (get_info dag k) v) dag.graph + +let all_nodes dag = NodeMap.domain dag.graph + +end + diff --git a/stm/dag.mli b/stm/dag.mli new file mode 100644 index 0000000000..702ccd80f8 --- /dev/null +++ b/stm/dag.mli @@ -0,0 +1,52 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'd t -> bool + val compare : 'd t -> 'd t -> int + val to_string : 'd t -> string + val data : 'd t -> 'd + end + + type node + module NodeSet : Set.S with type elt = node + + type ('edge,'info,'cdata) t + + val empty : ('e,'i,'d) t + + val add_edge : ('e,'i,'d) t -> node -> 'e -> node -> ('e,'i,'d) t + val from_node : ('e,'i,'d) t -> node -> (node * 'e) list + val mem : ('e,'i,'d) t -> node -> bool + val del_edge : ('e,'i,'d) t -> node -> node -> ('e,'i,'d) t + val del_nodes : ('e,'i,'d) t -> NodeSet.t -> ('e,'i,'d) t + val all_nodes : ('e,'i,'d) t -> NodeSet.t + + val iter : ('e,'i,'d) t -> + (node -> 'd Cluster.t option -> 'i option -> + (node * 'e) list -> unit) -> unit + + val create_cluster : ('e,'i,'d) t -> node list -> 'd -> ('e,'i,'d) t + val cluster_of : ('e,'i,'d) t -> node -> 'd Cluster.t option + val del_cluster : ('e,'i,'d) t -> 'd Cluster.t -> ('e,'i,'d) t + + val get_info : ('e,'i,'d) t -> node -> 'i option + val set_info : ('e,'i,'d) t -> node -> 'i -> ('e,'i,'d) t + val clear_info : ('e,'i,'d) t -> node -> ('e,'i,'d) t + +end + +module Make(OT : Map.OrderedType) : S with type node = OT.t + diff --git a/stm/lemmas.ml b/stm/lemmas.ml new file mode 100644 index 0000000000..8f16ad5a4b --- /dev/null +++ b/stm/lemmas.ml @@ -0,0 +1,431 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + (pi2 (Global.lookup_named id),variable_opacity id) + | ConstRef cst -> + let cb = Global.lookup_constant cst in + (body_of_constant cb, is_opaque cb) + | _ -> assert false + +let adjust_guardness_conditions const = function + | [] -> const (* Not a recursive statement *) + | possible_indexes -> + (* Try all combinations... not optimal *) + let env = Global.env() in + { const with const_entry_body = + Future.chain ~greedy:true ~pure:true const.const_entry_body + (fun (body, eff) -> + match kind_of_term body with + | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> +(* let possible_indexes = + List.map2 (fun i c -> match i with Some i -> i | None -> + List.interval 0 (List.length ((lam_assum c)))) + lemma_guard (Array.to_list fixdefs) in +*) + let indexes = + search_guard Loc.ghost env + possible_indexes fixdecls in + mkFix ((indexes,0),fixdecls), eff + | _ -> body, eff) } + +let find_mutually_recursive_statements thms = + let n = List.length thms in + let inds = List.map (fun (id,(t,impls,annot)) -> + let (hyps,ccl) = decompose_prod_assum t in + let x = (id,(t,impls)) in + match annot with + (* Explicit fixpoint decreasing argument is given *) + | Some (Some (_,id),CStructRec) -> + let i,b,typ = lookup_rel_id id hyps in + (match kind_of_term t with + | Ind (kn,_ as ind) when + let mind = Global.lookup_mind kn in + mind.mind_finite && Option.is_empty b -> + [ind,x,i],[] + | _ -> + error "Decreasing argument is not an inductive assumption.") + (* Unsupported cases *) + | Some (_,(CWfRec _|CMeasureRec _)) -> + error "Only structural decreasing is supported for mutual statements." + (* Cofixpoint or fixpoint w/o explicit decreasing argument *) + | None | Some (None, CStructRec) -> + let whnf_hyp_hds = map_rel_context_in_env + (fun env c -> fst (whd_betadeltaiota_stack env Evd.empty c)) + (Global.env()) hyps in + let ind_hyps = + List.flatten (List.map_i (fun i (_,b,t) -> + match kind_of_term t with + | Ind (kn,_ as ind) when + let mind = Global.lookup_mind kn in + mind.mind_finite && Option.is_empty b -> + [ind,x,i] + | _ -> + []) 0 (List.rev whnf_hyp_hds)) in + let ind_ccl = + let cclenv = push_rel_context hyps (Global.env()) in + let whnf_ccl,_ = whd_betadeltaiota_stack cclenv Evd.empty ccl in + match kind_of_term whnf_ccl with + | Ind (kn,_ as ind) when + let mind = Global.lookup_mind kn in + Int.equal mind.mind_ntypes n && not mind.mind_finite -> + [ind,x,0] + | _ -> + [] in + ind_hyps,ind_ccl) thms in + let inds_hyps,ind_ccls = List.split inds in + let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> eq_mind kn kn' in + (* Check if all conclusions are coinductive in the same type *) + (* (degenerated cartesian product since there is at most one coind ccl) *) + let same_indccl = + List.cartesians_filter (fun hyp oks -> + if List.for_all (of_same_mutind hyp) oks + then Some (hyp::oks) else None) [] ind_ccls in + let ordered_same_indccl = + List.filter (List.for_all_i (fun i ((kn,j),_,_) -> Int.equal i j) 0) same_indccl in + (* Check if some hypotheses are inductive in the same type *) + let common_same_indhyp = + List.cartesians_filter (fun hyp oks -> + if List.for_all (of_same_mutind hyp) oks + then Some (hyp::oks) else None) [] inds_hyps in + let ordered_inds,finite,guard = + match ordered_same_indccl, common_same_indhyp with + | indccl::rest, _ -> + assert (List.is_empty rest); + (* One occ. of common coind ccls and no common inductive hyps *) + if not (List.is_empty common_same_indhyp) then + if_verbose msg_info (str "Assuming mutual coinductive statements."); + flush_all (); + indccl, true, [] + | [], _::_ -> + let () = match same_indccl with + | ind :: _ -> + if List.distinct_f ind_ord (List.map pi1 ind) + then + if_verbose msg_info + (strbrk + ("Coinductive statements do not follow the order of "^ + "definition, assuming the proof to be by induction.")); + flush_all () + | _ -> () + in + let possible_guards = List.map (List.map pi3) inds_hyps in + (* assume the largest indices as possible *) + List.last common_same_indhyp, false, possible_guards + | _, [] -> + error + ("Cannot find common (mutual) inductive premises or coinductive" ^ + " conclusions in the statements.") + in + (finite,guard,None), ordered_inds + +let look_for_possibly_mutual_statements = function + | [id,(t,impls,None)] -> + (* One non recursively proved theorem *) + None,[id,(t,impls)],None + | _::_ as thms -> + (* More than one statement and/or an explicit decreasing mark: *) + (* we look for a common inductive hyp or a common coinductive conclusion *) + let recguard,ordered_inds = find_mutually_recursive_statements thms in + let thms = List.map pi2 ordered_inds in + Some recguard,thms, Some (List.map (fun (_,_,i) -> succ i) ordered_inds) + | [] -> anomaly (Pp.str "Empty list of theorems.") + +(* Saving a goal *) + +let save id const do_guard (locality,kind) hook = + let const = adjust_guardness_conditions const do_guard in + let k = Kindops.logical_kind_of_goal_kind kind in + let l,r = match locality with + | Discharge when Lib.sections_are_opened () -> + let c = SectionLocalDef const in + let _ = declare_variable id (Lib.cwd(), c, k) in + (Local, VarRef id) + | Local | Global | Discharge -> + let local = match locality with + | Local | Discharge -> true + | Global -> false + in + let kn = declare_constant id ~local (DefinitionEntry const, k) in + (locality, ConstRef kn) in + definition_message id; + hook l r + +let default_thm_id = Id.of_string "Unnamed_thm" + +let compute_proof_name locality = function + | Some (loc,id) -> + (* We check existence here: it's a bit late at Qed time *) + if Nametab.exists_cci (Lib.make_path id) || is_section_variable id || + locality == Global && Nametab.exists_cci (Lib.make_path_except_section id) + then + user_err_loc (loc,"",pr_id id ++ str " already exists."); + id + | None -> + next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()) + +let save_remaining_recthms (locality,kind) body opaq i (id,(t_i,(_,imps))) = + match body with + | None -> + (match locality with + | Discharge -> + let impl = false in (* copy values from Vernacentries *) + let k = IsAssumption Conjectural in + let c = SectionLocalAssum (t_i,impl) in + let _ = declare_variable id (Lib.cwd(),c,k) in + (Discharge, VarRef id,imps) + | Local | Global -> + let k = IsAssumption Conjectural in + let local = match locality with + | Local -> true + | Global -> false + | Discharge -> assert false + in + let decl = (ParameterEntry (None,t_i,None), k) in + let kn = declare_constant id ~local decl in + (locality,ConstRef kn,imps)) + | Some body -> + let k = Kindops.logical_kind_of_goal_kind kind in + let body_i = match kind_of_term body with + | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) + | CoFix (0,decls) -> mkCoFix (i,decls) + | _ -> anomaly (Pp.str "Not a proof by induction") in + match locality with + | Discharge -> + let const = { const_entry_body = + Future.from_val (body_i,Declareops.no_seff); + const_entry_secctx = None; + const_entry_type = Some t_i; + const_entry_opaque = opaq; + const_entry_inline_code = false; + const_entry_feedback = None; + } in + let c = SectionLocalDef const in + let _ = declare_variable id (Lib.cwd(), c, k) in + (Discharge,VarRef id,imps) + | Local | Global -> + let local = match locality with + | Local -> true + | Global -> false + | Discharge -> assert false + in + let const = { const_entry_body = + Future.from_val (body_i,Declareops.no_seff); + const_entry_secctx = None; + const_entry_type = Some t_i; + const_entry_opaque = opaq; + const_entry_inline_code = false; + const_entry_feedback = None; + } in + let kn = declare_constant id ~local (DefinitionEntry const, k) in + (locality,ConstRef kn,imps) + +let save_hook = ref ignore +let set_save_hook f = save_hook := f + +let save_named proof = + let id,const,do_guard,persistence,hook = proof in + save id const do_guard persistence hook + +let check_anonymity id save_ident = + if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then + error "This command can only be used for unnamed theorem." + + +let save_anonymous proof save_ident = + let id,const,do_guard,persistence,hook = proof in + check_anonymity id save_ident; + save save_ident const do_guard persistence hook + +let save_anonymous_with_strength proof kind save_ident = + let id,const,do_guard,_,hook = proof in + check_anonymity id save_ident; + (* we consider that non opaque behaves as local for discharge *) + save save_ident const do_guard (Global, Proof kind) hook + +(* Admitted *) + +let admit hook () = + let (id,k,typ) = Pfedit.current_proof_statement () in + let e = Pfedit.get_used_variables(), typ, None in + let kn = declare_constant id (ParameterEntry e,IsAssumption Conjectural) in + let () = match fst k with + | Global -> () + | Local | Discharge -> + msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++ + str "declared as an axiom.") + in + let () = assumption_message id in + hook Global (ConstRef kn) + +(* Starting a goal *) + +let start_hook = ref ignore +let set_start_hook = (:=) start_hook + + +let get_proof proof do_guard hook opacity = + let (id,(const,persistence)) = + Pfedit.cook_this_proof proof + in + id,{const with const_entry_opaque = opacity},do_guard,persistence,hook + +let standard_proof_terminator compute_guard hook = + let open Proof_global in function + | Admitted -> + admit hook (); + Pp.feedback Interface.AddedAxiom + | Proved (is_opaque,idopt,proof) -> + let proof = get_proof proof compute_guard hook is_opaque in + begin match idopt with + | None -> save_named proof + | Some ((_,id),None) -> save_anonymous proof id + | Some ((_,id),Some kind) -> + save_anonymous_with_strength proof kind id + end + +let start_proof id kind ?sign c ?init_tac ?(compute_guard=[]) hook = + let terminator = standard_proof_terminator compute_guard hook in + let sign = + match sign with + | Some sign -> sign + | None -> initialize_named_context_for_proof () + in + !start_hook c; + Pfedit.start_proof id kind sign c ?init_tac terminator + + +let rec_tac_initializer finite guard thms snl = + if finite then + match List.map (fun (id,(t,_)) -> (id,t)) thms with + | (id,_)::l -> Tactics.mutual_cofix id l 0 + | _ -> assert false + else + (* nl is dummy: it will be recomputed at Qed-time *) + let nl = match snl with + | None -> List.map succ (List.map List.last guard) + | Some nl -> nl + in match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with + | (id,n,_)::l -> Tactics.mutual_fix id n l 0 + | _ -> assert false + +let start_proof_with_initialization kind recguard thms snl hook = + let intro_tac (_, (_, (ids, _))) = + Tacticals.New.tclMAP (function + | Name id -> Tactics.intro_mustbe_force id + | Anonymous -> Tactics.intro) (List.rev ids) in + let init_tac,guard = match recguard with + | Some (finite,guard,init_tac) -> + let rec_tac = Proofview.V82.tactic (rec_tac_initializer finite guard thms snl) in + Some (match init_tac with + | None -> + if Flags.is_auto_intros () then + Tacticals.New.tclTHENS rec_tac (List.map intro_tac thms) + else + rec_tac + | Some tacl -> + Tacticals.New.tclTHENS rec_tac + (if Flags.is_auto_intros () then + List.map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms + else + tacl)),guard + | None -> + let () = match thms with [_] -> () | _ -> assert false in + (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in + match thms with + | [] -> anomaly (Pp.str "No proof to start") + | (id,(t,(_,imps)))::other_thms -> + let hook strength ref = + let other_thms_data = + if List.is_empty other_thms then [] else + (* there are several theorems defined mutually *) + let body,opaq = retrieve_first_recthm ref in + List.map_i (save_remaining_recthms kind body opaq) 1 other_thms in + let thms_data = (strength,ref,imps)::other_thms_data in + List.iter (fun (strength,ref,imps) -> + maybe_declare_manual_implicits false ref imps; + hook strength ref) thms_data in + start_proof id kind t ?init_tac hook ~compute_guard:guard + +let start_proof_com kind thms hook = + let evdref = ref Evd.empty in + let env0 = Global.env () in + let thms = List.map (fun (sopt,(bl,t,guard)) -> + let impls, ((env, ctx), imps) = interp_context_evars evdref env0 bl in + let t', imps' = interp_type_evars_impls ~impls evdref env t in + check_evars_are_solved env Evd.empty !evdref; + let ids = List.map pi1 ctx in + (compute_proof_name (fst kind) sopt, + (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), + (ids, imps @ lift_implicits (List.length ids) imps'), + guard))) + thms in + let recguard,thms,snl = look_for_possibly_mutual_statements thms in + start_proof_with_initialization kind recguard thms snl hook + + +(* Saving a proof *) + +let save_proof ?proof = function + | Vernacexpr.Admitted -> + Proof_global.get_terminator() Proof_global.Admitted + | Vernacexpr.Proved (is_opaque,idopt) -> + let (proof_obj,terminator) = + match proof with + | None -> Proof_global.close_proof (fun x -> x) + | Some proof -> proof + in + (* if the proof is given explicitly, nothing has to be deleted *) + if Option.is_empty proof then Pfedit.delete_current_proof (); + terminator (Proof_global.Proved (is_opaque,idopt,proof_obj)) + +(* Miscellaneous *) + +let get_current_context () = + try Pfedit.get_current_goal_context () + with e when Logic.catchable_exception e -> + (Evd.empty, Global.env()) + + + + + + + + + + diff --git a/stm/lemmas.mli b/stm/lemmas.mli new file mode 100644 index 0000000000..bbe383a857 --- /dev/null +++ b/stm/lemmas.mli @@ -0,0 +1,50 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit) -> unit + +val start_proof : Id.t -> goal_kind -> ?sign:Environ.named_context_val -> types -> + ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> + unit declaration_hook -> unit + +val start_proof_com : goal_kind -> + (lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)) list -> + unit declaration_hook -> unit + +val start_proof_with_initialization : + goal_kind -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option -> + (Id.t * (types * (Name.t list * Impargs.manual_explicitation list))) list + -> int list option -> unit declaration_hook -> unit + +val standard_proof_terminator : + Proof_global.lemma_possible_guards -> unit declaration_hook -> + Proof_global.proof_terminator + +(** {6 ... } *) + +(** A hook the next three functions pass to cook_proof *) +val set_save_hook : (Proof.proof -> unit) -> unit + +val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit + + +(** [get_current_context ()] returns the evar context and env of the + current open proof if any, otherwise returns the empty evar context + and the current global env *) + +val get_current_context : unit -> Evd.evar_map * Environ.env + diff --git a/stm/spawned.ml b/stm/spawned.ml new file mode 100644 index 0000000000..d025945690 --- /dev/null +++ b/stm/spawned.ml @@ -0,0 +1,84 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + prerr_endline (Printf.sprintf "Handshake with %d OK" pid); + output_value cout (Hello (proto_version,Unix.getpid ())); flush cout + | _ -> raise (Failure "handshake protocol") + with + | Failure s | Invalid_argument s | Sys_error s -> + pr_err ("Handshake failed: " ^ s); raise (Failure "handshake") + | End_of_file -> + pr_err "Handshake failed: End_of_file"; raise (Failure "handshake") + +let open_bin_connection h p = + let open Unix in + let cin, cout = open_connection (ADDR_INET (inet_addr_of_string h,p)) in + set_binary_mode_in cin true; + set_binary_mode_out cout true; + cin, cout + +let controller h p = + prerr_endline "starting controller thread"; + let main () = + let ic, oc = open_bin_connection h p in + let rec loop () = + try + match input_value ic with + | Hello _ -> prerr_endline "internal protocol error"; exit 1 + | ReqDie -> prerr_endline "death sentence received"; exit 0 + | ReqStats -> + output_value oc (RespStats (Gc.stat ())); flush oc; loop () + with + | e -> + prerr_endline ("control channel broken: " ^ Printexc.to_string e); + exit 1 in + loop () in + ignore(Thread.create main ()) + +let main_channel = ref None +let control_channel = ref None + +let channels = ref None + +let init_channels () = + if !channels <> None then Errors.anomaly(Pp.str "init_channels called twice"); + let () = match !main_channel with + | None -> () + | Some (Socket(mh,mp)) -> + channels := Some (open_bin_connection mh mp); + | Some AnonPipe -> + let stdin = Unix.in_channel_of_descr (Unix.dup Unix.stdin) in + let stdout = Unix.out_channel_of_descr (Unix.dup Unix.stdout) in + Unix.dup2 Unix.stderr Unix.stdout; + set_binary_mode_in stdin true; + set_binary_mode_out stdout true; + channels := Some (stdin, stdout); + in + match !control_channel with + | None -> () + | Some (Socket (ch, cp)) -> + controller ch cp + | Some AnonPipe -> + Errors.anomaly (Pp.str "control channel cannot be a pipe") + +let get_channels () = + match !channels with + | None -> Errors.anomaly(Pp.str "init_channels not called") + | Some(ic, oc) -> ic, oc + diff --git a/stm/spawned.mli b/stm/spawned.mli new file mode 100644 index 0000000000..18b88dc64b --- /dev/null +++ b/stm/spawned.mli @@ -0,0 +1,22 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit + +(* Once initialized, these are the channels to talk with our master *) +val get_channels : unit -> in_channel * out_channel + diff --git a/stm/stm.ml b/stm/stm.ml new file mode 100644 index 0000000000..e791e37cfc --- /dev/null +++ b/stm/stm.ml @@ -0,0 +1,2075 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + "master" ^ string_of_int (Thread.id (Thread.self ())) + | Flags.APonParallel n -> "worker" ^ string_of_int n + +let pr_err s = Printf.eprintf "%s] %s\n" (process_id ()) s; flush stderr + +let prerr_endline s = if !Flags.debug then begin pr_err s end else () + +let (f_process_error, process_error_hook) = Hook.make () +let ((f_interp : (?verbosely:bool -> ?proof:Proof_global.closed_proof -> + Loc.t * Vernacexpr.vernac_expr -> unit) Hook.value), interp_hook) = Hook.make () + +open Vernacexpr +open Errors +open Pp +open Names +open Util +open Ppvernac +open Vernac_classifier + +(* During interactive use we cache more states so that Undoing is fast *) +let interactive () = + if !Flags.ide_slave || !Flags.print_emacs || not !Flags.batch_mode then `Yes + else `No + +let fallback_to_lazy_if_marshal_error = ref true +let fallback_to_lazy_if_slave_dies = ref true +let async_proofs_workers_extra_env = ref [||] + +type ast = { verbose : bool; loc : Loc.t; mutable expr : vernac_expr } +let pr_ast { expr } = pr_vernac expr + +(* Wrapper for Vernacentries.interp to set the feedback id *) +let vernac_interp ?proof id { verbose; loc; expr } = + let internal_command = function + | VernacResetName _ | VernacResetInitial | VernacBack _ + | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _ + | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true | _ -> false in + if internal_command expr then begin + prerr_endline ("ignoring " ^ string_of_ppcmds(pr_vernac expr)) + end else begin + Pp.set_id_for_feedback (Interface.State id); + Aux_file.record_in_aux_set_at loc; + prerr_endline ("interpreting " ^ string_of_ppcmds(pr_vernac expr)); + let interp = Hook.get f_interp in + try interp ~verbosely:verbose ?proof (loc, expr) + with e -> + let e = Errors.push e in + raise (Hook.get f_process_error e) + end + +(* Wrapper for Vernac.parse_sentence to set the feedback id *) +let vernac_parse eid s = + set_id_for_feedback (Interface.Edit eid); + let pa = Pcoq.Gram.parsable (Stream.of_string s) in + Flags.with_option Flags.we_are_parsing (fun () -> + match Pcoq.Gram.entry_parse Pcoq.main_entry pa with + | None -> raise (Invalid_argument "vernac_parse") + | Some ast -> ast) + () + +module Vcs_ = Vcs.Make(Stateid) +type future_proof = Entries.proof_output list Future.computation +type proof_mode = string +type depth = int +type cancel_switch = bool ref +type branch_type = + [ `Master + | `Proof of proof_mode * depth + | `Edit of proof_mode * Stateid.t * Stateid.t ] +type cmd_t = ast * Id.t list +type fork_t = ast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Id.t list +type qed_t = { + qast : ast; + keep : vernac_qed_type; + mutable fproof : (future_proof * cancel_switch) option; + brname : Vcs_.Branch.t; + brinfo : branch_type Vcs_.branch_info +} +type seff_t = ast option +type alias_t = Stateid.t +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 + | `Qed of qed_t * Stateid.t + | `Sideff of [ `Ast of ast * Stateid.t | `Id of Stateid.t ] + | `Alias of alias_t ] +type visit = { step : step; next : Stateid.t } + +type state = { + system : States.state; + proof : Proof_global.state; + shallow : bool +} +type branch = Vcs_.Branch.t * branch_type Vcs_.branch_info +type backup = { mine : branch; others : branch list } +type 'vcs state_info = { (* Make private *) + mutable n_reached : int; + mutable n_goals : int; + mutable state : state option; + mutable vcs_backup : 'vcs option * backup option; +} +let default_info () = + { n_reached = 0; n_goals = 0; state = None; vcs_backup = None,None } + +(* Functions that work on a Vcs with a specific branch type *) +module Vcs_aux : sig + + val proof_nesting : (branch_type, 't,'i) Vcs_.t -> int + val find_proof_at_depth : + (branch_type, 't, 'i) Vcs_.t -> int -> + Vcs_.Branch.t * branch_type Vcs_.branch_info + exception Expired + val visit : (branch_type, transaction,'i) Vcs_.t -> Vcs_.Dag.node -> visit + +end = struct (* {{{ *) + + let proof_nesting vcs = + List.fold_left max 0 + (List.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(m, n) } -> Int.equal n pl + | _, { Vcs_.kind = `Edit _ } -> anomaly(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(str"Visiting the initial state id") + else if Stateid.equal id Stateid.dummy then + anomaly(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; next = n } + | [n, Qed x; p, Noop] + | [p, Noop; n, Qed x] -> { step = `Qed (x,p); next = n } + | [n, Sideff None; p, Noop] + | [p, Noop; n, Sideff None]-> { step = `Sideff (`Id p); next = n } + | [n, Sideff (Some x); p, Noop] + | [p, Noop; n, Sideff (Some x)]-> { step = `Sideff(`Ast (x,p)); next = n } + | [n, Sideff (Some x)]-> {step = `Sideff(`Ast (x,Stateid.dummy)); next=n} + | _ -> anomaly (str ("Malformed VCS at node "^Stateid.to_string id)) + with Not_found -> raise Expired + +end (* }}} *) + +(* Imperative wrap around VCS to obtain _the_ VCS *) +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) Vcs_.t + + val init : id -> unit + + 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 : 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 : ast -> 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 -> Vcs_.NodeSet.t + val cur_tip : unit -> id + + val get_info : id -> vcs state_info + val reached : id -> bool -> unit + val goals : id -> int -> unit + val set_state : id -> state -> unit + val get_state : id -> state option + val forget_state : id -> unit + + (* cuts from start -> stop, raising Expired if some nodes are not there *) + val slice : start:id -> stop:id -> vcs + + val create_cluster : id list -> tip:id -> unit + val cluster_of : id -> id option + val delete_cluster_of : id -> unit + + val proof_nesting : unit -> int + val checkout_shallowest_proof_branch : unit -> unit + val propagate_sideff : ast option -> 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 + + module StateidSet = Set.Make(Stateid) + open Printf + + let print_dag vcs () = (* {{{ *) + let fname = "stm_" ^ process_id () in + let string_of_transaction = function + | Cmd (t, _) | Fork (t, _,_,_) -> + (try string_of_ppcmds (pr_ast t) with _ -> "ERR") + | Sideff (Some t) -> + sprintf "Sideff(%s)" + (try string_of_ppcmds (pr_ast t) with _ -> "ERR") + | Sideff None -> "EnvChange" + | Noop -> " " + | Alias id -> sprintf "Alias(%s)" (Stateid.to_string id) + | Qed { qast } -> string_of_ppcmds (pr_ast qast) in + let is_green id = + match get_info vcs id with + | Some { state = Some _ } -> true + | _ -> false in + let is_red id = + match get_info vcs id with + | Some s -> Int.equal s.n_reached ~-1 + | _ -> 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 "<%s>" + (quote (string_of_transaction tr)) in + let ids = ref StateidSet.empty in + let clus = Hashtbl.create 13 in + let node_info id = + match get_info vcs id with + | None -> "" + | Some info -> + sprintf "<%s" (Stateid.to_string id) ^ + sprintf " 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 add_to_clus_or_ids from cf = + match cf with + | None -> ids := StateidSet.add from !ids; false + | Some c -> Hashtbl.replace clus c + (try let n = Hashtbl.find clus c in from::n + with Not_found -> [from]); true in + let oc = open_out fname_dot in + output_string oc "digraph states {\nsplines=ortho\n"; + Dag.iter graph (fun from cf _ l -> + let c1 = add_to_clus_or_ids from cf in + List.iter (fun (dest, trans) -> + let c2 = add_to_clus_or_ids dest (Dag.cluster_of graph dest) in + fprintf oc "%s -> %s [label=%s,labelfloat=%b];\n" + (node from) (node dest) (edge trans) (c1 && c2)) l + ); + StateidSet.iter (nodefmt oc) !ids; + Hashtbl.iter (fun c nodes -> + fprintf oc "subgraph cluster_%s {\n" (Dag.Cluster.to_string c); + List.iter (nodefmt oc) nodes; + fprintf oc "color=blue; }\n" + ) clus; + 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) t + let vcs : vcs ref = ref (empty Stateid.dummy) + + let init id = + vcs := empty id; + vcs := set_info !vcs id (default_info ()) + + 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 () = + let id = Stateid.fresh () in + vcs := set_info !vcs id (default_info ()); + 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 x with + | VernacDefinition (_,(_,i),_) -> string_of_id i + | VernacStartTheoremProof (_,[Some (_,i),_],_) -> string_of_id 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 = (get_info id).state <- Some s + let get_state id = (get_info id).state + let forget_state id = (get_info id).state <- None + let reached id b = + let info = get_info id in + if b then info.n_reached <- info.n_reached + 1 + else 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; + match get_branch edit_branch with + | { kind = `Edit (mode, _, _) } -> Proof_global.activate_proof_mode mode + | _ -> assert false + end else + let pl = proof_nesting () in + try + let branch, mode = match Vcs_aux.find_proof_at_depth !vcs pl with + | h, { Vcs_.kind = `Proof (m, _) } -> h, m | _ -> assert false in + checkout branch; + prerr_endline ("mode:" ^ mode); + Proof_global.activate_proof_mode mode + with Failure _ -> + checkout Branch.master; + Proof_global.disactivate_proof_mode "Classic" + + (* copies the transaction on every open branch *) + let propagate_sideff t = + List.iter (fun b -> + checkout b; + let id = new_node () in + merge id ~ours:(Sideff t) ~into:b Branch.master) + (List.filter (fun b -> not (Branch.equal b Branch.master)) (branches ())) + + let visit id = Vcs_aux.visit !vcs id + + let slice ~start ~stop = + let l = + let rec aux id = + if Stateid.equal id stop 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 (`Ast (x,_)) } -> + (id,Sideff (Some x)) :: aux n + | _ -> anomaly(str("Cannot slice from "^ Stateid.to_string start ^ + " to "^Stateid.to_string stop)) + in aux start in + let copy_info v id = + Vcs_.set_info v id + { (get_info id) with state = None; vcs_backup = None,None } in + let copy_info_w_state v id = + Vcs_.set_info v id { (get_info id) with vcs_backup = None,None } in + let v = Vcs_.empty stop in + let v = copy_info v stop 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 (not (Option.is_empty (get_info stop).state)); + (* We put in the new dag the most recent state known to master *) + let rec fill id = + if (get_info id).state = None then fill (Vcs_aux.visit v id).next + else copy_info_w_state v id in + fill start + + let create_cluster l ~tip = vcs := create_cluster !vcs l tip + let cluster_of id = Option.map Dag.Cluster.data (cluster_of !vcs id) + let delete_cluster_of id = + Option.iter (fun x -> vcs := delete_cluster !vcs x) (Vcs_.cluster_of !vcs id) + + let gc () = + let old_vcs = !vcs in + let new_vcs, erased_nodes = gc old_vcs in + Vcs_.NodeSet.iter (fun id -> + match (Vcs_aux.visit old_vcs id).step with + | `Qed ({ fproof = Some (_, 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 (Thread.create run_command ()) + end + + end (* }}} *) + + let print ?(now=false) () = + if not !Flags.debug && not now then () else NB.command ~now (print_dag !vcs) + + let backup () = !vcs + let restore v = vcs := v + +end (* }}} *) + +(* Fills in the nodes of the VCS *) +module State : sig + + (** 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 : + ?redefine:bool -> ?cache:Summary.marshallable -> (unit -> unit) -> Stateid.t -> unit + + val install_cached : Stateid.t -> unit + val is_cached : Stateid.t -> bool + + + val exn_on : Stateid.t -> ?valid:Stateid.t -> exn -> exn + (* to send states across worker/master *) + type frozen_state + val get_cached : Stateid.t -> frozen_state + val assign : Stateid.t -> frozen_state -> unit + +end = struct (* {{{ *) + + (* 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 + + (* helpers *) + let freeze_global_state marshallable = + { system = States.freeze ~marshallable; + proof = Proof_global.freeze ~marshallable; + shallow = (marshallable = `Shallow) } + let unfreeze_global_state { system; proof } = + States.unfreeze system; Proof_global.unfreeze proof + + (* hack to make futures functional *) + let in_t, out_t = Dyn.create "state4future" + let () = Future.set_freeze + (fun () -> in_t (freeze_global_state `No, !cur_id)) + (fun t -> let s,i = out_t t in unfreeze_global_state s; cur_id := i) + + let is_cached id = + Stateid.equal id !cur_id || + match VCS.get_info id with + | { state = Some _ } -> true + | _ -> false + + let install_cached id = + if Stateid.equal id !cur_id then () else (* optimization *) + let s = + match VCS.get_info id with + | { state = Some s } -> s + | _ -> anomaly (str "unfreezing a non existing state") in + unfreeze_global_state s; cur_id := id + + type frozen_state = state + + let get_cached id = + try match VCS.get_info id with + | { state = Some s } -> s + | _ -> anomaly (str "not a cached state") + with VCS.Expired -> anomaly (str "not a cached state (expired)") + + let assign id s = + try if VCS.get_state id = None then VCS.set_state id s + with VCS.Expired -> () + + let freeze marhallable id = VCS.set_state id (freeze_global_state marhallable) + + let exn_on id ?valid e = + match Stateid.get e with + | Some _ -> e + | None -> + let loc = Option.default Loc.ghost (Loc.get_loc e) in + let msg = string_of_ppcmds (print e) in + Pp.feedback ~state_id:id (Interface.ErrorMsg (loc, msg)); + Stateid.add (Hook.get f_process_error e) ?valid id + + let define ?(redefine=false) ?(cache=`No) f id = + let str_id = Stateid.to_string id in + if is_cached id && not redefine then + anomaly (str"defining state "++str str_id++str" twice"); + try + prerr_endline("defining "^str_id^" (cache="^ + if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)"); + f (); + if cache = `Yes then freeze `No id + else if cache = `Shallow then freeze `Shallow id; + prerr_endline ("setting cur id to "^str_id); + cur_id := id; + feedback ~state_id:id Interface.Processed; + VCS.reached id true; + if Proof_global.there_are_pending_proofs () then + VCS.goals id (Proof_global.get_open_goals ()); + with e -> + let e = Errors.push e in + let good_id = !cur_id in + cur_id := Stateid.dummy; + VCS.reached id false; + match Stateid.get e with + | Some _ -> raise e + | None -> raise (exn_on id ~valid:good_id e) + +end +(* }}} *) + +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 !hints loc "context_used" in + let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") s) in + let ids = List.map (fun id -> Loc.ghost, id) ids in + SsExpr (SsSet ids) + +let get_hint_bp_time proof_name = + try float_of_string (Aux_file.get !hints Loc.ghost proof_name) + with Not_found -> 1.0 + +module Worker = Spawn.Sync(struct + let add_timeout ~sec f = + ignore(Thread.create (fun () -> + while true do + Unix.sleep sec; + if not (f ()) then Thread.exit () + done) + ()) +end) + +module WorkersPool = WorkerPool.Make(Worker) + +let record_pb_time proof_name loc 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 Loc.ghost proof_name proof_build_time; + hints := Aux_file.set !hints Loc.ghost proof_name proof_build_time + end + +(* Slave processes (if initialized, otherwise local lazy evaluation) *) +module Slaves : sig + + (* (eventually) remote calls *) + val build_proof : loc:Loc.t -> + exn_info:(Stateid.t * Stateid.t) -> start:Stateid.t -> stop:Stateid.t -> + name:string -> future_proof * 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 + + (* slave process main loop *) + val slave_main_loop : (unit -> unit) -> unit + val slave_init_stdout : unit -> unit + + (* to disentangle modules *) + val set_reach_known_state : + (?redefine_qed:bool -> cache:Summary.marshallable -> Stateid.t -> unit) -> unit + + type tasks + val dump : (Future.UUID.t * int) list -> tasks + val check_task : string -> tasks -> int -> bool + val info_tasks : tasks -> (string * float * int) list + val finish_task : + string -> + Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs -> + tasks -> int -> Library.seg_univ + + val cancel_worker : int -> unit + + val set_perspective : Stateid.t list -> unit + +end = struct (* {{{ *) + + + let cancel_worker n = WorkersPool.cancel (n-1) + + let reach_known_state = ref (fun ?redefine_qed ~cache id -> ()) + let set_reach_known_state f = reach_known_state := f + + type 'a request = + ReqBuildProof of + (Stateid.t * Stateid.t) * Stateid.t * VCS.vcs * Loc.t * 'a * string + + let name_of_request (ReqBuildProof (_,_,_,_,_,s)) = s + + type response = + | RespBuiltProof of Entries.proof_output list * float + | RespError of (* err, safe, msg, safe_states *) + Stateid.t * Stateid.t * std_ppcmds * + (Stateid.t * State.frozen_state) list + | RespFeedback of Interface.feedback + | RespGetCounterFreshLocalUniv + | RespGetCounterNewUnivLevel + let pr_response = function + | RespBuiltProof _ -> "Sucess" + | RespError _ -> "Error" + | RespFeedback { Interface.id = Interface.State id } -> + "Feedback on " ^ Stateid.to_string id + | RespFeedback _ -> assert false + | RespGetCounterFreshLocalUniv -> "GetCounterFreshLocalUniv" + | RespGetCounterNewUnivLevel -> "GetCounterNewUnivLevel" + + type more_data = + | MoreDataLocalUniv of Univ.universe list + | MoreDataUnivLevel of Univ.universe_level list + + type task = + | TaskBuildProof of (Stateid.t * Stateid.t) * Stateid.t * Stateid.t * + (Entries.proof_output list Future.assignement -> unit) * cancel_switch + * Loc.t * Future.UUID.t * string + let pr_task = function + | TaskBuildProof(_,bop,eop,_,_,_,_,s) -> + "TaskBuilProof("^Stateid.to_string bop^","^Stateid.to_string eop^ + ","^s^")" + + let request_of_task task : Future.UUID.t request = + match task with + | TaskBuildProof (exn_info,bop,eop,_,_,loc,uuid,s) -> + ReqBuildProof(exn_info,eop,VCS.slice ~start:eop ~stop:bop,loc,uuid,s) + + let cancel_switch_of_task = function + | TaskBuildProof (_,_,_,_,c,_,_,_) -> c + + let build_proof_here_core loc eop () = + let wall_clock1 = Unix.gettimeofday () in + if !Flags.batch_mode then !reach_known_state ~cache:`No eop + else !reach_known_state ~cache:`Shallow eop; + let wall_clock2 = Unix.gettimeofday () in + Aux_file.record_in_aux_at loc "proof_build_time" + (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); + Proof_global.return_proof () + let build_proof_here (id,valid) loc eop = + Future.create (State.exn_on id ~valid) (build_proof_here_core loc eop) + + let slave_respond msg = + match msg with + | ReqBuildProof(exn_info,eop,vcs,loc,_,_) -> + VCS.restore vcs; + VCS.print (); + let rc, time = + let wall_clock = Unix.gettimeofday () in + let l = Future.force (build_proof_here exn_info loc eop) in + List.iter (fun (_,se) -> Declareops.iter_side_effects (function + | Declarations.SEsubproof(_, + { Declarations.const_body = Declarations.OpaqueDef f } ) -> + Opaqueproof.join_opaque f + | _ -> ()) + se) l; + l, Unix.gettimeofday () -. wall_clock in + VCS.print (); + RespBuiltProof(rc,time) + + let check_task_aux extra name l i = + match List.nth l i with + | ReqBuildProof ((id,valid),eop,vcs,loc,_,s) -> + Pp.msg_info( + str(Printf.sprintf "Checking task %d (%s%s) of %s" i s extra name)); + VCS.restore vcs; + try + !reach_known_state ~cache:`No eop; + (* The original terminator, a hook, has not been saved in the .vi*) + Proof_global.set_terminator + (Lemmas.standard_proof_terminator [] (fun _ _ -> ())); + let proof = Proof_global.close_proof (fun x -> x) in + vernac_interp eop ~proof + { verbose = false; loc; + expr = (VernacEndProof (Proved (true,None))) }; + Some proof + with e -> + let e = Errors.push e in + (try match Stateid.get e with + | None -> + Pp.pperrnl Pp.( + str"File " ++ str name ++ str ": proof of " ++ str s ++ + spc () ++ print e) + | Some (_, cur) -> + match VCS.visit cur with + | { step = `Cmd ( { loc }, _) } + | { step = `Fork ( { loc }, _, _, _) } + | { step = `Qed ( { qast = { loc } }, _) } + | { step = `Sideff (`Ast ( { loc }, _)) } -> + let start, stop = Loc.unloc loc in + Pp.pperrnl Pp.( + str"File " ++ str name ++ str ": proof of " ++ str s ++ + str ": chars " ++ int start ++ str "-" ++ int stop ++ + spc () ++ print e) + | _ -> + Pp.pperrnl Pp.( + str"File " ++ str name ++ str ": proof of " ++ str s ++ + spc () ++ print e) + with e -> + Pp.msg_error (str"unable to print error message: " ++ + str (Printexc.to_string e))); None + + let finish_task name (u,cst,_) d p l i = + let bucket = + match List.nth l i with ReqBuildProof (_,_,_,_,bucket,_) -> bucket in + match check_task_aux (Printf.sprintf ", bucket %d" bucket) name l i with + | None -> exit 1 + | Some (po,pt) -> + let discharge c = List.fold_right Cooking.cook_constr d.(bucket) c in + let con = + Nametab.locate_constant + (Libnames.qualid_of_ident po.Proof_global.id) in + let c = Global.lookup_constant con in + match c.Declarations.const_body with + | Declarations.OpaqueDef lc -> + let uc = Option.get (Opaqueproof.get_constraints lc) in + let uc = + Future.chain ~greedy:true ~pure:true uc Univ.hcons_constraints in + let pr = Opaqueproof.get_proof lc in + let pr = Future.chain ~greedy:true ~pure:true pr discharge in + let pr = Future.chain ~greedy:true ~pure:true pr Constr.hcons in + Future.sink pr; + let extra = Future.join uc in + u.(bucket) <- uc; + p.(bucket) <- pr; + u, Univ.union_constraints cst extra, false + | _ -> assert false + + let check_task name l i = + match check_task_aux "" name l i with + | Some _ -> true + | None -> false + + let info_tasks l = + CList.map_i (fun i (ReqBuildProof(_,_,_,loc,_,s)) -> + let time1 = + try float_of_string (Aux_file.get !hints loc "proof_build_time") + with Not_found -> 0.0 in + let time2 = + try float_of_string (Aux_file.get !hints loc "proof_check_time") + with Not_found -> 0.0 in + s,max (time1 +. time2) 0.0001,i) 0 l + + open Interface + + exception MarshalError of string + + let marshal_to_channel oc data = + Marshal.to_channel oc data []; + flush oc + + let marshal_err s = raise (MarshalError s) + + let marshal_request oc (req : Future.UUID.t request) = + try marshal_to_channel oc req + with Failure s | Invalid_argument s | Sys_error s -> + marshal_err ("marshal_request: "^s) + + let unmarshal_request ic = + try (Marshal.from_channel ic : Future.UUID.t request) + with Failure s | Invalid_argument s | Sys_error s -> + marshal_err ("unmarshal_request: "^s) + + let marshal_response oc (res : response) = + try marshal_to_channel oc res + with Failure s | Invalid_argument s | Sys_error s -> + marshal_err ("marshal_response: "^s) + + let unmarshal_response ic = + try (CThread.thread_friendly_input_value ic : response) + with Failure s | Invalid_argument s | Sys_error s -> + marshal_err ("unmarshal_response: "^s) + + let marshal_more_data oc (res : more_data) = + try marshal_to_channel oc res + with Failure s | Invalid_argument s | Sys_error s -> + marshal_err ("marshal_more_data: "^s) + + let unmarshal_more_data ic = + try (Marshal.from_channel ic : more_data) + with Failure s | Invalid_argument s | Sys_error s -> + marshal_err ("unmarshal_more_data: "^s) + + let queue : task TQueue.t = TQueue.create () + + let set_perspective idl = + let open Stateid in + let p = List.fold_right Set.add idl Set.empty in + TQueue.reorder queue (fun task1 task2 -> + let TaskBuildProof (_, a1, b1, _, _,_,_,_) = task1 in + let TaskBuildProof (_, a2, b2, _, _,_,_,_) = task2 in + match Set.mem a1 p || Set.mem b1 p, Set.mem a2 p || Set.mem b2 p with + | true, true | false, false -> 0 + | true, false -> -1 + | false, true -> 1) + + let wait_all_done () = + if not (WorkersPool.is_empty ()) then + TQueue.wait_until_n_are_waiting_and_queue_empty + (WorkersPool.n_workers ()) queue + + let build_proof ~loc ~exn_info:(id,valid as exn_info) ~start ~stop ~name = + let cancel_switch = ref false in + if WorkersPool.is_empty () then + if !Flags.compilation_mode = Flags.BuildVi then begin + let force () : Entries.proof_output list Future.assignement = + try `Val (build_proof_here_core loc stop ()) + with e -> let e = Errors.push e in `Exn e in + let f,assign = Future.create_delegate ~force (State.exn_on id ~valid) in + let uuid = Future.uuid f in + TQueue.push queue (TaskBuildProof + (exn_info,start,stop,assign,cancel_switch,loc,uuid,name)); + f, cancel_switch + end else + build_proof_here exn_info loc stop, cancel_switch + else + let f, assign = Future.create_delegate (State.exn_on id ~valid) in + let uuid = Future.uuid f in + Pp.feedback (Interface.InProgress 1); + TQueue.push queue (TaskBuildProof + (exn_info,start,stop,assign,cancel_switch,loc,uuid,name)); + f, cancel_switch + + exception RemoteException of std_ppcmds + let _ = Errors.register_handler (function + | RemoteException ppcmd -> ppcmd + | _ -> raise Unhandled) + + exception KillRespawn + + let report_status ?id s = + let id = + match id with + | Some n -> n + | None -> + match !Flags.async_proofs_mode with + | Flags.APonParallel n -> n + | _ -> assert false in + Pp.feedback ~state_id:Stateid.initial (Interface.SlaveStatus(id, s)) + + let rec manage_slave ~cancel:cancel_user_req id_slave respawn = + let ic, oc, proc = + let rec set_slave_opt = function + | [] -> ["-async-proofs"; "worker"; string_of_int id_slave; "-feedback-glob"] + | ("-ideslave"|"-emacs"|"-emacs-U")::tl -> set_slave_opt tl + | ("-async-proofs" + |"-compile" + |"-compile-verbose")::_::tl -> set_slave_opt tl + | x::tl -> x :: set_slave_opt tl in + let args = + Array.of_list (set_slave_opt (List.tl (Array.to_list Sys.argv))) in + let env = + Array.append !async_proofs_workers_extra_env (Unix.environment ()) in + respawn ~args ~env () in + let last_task = ref None in + let task_expired = ref false in + let task_cancelled = ref false in + CThread.prepare_in_channel_for_thread_friendly_io ic; + try + while true do + prerr_endline "waiting for a task"; + report_status ~id:id_slave "Idle"; + let task = TQueue.pop queue in + prerr_endline ("got task: "^pr_task task); + last_task := Some task; + try + marshal_request oc (request_of_task task); + let cancel_switch = cancel_switch_of_task task in + Worker.kill_if proc ~sec:1 (fun () -> + task_expired := !cancel_switch; + task_cancelled := !cancel_user_req; + if !cancel_user_req then cancel_user_req := false; + !task_expired || !task_cancelled); + let rec loop () = + let response = unmarshal_response ic in + match task, response with + | TaskBuildProof(_,_,_, assign,_,loc,_,s), + RespBuiltProof(pl, time)-> + assign (`Val pl); + (* We restart the slave, to avoid memory leaks. We could just + Pp.feedback (Interface.InProgress ~-1) *) + record_pb_time s loc time; + last_task := None; + raise KillRespawn + | TaskBuildProof(_,_,_, assign,_,_,_,_), + RespError(err_id,valid,e,valid_states) -> + let e = Stateid.add ~valid (RemoteException e) err_id in + assign (`Exn e); + List.iter (fun (id,s) -> State.assign id s) valid_states; + (* We restart the slave, to avoid memory leaks. We could just + Pp.feedback (Interface.InProgress ~-1) *) + last_task := None; + raise KillRespawn + | _, RespGetCounterFreshLocalUniv -> + marshal_more_data oc (MoreDataLocalUniv + (CList.init 10 (fun _ -> Univ.fresh_local_univ ()))); + if !cancel_switch then raise KillRespawn else loop () + | _, RespGetCounterNewUnivLevel -> + marshal_more_data oc (MoreDataUnivLevel + (CList.init 10 (fun _ -> Termops.new_univ_level ()))); + loop () + | _, RespFeedback {id = State state_id; content = msg} -> + Pp.feedback ~state_id msg; + loop () + | _, RespFeedback _ -> assert false (* Parsing in master process *) + in + loop () + with + | VCS.Expired -> (* task cancelled: e.g. the user did backtrack *) + Pp.feedback (Interface.InProgress ~-1); + prerr_endline ("Task expired: " ^ pr_task task) + | (Sys_error _ | Invalid_argument _ | End_of_file | KillRespawn) as e -> + raise e (* we pass the exception to the external handler *) + | MarshalError s when !fallback_to_lazy_if_marshal_error -> + msg_warning(strbrk("Marshalling error: "^s^". "^ + "The system state could not be sent to the worker process. "^ + "Falling back to local, lazy, evaluation.")); + let TaskBuildProof (exn_info, _, stop, assign,_,loc,_,_) = task in + assign(`Comp(build_proof_here exn_info loc stop)); + Pp.feedback (Interface.InProgress ~-1) + | MarshalError s -> + pr_err ("Fatal marshal error: " ^ s); + flush_all (); exit 1 + | e -> + pr_err ("Uncaught exception in worker manager: "^ + string_of_ppcmds (print e)); + flush_all () + done + with + | KillRespawn -> + Pp.feedback (Interface.InProgress ~-1); + Worker.kill proc; ignore(Worker.wait proc); + manage_slave ~cancel:cancel_user_req id_slave respawn + | Sys_error _ | Invalid_argument _ | End_of_file when !task_expired -> + Pp.feedback (Interface.InProgress ~-1); + ignore(Worker.wait proc); + manage_slave ~cancel:cancel_user_req id_slave respawn + | Sys_error _ | Invalid_argument _ | End_of_file when !task_cancelled -> + msg_warning(strbrk "The worker was cancelled."); + Option.iter (fun task -> + let TaskBuildProof (_, start, _, assign, _,_,_,_) = task in + let s = "Worker cancelled by the user" in + let e = Stateid.add ~valid:start (RemoteException (strbrk s)) start in + assign (`Exn e); + Pp.feedback ~state_id:start (Interface.ErrorMsg (Loc.ghost, s)); + Pp.feedback (Interface.InProgress ~-1); + ) !last_task; + Worker.kill proc; ignore(Worker.wait proc); + manage_slave ~cancel:cancel_user_req id_slave respawn + | Sys_error _ | Invalid_argument _ | End_of_file + when !fallback_to_lazy_if_slave_dies -> + msg_warning(strbrk "The worker process died badly."); + Option.iter (fun task -> + msg_warning(strbrk "Falling back to local, lazy, evaluation."); + let TaskBuildProof (exn_info, _, stop, assign,_,loc,_,_) = task in + assign(`Comp(build_proof_here exn_info loc stop)); + Pp.feedback (Interface.InProgress ~-1); + ) !last_task; + Worker.kill proc; ignore(Worker.wait proc); + manage_slave ~cancel:cancel_user_req id_slave respawn + | Sys_error _ | Invalid_argument _ | End_of_file -> + Worker.kill proc; + let exit_status proc = match Worker.wait proc with + | Unix.WEXITED 0x400 -> "exit code unavailable" + | Unix.WEXITED i -> Printf.sprintf "exit(%d)" i + | Unix.WSIGNALED sno -> Printf.sprintf "signalled(%d)" sno + | Unix.WSTOPPED sno -> Printf.sprintf "stopped(%d)" sno in + pr_err ("Fatal worker error: " ^ (exit_status proc)); + flush_all (); exit 1 + + let init () = WorkersPool.init !Flags.async_proofs_n_workers manage_slave + + let slave_ic = ref stdin + let slave_oc = ref stdout + + let slave_init_stdout () = + let ic, oc = Spawned.get_channels () in + slave_oc := oc; slave_ic := ic + + let bufferize f = + let l = ref [] in + fun () -> + match !l with + | [] -> let data = f () in l := List.tl data; List.hd data + | x::tl -> l := tl; x + + let slave_handshake () = WorkersPool.worker_handshake !slave_ic !slave_oc + + let slave_main_loop reset = + let slave_feeder oc fb = + Marshal.to_channel oc (RespFeedback fb) []; + flush oc in + Pp.set_feeder (slave_feeder !slave_oc); + Termops.set_remote_new_univ_level (bufferize (fun () -> + marshal_response !slave_oc RespGetCounterNewUnivLevel; + match unmarshal_more_data !slave_ic with + | MoreDataUnivLevel l -> l | _ -> assert false)); + Univ.set_remote_fresh_local_univ (bufferize (fun () -> + marshal_response !slave_oc RespGetCounterFreshLocalUniv; + match unmarshal_more_data !slave_ic with + | MoreDataLocalUniv l -> l | _ -> assert false)); + let working = ref false in + slave_handshake (); + while true do + try + working := false; + let request = unmarshal_request !slave_ic in + working := true; + report_status (name_of_request request); + let response = slave_respond request in + report_status "Idle"; + marshal_response !slave_oc response; + reset () + with + | MarshalError s -> + pr_err ("Fatal marshal error: " ^ s); flush_all (); exit 2 + | End_of_file -> + prerr_endline "connection lost"; flush_all (); exit 2 + | e when Errors.noncritical e -> + (* This can happen if the proof is broken. The error has also been + * signalled as a feedback, hence we can silently recover *) + let err_id, safe_id = match Stateid.get e with + | Some (safe, err) -> err, safe + | None -> Stateid.dummy, Stateid.dummy in + prerr_endline "failed with the following exception:"; + prerr_endline (string_of_ppcmds (print e)); + prerr_endline ("last safe id is: " ^ Stateid.to_string safe_id); + prerr_endline ("cached? " ^ string_of_bool (State.is_cached safe_id)); + let prog old_v n = + if n < 3 then n else old_v + n/3 + if n mod 3 > 0 then 1 else 0 in + let states = + let open State in + let rec aux n m prev_id = + let next = + try Some (VCS.visit prev_id).next + with VCS.Expired -> None in + match next with + | None -> [] + | Some id when n = m -> + prerr_endline ("sending back state " ^ string_of_int m); + let tail = aux (n+1) (prog m (n+1)) id in + if is_cached id then (id, get_cached id) :: tail else tail + | Some id -> aux (n+1) m id in + (if is_cached safe_id then [safe_id,get_cached safe_id] else []) + @ aux 1 (prog 1 1) safe_id in + marshal_response !slave_oc (RespError(err_id, safe_id, print e, states)) + | e -> + pr_err ("Slave: critical exception: " ^ Pp.string_of_ppcmds (print e)); + flush_all (); exit 1 + done + + (* For external users this name is nicer than request *) + type tasks = int request list + let dump f2t_map = + assert(WorkersPool.is_empty ()); (* ATM, we allow that only if no slaves *) + let tasks = TQueue.dump queue in + prerr_endline (Printf.sprintf "dumping %d\n" (List.length tasks)); + let tasks = List.map request_of_task tasks in + List.map (function ReqBuildProof(a,b,c,d,x,e) -> + ReqBuildProof(a,b,c,d,List.assoc x f2t_map,e)) tasks + +end (* }}} *) + +(* Runs all transactions needed to reach a state *) +module Reach : sig + + val known_state : + ?redefine_qed:bool -> cache:Summary.marshallable -> Stateid.t -> unit + +end = struct (* {{{ *) + +let pstate = ["meta counter"; "evar counter"; "program-tcc-table"] + +let delegate_policy_check time = + if interactive () = `Yes then + (!Flags.async_proofs_mode = Flags.APonParallel 0 || + !Flags.async_proofs_mode = Flags.APonLazy) && time >= 1.0 + else if !Flags.compilation_mode = Flags.BuildVi then true + else !Flags.async_proofs_mode <> Flags.APoff && time >= 1.0 + +let collect_proof cur hd brkind id = + prerr_endline ("Collecting proof ending at "^Stateid.to_string id); + let no_name = "" in + let name = function + | [] -> no_name + | id :: _ -> Id.to_string id in + let loc = (snd cur).loc in + let is_defined = function + | _, { expr = VernacEndProof (Proved (false,_)) } -> true + | _ -> false in + let rec collect last accn id = + let view = VCS.visit id in + match last, view.step with + | _, `Cmd (x, _) -> collect (Some (id,x)) (id::accn) view.next + | _, `Alias _ -> `Sync (no_name,`Alias) + | _, `Fork(_,_,_,_::_::_)-> `Sync (no_name,`MutualProofs) + | _, `Fork(_,_,Doesn'tGuaranteeOpacity,_) -> + `Sync (no_name,`Doesn'tGuaranteeOpacity) + | Some (parent, ({ expr = VernacProof(_,Some _)} as v)), + `Fork (_, hd', GuaranteesOpacity, ids) -> + let name = name ids in + let time = get_hint_bp_time name in + assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch); + if delegate_policy_check time + then `ASync (parent,Some v,accn,name) + else `Sync (name,`Policy) + | Some (parent, ({ expr = VernacProof(t,None)} as v)), + `Fork (_, hd', GuaranteesOpacity, ids) when + not (State.is_cached parent) && + !Flags.compilation_mode = Flags.BuildVi -> + (try + let name = name ids in + let hint, time = get_hint_ctx loc, get_hint_bp_time name in + assert (VCS.Branch.equal hd hd'||VCS.Branch.equal hd VCS.edit_branch); + v.expr <- VernacProof(t, Some hint); + if delegate_policy_check time + then `ASync (parent,Some v,accn,name) + else `Sync (name,`Policy) + with Not_found -> `Sync (no_name,`NoHint)) + | Some (parent, _), `Fork (_, hd', GuaranteesOpacity, ids) -> + assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch); + let name = name ids in + let time = get_hint_bp_time name in + if delegate_policy_check time + then `MaybeASync (parent, accn, name) + else `Sync (name,`Policy) + | _, `Sideff _ -> `Sync (no_name,`NestedProof) + | _ -> `Sync (no_name,`Unknown) in + match cur, (VCS.visit id).step, brkind with + |( parent, { expr = VernacExactProof _ }), `Fork _, _ -> + `Sync (no_name,`Immediate) + | _, _, { VCS.kind = `Edit _ } -> collect (Some cur) [] id + | _ -> + if is_defined cur then `Sync (no_name,`Transparent) + else + let rc = collect (Some cur) [] id in + if not (State.is_cached id) then rc + else (* we already have the proof, no gain in delaying *) + match rc with + | `Sync(name,_) -> `Sync (name,`AlreadyEvaluated) + | `MaybeASync(_,_,name) -> `Sync (name,`AlreadyEvaluated) + | `ASync(_,_,_,name) -> `Sync (name,`AlreadyEvaluated) + +let string_of_reason = function + | `Transparent -> "Transparent" + | `AlreadyEvaluated -> "AlreadyEvaluated" + | `Policy -> "Policy" + | `NestedProof -> "NestedProof" + | `Immediate -> "Immediate" + | `Alias -> "Alias" + | `NoHint -> "NoHint" + | `Doesn'tGuaranteeOpacity -> "Doesn'tGuaranteeOpacity" + | _ -> "Unknown Reason" + +let wall_clock_last_fork = ref 0.0 + +let known_state ?(redefine_qed=false) ~cache id = + + (* ugly functions to process nested lemmas, i.e. hard to reproduce + * side effects *) + let cherry_pick_non_pstate () = + Summary.freeze_summary ~marshallable:`No ~complement:true pstate, + Lib.freeze ~marshallable:`No in + let inject_non_pstate (s,l) = Summary.unfreeze_summary s; Lib.unfreeze l in + + let rec pure_cherry_pick_non_pstate id = Future.purify (fun id -> + prerr_endline ("cherry-pick non pstate " ^ Stateid.to_string id); + reach id; + cherry_pick_non_pstate ()) id + + (* traverses the dag backward from nodes being already calculated *) + and reach ?(redefine_qed=false) ?(cache=cache) id = + prerr_endline ("reaching: " ^ Stateid.to_string id); + if not redefine_qed && State.is_cached id then begin + State.install_cached id; + feedback ~state_id:id Interface.Processed; + prerr_endline ("reached (cache)") + end else + let step, cache_step = + let view = VCS.visit id in + match view.step with + | `Alias id -> (fun () -> + reach view.next; reach id + ), cache + | `Cmd (x,_) -> (fun () -> + reach view.next; vernac_interp id x + ), cache + | `Fork (x,_,_,_) -> (fun () -> + reach view.next; vernac_interp id x; + wall_clock_last_fork := Unix.gettimeofday () + ), `Yes + | `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) -> + let rec aux = function + | `ASync (start, proof_using_ast, nodes, name) -> (fun () -> + prerr_endline ("Asynchronous " ^ Stateid.to_string id); + VCS.create_cluster nodes ~tip:id; + begin match keep, brinfo, qed.fproof with + | VtKeep, { VCS.kind = `Edit _ }, None -> assert false + | VtKeep, { VCS.kind = `Edit _ }, Some (ofp, cancel) -> + assert(redefine_qed = true); + VCS.create_cluster nodes ~tip:id; + let fp, cancel = Slaves.build_proof + ~loc:x.loc ~exn_info:(id,eop) ~start ~stop:eop ~name in + Future.replace ofp fp; + qed.fproof <- Some (fp, cancel) + | VtKeep, { VCS.kind = `Proof _ }, Some _ -> assert false + | VtKeep, { VCS.kind = `Proof _ }, None -> + reach ~cache:`Shallow start; + let fp, cancel = Slaves.build_proof + ~loc:x.loc ~exn_info:(id,eop) ~start ~stop:eop ~name in + qed.fproof <- Some (fp, cancel); + let proof = + Proof_global.close_future_proof ~feedback_id:id fp in + reach view.next; + vernac_interp id ~proof x; + feedback ~state_id:id Interface.Incomplete + | VtDrop, _, _ -> + reach view.next; + Option.iter (vernac_interp start) proof_using_ast; + vernac_interp id x + | _, { VCS.kind = `Master }, _ -> assert false + end; + Proof_global.discard_all () + ), if redefine_qed then `No else `Yes + | `Sync (name, `Immediate) -> (fun () -> + assert (Stateid.equal view.next eop); + reach eop; vernac_interp id x; Proof_global.discard_all () + ), `Yes + | `Sync (name, reason) -> (fun () -> + prerr_endline ("Synchronous " ^ Stateid.to_string id ^ " " ^ + string_of_reason reason); + reach eop; + let wall_clock = Unix.gettimeofday () in + record_pb_time name x.loc (wall_clock -. !wall_clock_last_fork); + begin match keep with + | VtKeep -> + let proof = + Proof_global.close_proof (State.exn_on id ~valid:eop) in + reach view.next; + let wall_clock2 = Unix.gettimeofday () in + vernac_interp id ~proof x; + let wall_clock3 = Unix.gettimeofday () in + Aux_file.record_in_aux_at x.loc "proof_check_time" + (Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2)) + | VtDrop -> + reach view.next; + vernac_interp id x + end; + Proof_global.discard_all () + ), `Yes + | `MaybeASync (start, nodes, name) -> (fun () -> + prerr_endline ("MaybeAsynchronous " ^ Stateid.to_string id); + reach ~cache:`Shallow start; + (* no sections *) + if List.is_empty (Environ.named_context (Global.env ())) + then fst (aux (`ASync (start, None, nodes, name))) () + else fst (aux (`Sync (name, `Unknown))) () + ), if redefine_qed then `No else `Yes + in + aux (collect_proof (view.next, x) brname brinfo eop) + | `Sideff (`Ast (x,_)) -> (fun () -> + reach view.next; vernac_interp id x + ), cache + | `Sideff (`Id origin) -> (fun () -> + let s = pure_cherry_pick_non_pstate origin in + reach view.next; + inject_non_pstate s + ), cache + in + if !Flags.async_proofs_mode = Flags.APonParallel 0 then + Pp.feedback ~state_id:id Interface.ProcessingInMaster; + State.define ~cache:cache_step ~redefine:redefine_qed step id; + prerr_endline ("reached: "^ Stateid.to_string id) in + reach ~redefine_qed id + +end (* }}} *) +let _ = Slaves.set_reach_known_state Reach.known_state + +(* The backtrack module simulates the classic behavior of a linear document *) +module Backtrack : sig + + val record : unit -> unit + val backto : Stateid.t -> unit + val back_safe : unit -> unit + + (* we could navigate the dag, but this ways easy *) + val branches_of : Stateid.t -> backup + + (* To be installed during initialization *) + val undo_vernac_classifier : vernac_expr -> vernac_classification + +end = struct (* {{{ *) + + let record () = + let current_branch = VCS.current_branch () in + 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 + info.vcs_backup <- Some (VCS.backup ()), Some { mine; others } + + let backto oid = + let info = VCS.get_info oid in + match info.vcs_backup with + | None, _ -> + anomaly(str"Backtrack.backto "++str(Stateid.to_string oid)++ + str": a state with no vcs_backup") + | Some vcs, _ -> + VCS.restore vcs; + let id = VCS.get_branch_pos (VCS.current_branch ()) in + if not (Stateid.equal id oid) then + anomaly (str "Backtrack.backto did not jump to the right state") + + let branches_of id = + let info = VCS.get_info id in + match info.vcs_backup with + | _, None -> + anomaly(str"Backtrack.backto "++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 = + if id = Stateid.initial || id = Stateid.dummy then [] else + match VCS.visit id with + | { step = `Fork (_,_,_,l) } -> l + | { step = `Cmd (_,l) } -> l + | _ -> [] in + match f acc (id, vcs, ids) with + | `Stop x -> x + | `Cont acc -> next acc + + let back_safe () = + let id = + fold_until (fun n (id,_,_) -> + if n >= 0 && State.is_cached id then `Stop id else `Cont (succ n)) + 0 (VCS.get_branch_pos (VCS.current_branch ())) in + backto id + + let undo_vernac_classifier v = + try + match v with + | VernacResetInitial -> + VtStm (VtBack Stateid.initial, true), VtNow + | VernacResetName (_,name) -> + msg_warning + (str"Reset not implemented for automatically generated constants"); + let id = VCS.get_branch_pos (VCS.current_branch ()) in + (try + let oid = + fold_until (fun b (id,_,label) -> + if b then `Stop id else `Cont (List.mem name label)) + false id in + VtStm (VtBack oid, true), VtNow + with Not_found -> + VtStm (VtBack id, true), VtNow) + | VernacBack n -> + let id = VCS.get_branch_pos (VCS.current_branch ()) in + let oid = fold_until (fun n (id,_,_) -> + if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in + VtStm (VtBack oid, true), VtNow + | VernacUndo n -> + let id = VCS.get_branch_pos (VCS.current_branch ()) in + let oid = fold_until (fun n (id,_,_) -> + if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in + VtStm (VtBack oid, true), VtLater + | VernacUndoTo _ + | VernacRestart as e -> + let m = match e with VernacUndoTo m -> m | _ -> 0 in + let id = VCS.get_branch_pos (VCS.current_branch ()) in + let vcs = + match (VCS.get_info id).vcs_backup with + | None, _ -> anomaly(str"Backtrack: tip with no vcs_backup") + | Some vcs, _ -> vcs in + let cb, _ = + Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs) 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 + VtStm (VtBack oid, true), VtLater + | VernacAbortAll -> + let id = VCS.get_branch_pos (VCS.current_branch ()) in + let oid = fold_until (fun () (id,vcs,_) -> + match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ()) + () id in + VtStm (VtBack oid, true), VtLater + | VernacBacktrack (id,_,_) + | VernacBackTo id -> + VtStm (VtBack (Stateid.of_int id), true), VtNow + | _ -> VtUnknown, VtNow + with + | Not_found -> + msg_warning(str"undo_vernac_classifier: going back to the initial state."); + VtStm (VtBack Stateid.initial, true), VtNow + +end (* }}} *) + +let init () = + VCS.init Stateid.initial; + set_undo_classifier Backtrack.undo_vernac_classifier; + State.define ~cache:`Yes (fun () -> ()) Stateid.initial; + Backtrack.record (); + if !Flags.async_proofs_mode = Flags.APonParallel 0 then begin + Slaves.init (); + let opts = match !Flags.async_proofs_worker_flags with + | None -> [] + | Some s -> Str.split_delim (Str.regexp ",") s in + if String.List.mem "fallback-to-lazy-if-marshal-error=no" opts then + fallback_to_lazy_if_marshal_error := false; + if String.List.mem "fallback-to-lazy-if-slave-dies=no" opts then + fallback_to_lazy_if_slave_dies := false; + begin try + let env_opt = Str.regexp "^extra-env=" in + let env = List.find (fun s -> Str.string_match env_opt s 0) opts in + async_proofs_workers_extra_env := Array.of_list + (Str.split_delim (Str.regexp ";") (Str.replace_first env_opt "" env)) + with Not_found -> () end; + end + +let slave_main_loop () = Slaves.slave_main_loop Ephemeron.clear + +let slave_init_stdout () = Slaves.slave_init_stdout () + +let observe id = + let vcs = VCS.backup () in + try + Reach.known_state ~cache:(interactive ()) id; + VCS.print () + with e -> + let e = Errors.push e in + VCS.print (); + VCS.restore vcs; + raise e + +let finish () = + observe (VCS.get_branch_pos (VCS.current_branch ())); + VCS.print () + +let wait () = + Slaves.wait_all_done (); + VCS.print () + +let join () = + let rec jab id = + if Stateid.equal id Stateid.initial then () + else + let view = VCS.visit id in + match view.step with + | `Qed ({ keep = VtDrop }, eop) -> + Future.purify observe eop; jab view.next + | _ -> jab view.next in + finish (); + wait (); + prerr_endline "Joining the environment"; + Global.join_safe_environment (); + VCS.print (); + prerr_endline "Joining the aborted proofs"; + jab (VCS.get_branch_pos VCS.Branch.master); + VCS.print () + +type tasks = Slaves.tasks * RemoteCounter.remote_counters_status +let dump x = Slaves.dump x, RemoteCounter.backup () +let check_task name (tasks,_) i = + let vcs = VCS.backup () in + try + let rc = Future.purify (Slaves.check_task name tasks) i in + Pp.pperr_flush (); + VCS.restore vcs; + rc + with e when Errors.noncritical e -> VCS.restore vcs; false +let info_tasks (tasks,_) = Slaves.info_tasks tasks +let finish_tasks name u d p (t,rcbackup as tasks) = + RemoteCounter.restore rcbackup; + let finish_task u (_,_,i) = + let vcs = VCS.backup () in + let u = Future.purify (Slaves.finish_task name u d p t) i in + Pp.pperr_flush (); + VCS.restore vcs; + u in + try + let u, a, _ = List.fold_left finish_task u (info_tasks tasks) in + (u,a,true), p + with e -> + let e = Errors.push e in + Pp.pperrnl Pp.(str"File " ++ str name ++ str ":" ++ spc () ++ print e); + exit 1 + +let merge_proof_branch qast keep brname = + let brinfo = VCS.get_branch brname in + let qed fproof = { qast; keep; brname; brinfo; fproof } in + match brinfo with + | { VCS.kind = `Proof _ } -> + VCS.checkout VCS.Branch.master; + let id = VCS.new_node () in + VCS.merge id ~ours:(Qed (qed None)) brname; + VCS.delete_branch brname; + if keep == VtKeep then VCS.propagate_sideff None; + `Ok + | { VCS.kind = `Edit (mode, qed_id, master_id) } -> + let ofp = + match VCS.visit qed_id with + | { step = `Qed ({ fproof }, _) } -> fproof + | _ -> assert false in + VCS.rewrite_merge qed_id ~ours:(Qed (qed ofp)) ~at:master_id brname; + VCS.delete_branch brname; + VCS.gc (); + Reach.known_state ~redefine_qed:true ~cache:`No qed_id; + VCS.checkout VCS.Branch.master; + `Unfocus qed_id + | { VCS.kind = `Master } -> + raise (State.exn_on Stateid.dummy Proof_global.NoCurrentProof) + +(* When tty is true, this code also does some of the job of the user interface: + jump back to a state that is valid *) +let handle_failure e vcs tty = + match Stateid.get e with + | None -> + VCS.restore vcs; + VCS.print (); + if tty && interactive () = `Yes then begin + (* Hopefully the 1 to last state is valid *) + Backtrack.back_safe (); + VCS.checkout_shallowest_proof_branch (); + end; + VCS.print (); + anomaly(str"error with no safe_id attached:" ++ spc() ++ + Errors.print_no_report e) + | Some (safe_id, id) -> + prerr_endline ("Failed at state " ^ Stateid.to_string id); + VCS.restore vcs; + if tty && interactive () = `Yes then begin + (* We stay on a valid state *) + Backtrack.backto safe_id; + VCS.checkout_shallowest_proof_branch (); + Reach.known_state ~cache:(interactive ()) safe_id; + end; + VCS.print (); + raise e + +let process_transaction ~tty verbose c (loc, expr) = + let warn_if_pos a b = + if b then msg_warning(pr_ast a ++ str" should not be part of a script") in + let v, x = expr, { verbose = verbose && Flags.is_verbose(); loc; expr } in + prerr_endline ("{{{ processing: "^ string_of_ppcmds (pr_ast x)); + let vcs = VCS.backup () in + try + let head = VCS.current_branch () in + VCS.checkout head; + let rc = begin + prerr_endline (" classified as: " ^ string_of_vernac_classification c); + match c with + (* PG stuff *) + | VtStm(VtPG,false), VtNow -> vernac_interp Stateid.dummy x; `Ok + | VtStm(VtPG,_), _ -> anomaly(str "PG command in script or VtLater") + (* Joining various parts of the document *) + | VtStm (VtJoinDocument, b), VtNow -> warn_if_pos x b; join (); `Ok + | VtStm (VtFinish, b), VtNow -> warn_if_pos x b; finish (); `Ok + | VtStm (VtWait, b), VtNow -> warn_if_pos x b; finish (); wait (); `Ok + | VtStm (VtPrintDag, b), VtNow -> + warn_if_pos x b; VCS.print ~now:true (); `Ok + | VtStm (VtObserve id, b), VtNow -> warn_if_pos x b; observe id; `Ok + | VtStm ((VtObserve _ | VtFinish | VtJoinDocument + |VtPrintDag |VtWait),_), VtLater -> + anomaly(str"classifier: join actions cannot be classified as VtLater") + + (* Back *) + | VtStm (VtBack oid, true), w -> + let id = VCS.new_node () in + let { mine; others } = Backtrack.branches_of oid in + List.iter (fun branch -> + if not (List.mem_assoc branch (mine::others)) then + ignore(merge_proof_branch x VtDrop branch)) + (VCS.branches ()); + VCS.checkout_shallowest_proof_branch (); + let head = VCS.current_branch () in + List.iter (fun b -> + if not(VCS.Branch.equal b head) then begin + VCS.checkout b; + VCS.commit (VCS.new_node ()) (Alias oid); + end) + (VCS.branches ()); + VCS.checkout_shallowest_proof_branch (); + VCS.commit id (Alias oid); + Backtrack.record (); if w == VtNow then finish (); `Ok + | VtStm (VtBack id, false), VtNow -> + prerr_endline ("undo to state " ^ Stateid.to_string id); + Backtrack.backto id; + VCS.checkout_shallowest_proof_branch (); + Reach.known_state ~cache:(interactive ()) id; `Ok + | VtStm (VtBack id, false), VtLater -> + anomaly(str"classifier: VtBack + VtLater must imply part_of_script") + + (* Query *) + | VtQuery false, VtNow when tty = true -> + finish (); + (try Future.purify (vernac_interp Stateid.dummy) + { verbose = true; loc; expr } + with e when Errors.noncritical e -> + let e = Errors.push e in + raise(State.exn_on Stateid.dummy e)); `Ok + | VtQuery false, VtNow -> + (try vernac_interp Stateid.dummy x + with e when Errors.noncritical e -> + let e = Errors.push e in + raise(State.exn_on Stateid.dummy e)); `Ok + | VtQuery true, w -> + let id = VCS.new_node () in + VCS.commit id (Cmd (x,[])); + Backtrack.record (); if w == VtNow then finish (); `Ok + | VtQuery false, VtLater -> + anomaly(str"classifier: VtQuery + VtLater must imply part_of_script") + + (* Proof *) + | VtStartProof (mode, guarantee, names), w -> + let id = VCS.new_node () in + let bname = VCS.mk_branch_name x in + VCS.checkout VCS.Branch.master; + VCS.commit id (Fork (x, bname, guarantee, names)); + VCS.branch bname (`Proof (mode, VCS.proof_nesting () + 1)); + Proof_global.activate_proof_mode mode; + Backtrack.record (); if w == VtNow then finish (); `Ok + | VtProofMode _, VtLater -> + anomaly(str"VtProofMode must be executed VtNow") + | VtProofMode mode, VtNow -> + let id = VCS.new_node () in + VCS.checkout VCS.Branch.master; + VCS.commit id (Cmd (x,[])); + VCS.propagate_sideff (Some x); + List.iter + (fun bn -> match VCS.get_branch bn with + | { VCS.root; kind = `Master; pos } -> () + | { VCS.root; kind = `Proof(_,d); pos } -> + VCS.delete_branch bn; + VCS.branch ~root ~pos bn (`Proof(mode,d)) + | { VCS.root; kind = `Edit(_,f,q); pos } -> + VCS.delete_branch bn; + VCS.branch ~root ~pos bn (`Edit(mode,f,q))) + (VCS.branches ()); + VCS.checkout_shallowest_proof_branch (); + Backtrack.record (); + finish (); + `Ok + | VtProofStep, w -> + let id = VCS.new_node () in + VCS.commit id (Cmd (x,[])); + Backtrack.record (); if w == VtNow then finish (); `Ok + | VtQed keep, w -> + let rc = merge_proof_branch x keep head in + VCS.checkout_shallowest_proof_branch (); + Backtrack.record (); if w == VtNow then finish (); + rc + + (* Side effect on all branches *) + | VtSideff l, w -> + let id = VCS.new_node () in + VCS.checkout VCS.Branch.master; + VCS.commit id (Cmd (x,l)); + VCS.propagate_sideff (Some x); + VCS.checkout_shallowest_proof_branch (); + Backtrack.record (); if w == VtNow then finish (); `Ok + + (* Unknown: we execute it, check for open goals and propagate sideeff *) + | VtUnknown, VtNow -> + let id = VCS.new_node () in + let step () = + VCS.checkout VCS.Branch.master; + let mid = VCS.get_branch_pos VCS.Branch.master in + Reach.known_state ~cache:(interactive ()) mid; + vernac_interp id x; + (* Vernac x may or may not start a proof *) + if VCS.Branch.equal head VCS.Branch.master && + Proof_global.there_are_pending_proofs () + then begin + let bname = VCS.mk_branch_name x in + VCS.commit id (Fork (x,bname,Doesn'tGuaranteeOpacity,[])); + VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1)); + Proof_global.activate_proof_mode "Classic"; + end else begin + VCS.commit id (Cmd (x,[])); + VCS.propagate_sideff (Some x); + VCS.checkout_shallowest_proof_branch (); + end in + State.define ~cache:`Yes step id; + Backtrack.record (); `Ok + + | VtUnknown, VtLater -> + anomaly(str"classifier: VtUnknown must imply VtNow") + end in + (* Proof General *) + begin match v with + | VernacStm (PGLast _) -> + if not (VCS.Branch.equal head VCS.Branch.master) then + vernac_interp Stateid.dummy + { verbose = true; loc = Loc.ghost; + expr = VernacShow (ShowGoal OpenSubgoals) } + | _ -> () + end; + prerr_endline "processed }}}"; + VCS.print (); + rc + with e -> + let e = Errors.push e in + handle_failure e vcs tty + +(** STM interface {{{******************************************************* **) + +let stop_worker n = Slaves.cancel_worker n + +let query ~at s = + Future.purify (fun s -> + if Stateid.equal at Stateid.dummy then finish () + else Reach.known_state ~cache:`Yes at; + let _, ast as loc_ast = vernac_parse 0 s in + let clas = classify_vernac ast in + match clas with + | VtStm (w,_), _ -> + ignore(process_transaction + ~tty:false true (VtStm (w,false), VtNow) loc_ast) + | _ -> + ignore(process_transaction + ~tty:false true (VtQuery false, VtNow) loc_ast)) + s + +let add ~ontop ?(check=ignore) verb eid s = + let cur_tip = VCS.cur_tip () in + if Stateid.equal ontop cur_tip then begin + let _, ast as loc_ast = vernac_parse eid s in + check(loc_ast); + let clas = classify_vernac ast in + match process_transaction ~tty:false verb clas loc_ast with + | `Ok -> VCS.cur_tip (), `NewTip + | `Unfocus qed_id -> qed_id, `Unfocus (VCS.cur_tip ()) + end else begin + (* For now, arbitrary edits should be announced with edit_at *) + anomaly(str"Not yet implemented, the GUI should not try this") + end + +let set_perspective id_list = Slaves.set_perspective id_list + +type focus = { + start : Stateid.t; + stop : Stateid.t; + tip : Stateid.t +} + +let edit_at id = + if Stateid.equal id Stateid.dummy then anomaly(str"edit_at dummy") else + let vcs = VCS.backup () in + let on_cur_branch id = + let rec aux cur = + if id = cur then true + else match VCS.visit cur with + | { step = `Fork _ } -> false + | { next } -> aux next in + aux (VCS.get_branch_pos (VCS.current_branch ())) in + let is_ancestor_of_cur_branch id = + Vcs_.NodeSet.mem id + (VCS.reachable (VCS.get_branch_pos (VCS.current_branch ()))) in + let has_failed qed_id = + match VCS.visit qed_id with + | { step = `Qed ({ fproof = Some (fp,_) }, _) } -> Future.is_exn fp + | _ -> false in + let rec master_for_br root tip = + if Stateid.equal tip Stateid.initial then tip else + match VCS.visit tip with + | { next } when next = root -> root + | { step = `Fork _ } -> tip + | { step = `Sideff (`Ast(_,id)|`Id id) } -> id + | { next } -> master_for_br root next in + let reopen_branch at_id mode qed_id tip = + VCS.delete_cluster_of id; + let master_id = + match VCS.visit qed_id with + | { step = `Qed _; next = master_id } -> master_id + | _ -> anomaly (str "Cluster not ending with Qed") in + VCS.branch ~root:master_id ~pos:id + VCS.edit_branch (`Edit (mode, qed_id, master_id)); + Reach.known_state ~cache:(interactive ()) id; + VCS.checkout_shallowest_proof_branch (); + `Focus { stop = qed_id; start = master_id; tip } in + let backto id = + List.iter VCS.delete_branch (VCS.branches ()); + let ancestors = VCS.reachable id in + let { mine = brname, brinfo; others } = Backtrack.branches_of id in + List.iter (fun (name,{ VCS.kind = k; root; pos }) -> + if not(VCS.Branch.equal name VCS.Branch.master) && + Vcs_.NodeSet.mem root ancestors then + VCS.branch ~root ~pos name k) + others; + VCS.reset_branch VCS.Branch.master (master_for_br brinfo.VCS.root id); + VCS.branch ~root:brinfo.VCS.root ~pos:brinfo.VCS.pos brname brinfo.VCS.kind; + VCS.delete_cluster_of id; + VCS.gc (); + Reach.known_state ~cache:(interactive ()) id; + VCS.checkout_shallowest_proof_branch (); + `NewTip in + try + let rc = + let focused = List.exists ((=) VCS.edit_branch) (VCS.branches ()) in + let branch_info = + match snd (VCS.get_info id).vcs_backup with + | Some{ mine = _, { VCS.kind = (`Proof(m,_)|`Edit(m,_,_)) }} -> Some m + | _ -> None in + match focused, VCS.cluster_of id, branch_info with + | _, Some _, None -> assert false + | false, Some qed_id, Some mode -> + let tip = VCS.cur_tip () in + if has_failed qed_id then reopen_branch id mode qed_id tip + else backto id + | true, Some qed_id, Some mode -> + if on_cur_branch id then begin + assert false + end else if is_ancestor_of_cur_branch id then begin + backto id + end else begin + anomaly(str"Cannot leave an `Edit branch open") + end + | true, None, _ -> + if on_cur_branch id then begin + VCS.reset_branch (VCS.current_branch ()) id; + Reach.known_state ~cache:(interactive ()) id; + VCS.checkout_shallowest_proof_branch (); + `NewTip + end else if is_ancestor_of_cur_branch id then begin + backto id + end else begin + anomaly(str"Cannot leave an `Edit branch open") + end + | false, None, _ -> backto id + in + VCS.print (); + rc + with e -> + let e = Errors.push e in + match Stateid.get e with + | None -> + VCS.print (); + anomaly (str ("edit_at: "^string_of_ppcmds (Errors.print_no_report e))) + | Some (_, id) -> + prerr_endline ("Failed at state " ^ Stateid.to_string id); + VCS.restore vcs; + VCS.print (); + raise e +(* }}} *) + +(** Old tty interface {{{*************************************************** **) + +let interp verb (_,e as lexpr) = + let clas = classify_vernac e in + let rc = process_transaction ~tty:true verb clas lexpr in + if rc <> `Ok then anomaly(str"tty loop can't be mixed with the STM protocol"); + if interactive () = `Yes || + (!Flags.async_proofs_mode = Flags.APoff && + !Flags.compilation_mode = Flags.BuildVo) then + let vcs = VCS.backup () in + try finish () + with e -> + let e = Errors.push e in + handle_failure e vcs true + +let get_current_state () = VCS.cur_tip () + +let current_proof_depth () = + let head = VCS.current_branch () in + match VCS.get_branch head with + | { VCS.kind = `Master } -> 0 + | { VCS.pos = cur; VCS.kind = (`Proof _ | `Edit _); VCS.root = root } -> + let rec distance root = + if Stateid.equal cur root then 0 + else 1 + distance (VCS.visit cur).next in + distance cur + +let unmangle n = + let n = VCS.Branch.to_string n in + let idx = String.index n '_' + 1 in + Names.id_of_string (String.sub n idx (String.length n - idx)) + +let proofname b = match VCS.get_branch b with + | { VCS.kind = (`Proof _| `Edit _) } -> Some b + | _ -> None + +let get_all_proof_names () = + List.map unmangle (List.map_filter proofname (VCS.branches ())) + +let get_current_proof_name () = + Option.map unmangle (proofname (VCS.current_branch ())) + +let get_script prf = + let branch, test = + match prf with + | None -> VCS.Branch.master, fun _ -> true + | Some name -> VCS.current_branch (), List.mem name 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 (`Ast (x,_)) -> + find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next + | `Sideff (`Id id) -> find acc id + | `Cmd (x,_) -> find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next + | `Alias id -> find acc id + | `Fork _ -> find acc view.next + in + find [] (VCS.get_branch_pos branch) + +(* indentation code for Show Script, initially contributed + by D. de Rauglaudre *) + +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 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 = + (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 show_script ?proof () = + try + let prf = + try match proof with + | None -> Some (Pfedit.get_current_proof_name ()) + | Some (p,_) -> Some (p.Proof_global.id) + with Proof_global.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 (v 0 (Pp.prlist_with_sep Pp.fnl (fun x -> x) indented_cmds)) + with Vcs_aux.Expired -> () + +(* }}} *) + +(* vim:set foldmethod=marker: *) diff --git a/stm/stm.mli b/stm/stm.mli new file mode 100644 index 0000000000..a58100b5a0 --- /dev/null +++ b/stm/stm.mli @@ -0,0 +1,85 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* ?check:(located_vernac_expr -> unit) -> + bool -> edit_id -> string -> + Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] + +(* parses and xecutes a command at a given state, throws away its side effects + but for the printings *) +val query : at:Stateid.t -> string -> unit + +(* [edit_at id] is issued to change the editing zone. [`NewTip] is returned if + the requested id is the new document tip hence the document portion following + [id] is dropped by Coq. [`Focus fo] is returned to say that [fo.tip] is the + new document tip, the document between [id] and [fo.stop] has been dropped. + The portion between [fo.stop] and [fo.tip] has been kept. [fo.start] is + just to tell the gui where the editing zone starts, in case it wants to + graphically denote it. All subsequent [add] happen on top of [id]. *) +type focus = { start : Stateid.t; stop : Stateid.t; tip : Stateid.t } +val edit_at : Stateid.t -> [ `NewTip | `Focus of focus ] + +(* Evaluates the tip of the current branch *) +val finish : unit -> unit + +val stop_worker : int -> unit + +(* Joins the entire document. Implies finish, but also checks proofs *) +val join : unit -> unit +(* To save to disk an incomplete document *) +type tasks +val dump : (Future.UUID.t * int) list -> tasks + +val check_task : string -> tasks -> int -> bool +val info_tasks : tasks -> (string * float * int) list +val finish_tasks : string -> + Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs -> + tasks -> Library.seg_univ * Library.seg_proofs + +(* Id of the tip of the current branch *) +val get_current_state : unit -> Stateid.t + +(* Misc *) +val init : unit -> unit +val slave_main_loop : unit -> unit +val slave_init_stdout : unit -> unit + +(* Filename *) +val set_compilation_hints : string -> unit + +(* Reorders the task queue putting forward what is in the perspective *) +val set_perspective : Stateid.t list -> unit + +(** read-eval-print loop compatible interface ****************************** **) + +(* Adds a new line to the document. It replaces the core of Vernac.interp. + [finish] is called as the last bit of this function is the system + is running interactively (-emacs or coqtop). *) +val interp : bool -> located_vernac_expr -> unit + +(* Queries for backward compatibility *) +val current_proof_depth : unit -> int +val get_all_proof_names : unit -> Id.t list +val get_current_proof_name : unit -> Id.t option +val show_script : ?proof:Proof_global.closed_proof -> unit -> unit + +(** Reverse dependency hooks *) +val process_error_hook : (exn -> exn) Hook.t +val interp_hook : (?verbosely:bool -> ?proof:Proof_global.closed_proof -> + Loc.t * Vernacexpr.vernac_expr -> unit) Hook.t diff --git a/stm/stm.mllib b/stm/stm.mllib new file mode 100644 index 0000000000..347416099b --- /dev/null +++ b/stm/stm.mllib @@ -0,0 +1,9 @@ +Spawned +Dag +Vcs +TQueue +WorkerPool +Vernac_classifier +Lemmas +Stm +Vi_checking diff --git a/stm/tQueue.ml b/stm/tQueue.ml new file mode 100644 index 0000000000..783c545fd0 --- /dev/null +++ b/stm/tQueue.ml @@ -0,0 +1,64 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Queue.push x tq.queue) (List.sort rel !l); + Mutex.unlock tq.lock diff --git a/stm/tQueue.mli b/stm/tQueue.mli new file mode 100644 index 0000000000..a3ea5532fc --- /dev/null +++ b/stm/tQueue.mli @@ -0,0 +1,17 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'a t +val pop : 'a t -> 'a +val push : 'a t -> 'a -> unit +val reorder : 'a t -> ('a -> 'a -> int) -> unit +val wait_until_n_are_waiting_and_queue_empty : int -> 'a t -> unit +val dump : 'a t -> 'a list diff --git a/stm/vcs.ml b/stm/vcs.ml new file mode 100644 index 0000000000..e2513b1c1e --- /dev/null +++ b/stm/vcs.ml @@ -0,0 +1,193 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* t + val equal : t -> t -> bool + val compare : t -> t -> int + val to_string : t -> string + val master : t + end + + type id + + (* Branches have [branch_info] attached to them. *) + type ('kind) branch_info = { + kind : [> `Master] as 'kind; + root : id; + pos : id; + } + + type ('kind,'diff,'info) t constraint 'kind = [> `Master ] + + val empty : id -> ('kind,'diff,'info) t + + val current_branch : ('k,'e,'i) t -> Branch.t + val branches : ('k,'e,'i) t -> Branch.t list + + val get_branch : ('k,'e,'i) t -> Branch.t -> 'k branch_info + val reset_branch : ('k,'e,'i) t -> Branch.t -> id -> ('k,'e,'i) t + val branch : + ('kind,'e,'i) t -> ?root:id -> ?pos:id -> + Branch.t -> 'kind -> ('kind,'e,'i) t + val delete_branch : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t + val merge : + ('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> ?into:Branch.t -> + Branch.t -> ('k,'diff,'i) t + val commit : ('k,'diff,'i) t -> id -> 'diff -> ('k,'diff,'i) t + val rewrite_merge : + ('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> at:id -> + Branch.t -> ('k,'diff,'i) t + val checkout : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t + + val set_info : ('k,'e,'info) t -> id -> 'info -> ('k,'e,'info) t + val get_info : ('k,'e,'info) t -> id -> 'info option + + module NodeSet : Set.S with type elt = id + + val gc : ('k,'e,'info) t -> ('k,'e,'info) t * NodeSet.t + + val reachable : ('k,'e,'info) t -> id -> NodeSet.t + + module Dag : Dag.S with type node = id + val dag : ('kind,'diff,'info) t -> ('diff,'info,id) Dag.t + + val create_cluster : ('k,'e,'i) t -> id list -> id -> ('k,'e,'i) t + val cluster_of : ('k,'e,'i) t -> id -> id Dag.Cluster.t option + val delete_cluster : ('k,'e,'i) t -> id Dag.Cluster.t -> ('k,'e,'i) t + +end + +module Make(OT : Map.OrderedType) = struct + +module Dag = Dag.Make(OT) + +type id = OT.t + +module NodeSet = Dag.NodeSet + + +module Branch = +struct + type t = string + let make = + let bid = ref 0 in + fun s -> incr bid; string_of_int !bid ^ "_" ^ s + let equal = CString.equal + let compare = CString.compare + let to_string s = s + let master = "master" +end + +module BranchMap = Map.Make(Branch) + +type 'kind branch_info = { + kind : [> `Master] as 'kind; + root : id; + pos : id; +} + +type ('kind,'edge,'info) t = { + cur_branch : Branch.t; + heads : 'kind branch_info BranchMap.t; + dag : ('edge,'info,id) Dag.t; +} + +let empty root = { + cur_branch = Branch.master; + heads = BranchMap.singleton Branch.master { root = root; pos = root; kind = `Master }; + dag = Dag.empty; +} + +let add_node vcs id edges = + assert (not (CList.is_empty edges)); + { vcs with dag = + List.fold_left (fun g (t,tgt) -> Dag.add_edge g id t tgt) vcs.dag edges } + +let get_branch vcs head = + try BranchMap.find head vcs.heads + with Not_found -> anomaly (str"head " ++ str head ++ str" not found") + +let reset_branch vcs head id = + let map name h = + if Branch.equal name head then { h with pos = id } else h + in + { vcs with heads = BranchMap.mapi map vcs.heads; } + +let current_branch vcs = vcs.cur_branch + +let branch + vcs ?(root=(get_branch vcs vcs.cur_branch).pos) ?(pos=root) name kind += + { vcs with + heads = BranchMap.add name { kind; root; pos } vcs.heads; + cur_branch = name } + +let delete_branch vcs name = + if Branch.equal Branch.master name then vcs else + let filter n _ = not (Branch.equal n name) in + { vcs with heads = BranchMap.filter filter vcs.heads } + +let merge vcs id ~ours:tr1 ~theirs:tr2 ?(into = vcs.cur_branch) name = + assert (not (Branch.equal name into)); + let br_id = (get_branch vcs name).pos in + let cur_id = (get_branch vcs into).pos in + let vcs = add_node vcs id [tr1,cur_id; tr2,br_id] in + let vcs = reset_branch vcs into id in + vcs + +let del_edge id vcs tgt = { vcs with dag = Dag.del_edge vcs.dag id tgt } + +let rewrite_merge vcs id ~ours:tr1 ~theirs:tr2 ~at:cur_id name = + let br_id = (get_branch vcs name).pos in + let old_edges = List.map fst (Dag.from_node vcs.dag id) in + let vcs = List.fold_left (del_edge id) vcs old_edges in + let vcs = add_node vcs id [tr1,cur_id; tr2,br_id] in + vcs + +let commit vcs id tr = + let vcs = add_node vcs id [tr, (get_branch vcs vcs.cur_branch).pos] in + let vcs = reset_branch vcs vcs.cur_branch id in + vcs + +let checkout vcs name = { vcs with cur_branch = name } + +let set_info vcs id info = { vcs with dag = Dag.set_info vcs.dag id info } +let get_info vcs id = Dag.get_info vcs.dag id + +let create_cluster vcs l i = { vcs with dag = Dag.create_cluster vcs.dag l i } +let cluster_of vcs i = Dag.cluster_of vcs.dag i +let delete_cluster vcs c = { vcs with dag = Dag.del_cluster vcs.dag c } + +let branches vcs = BranchMap.fold (fun x _ accu -> x :: accu) vcs.heads [] +let dag vcs = vcs.dag + +let rec closure s d n = + let l = try Dag.from_node d n with Not_found -> [] in + List.fold_left (fun s (n',_) -> + if Dag.NodeSet.mem n' s then s + else closure s d n') + (Dag.NodeSet.add n s) l + +let reachable vcs i = closure Dag.NodeSet.empty vcs.dag i + +let gc vcs = + let alive = + BranchMap.fold (fun b { pos } s -> closure s vcs.dag pos) + vcs.heads Dag.NodeSet.empty in + let dead = Dag.NodeSet.diff (Dag.all_nodes vcs.dag) alive in + { vcs with dag = Dag.del_nodes vcs.dag dead }, dead + +end diff --git a/stm/vcs.mli b/stm/vcs.mli new file mode 100644 index 0000000000..6c3571a082 --- /dev/null +++ b/stm/vcs.mli @@ -0,0 +1,90 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* t + val equal : t -> t -> bool + val compare : t -> t -> int + val to_string : t -> string + val master : t + end + + type id + + type ('kind) branch_info = { + kind : [> `Master] as 'kind; + root : id; + pos : id; + } + + type ('kind,'diff,'info) t constraint 'kind = [> `Master ] + + val empty : id -> ('kind,'diff,'info) t + + val current_branch : ('k,'e,'i) t -> Branch.t + val branches : ('k,'e,'i) t -> Branch.t list + + val get_branch : ('k,'e,'i) t -> Branch.t -> 'k branch_info + val reset_branch : ('k,'e,'i) t -> Branch.t -> id -> ('k,'e,'i) t + val branch : + ('kind,'e,'i) t -> ?root:id -> ?pos:id -> + Branch.t -> 'kind -> ('kind,'e,'i) t + val delete_branch : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t + val merge : + ('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> ?into:Branch.t -> + Branch.t -> ('k,'diff,'i) t + val commit : ('k,'diff,'i) t -> id -> 'diff -> ('k,'diff,'i) t + val rewrite_merge : + ('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> at:id -> + Branch.t -> ('k,'diff,'i) t + val checkout : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t + + val set_info : ('k,'e,'info) t -> id -> 'info -> ('k,'e,'info) t + val get_info : ('k,'e,'info) t -> id -> 'info option + + module NodeSet : Set.S with type elt = id + + (* Removes all unreachable nodes and returns them *) + val gc : ('k,'e,'info) t -> ('k,'e,'info) t * NodeSet.t + + val reachable : ('k,'e,'info) t -> id -> NodeSet.t + + (* read only dag *) + module Dag : Dag.S with type node = id + val dag : ('kind,'diff,'info) t -> ('diff,'info,id) Dag.t + + val create_cluster : ('k,'e,'i) t -> id list -> id -> ('k,'e,'i) t + val cluster_of : ('k,'e,'i) t -> id -> id Dag.Cluster.t option + val delete_cluster : ('k,'e,'i) t -> id Dag.Cluster.t -> ('k,'e,'i) t + +end + +module Make(OT : Map.OrderedType) : S with type id = OT.t diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml new file mode 100644 index 0000000000..49cbcd246b --- /dev/null +++ b/stm/vernac_classifier.ml @@ -0,0 +1,189 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* "Unknown" + | VtStartProof _ -> "StartProof" + | VtSideff _ -> "Sideff" + | VtQed VtKeep -> "Qed(keep)" + | VtQed VtDrop -> "Qed(drop)" + | VtProofStep -> "ProofStep" + | VtProofMode s -> "ProofMode " ^ s + | VtQuery b -> "Query" ^ string_of_in_script b + | VtStm ((VtFinish|VtJoinDocument|VtObserve _|VtPrintDag|VtWait), b) -> + "Stm" ^ string_of_in_script b + | VtStm (VtPG, b) -> "Stm PG" ^ string_of_in_script b + | VtStm (VtBack _, b) -> "Stm Back" ^ string_of_in_script b + +let string_of_vernac_when = function + | VtLater -> "Later" + | VtNow -> "Now" + +let string_of_vernac_classification (t,w) = + string_of_vernac_type t ^ " " ^ string_of_vernac_when w + +let classifiers = ref [] +let declare_vernac_classifier + (s : string) + (f : Genarg.raw_generic_argument list -> unit -> vernac_classification) += + classifiers := !classifiers @ [s,f] + +let elide_part_of_script_and_now (a, _) = + match a with + | VtQuery _ -> VtQuery false, VtNow + | VtStm (x, _) -> VtStm (x, false), VtNow + | x -> x, VtNow + +let undo_classifier = ref (fun _ -> assert false) +let set_undo_classifier f = undo_classifier := f + +let rec classify_vernac e = + let static_classifier e = match e with + (* PG compatibility *) + | VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"]) + | VernacSetOption ((["Silent"]|["Undo"]|["Printing";"Depth"]),_) + when !Flags.print_emacs -> VtStm(VtPG,false), VtNow + (* Stm *) + | VernacStm Finish -> VtStm (VtFinish, true), VtNow + | VernacStm Wait -> VtStm (VtWait, true), VtNow + | VernacStm JoinDocument -> VtStm (VtJoinDocument, true), VtNow + | VernacStm PrintDag -> VtStm (VtPrintDag, true), VtNow + | VernacStm (Observe id) -> VtStm (VtObserve id, true), VtNow + | VernacStm (Command x) -> elide_part_of_script_and_now (classify_vernac x) + | VernacStm (PGLast x) -> fst (classify_vernac x), VtNow + (* Nested vernac exprs *) + | VernacProgram e -> classify_vernac e + | VernacLocal (_,e) -> classify_vernac e + | VernacTimeout (_,e) -> classify_vernac e + | VernacTime e -> classify_vernac e + | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) + (match classify_vernac e with + | ( VtQuery _ | VtProofStep | VtSideff _ + | VtStm _ | VtProofMode _ ), _ as x -> x + | VtQed _, _ -> VtProofStep, VtNow + | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow) + (* Qed *) + | VernacEndProof Admitted | VernacAbort _ -> VtQed VtDrop, VtLater + | VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater + (* Query *) + | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _ + | VernacCheckMayEval _ -> VtQuery true, VtLater + (* ProofStep *) + | VernacProof _ + | VernacBullet _ + | VernacFocus _ | VernacUnfocus + | VernacSubproof _ | VernacEndSubproof + | VernacSolve _ | VernacError _ + | VernacCheckGuard + | VernacUnfocused + | VernacSolveExistential _ -> VtProofStep, VtLater + (* Options changing parser *) + | VernacUnsetOption (["Default";"Proof";"Using"]) + | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow + (* StartProof *) + | VernacDefinition (_,(_,i),ProveBody _) -> + VtStartProof("Classic",GuaranteesOpacity,[i]), VtLater + | VernacStartTheoremProof (_,l,_) -> + let ids = + CList.map_filter (function (Some(_,i), _) -> Some i | _ -> None) l in + VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater + | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater + | VernacFixpoint (_,l) -> + let ids, open_proof = + List.fold_left (fun (l,b) (((_,id),_,_,_,p),_) -> + id::l, b || p = None) ([],false) l in + if open_proof then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater + else VtSideff ids, VtLater + | VernacCoFixpoint (_,l) -> + let ids, open_proof = + List.fold_left (fun (l,b) (((_,id),_,_,p),_) -> + id::l, b || p = None) ([],false) l in + if open_proof then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater + else VtSideff ids, VtLater + (* Sideff: apply to all open branches. usually run on master only *) + | VernacAssumption (_,_,l) -> + let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd l) l) in + VtSideff ids, VtLater + | VernacDefinition (_,(_,id),DefineBody _) -> VtSideff [id], VtLater + | VernacInductive (_,_,l) -> + let ids = List.map (fun (((_,(_,id)),_,_,_,cl),_) -> id :: match cl with + | Constructors l -> List.map (fun (_,((_,id),_)) -> id) l + | RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @ + CList.map_filter (function + | ((_,AssumExpr((_,Names.Name n),_)),_),_ -> Some n + | _ -> None) l) l in + VtSideff (List.flatten ids), VtLater + | VernacScheme l -> + let ids = List.map snd (CList.map_filter (fun (x,_) -> x) l) in + VtSideff ids, VtLater + | VernacCombinedScheme ((_,id),_) -> VtSideff [id], VtLater + | VernacBeginSection _ + | VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _ + | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _ + | VernacChdir _ + | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _ + | VernacDeclareImplicits _ | VernacArguments _ | VernacArgumentsScope _ + | VernacReserve _ + | VernacGeneralizable _ + | VernacSetOpacity _ | VernacSetStrategy _ + | VernacUnsetOption _ | VernacSetOption _ + | VernacAddOption _ | VernacRemoveOption _ + | VernacMemOption _ | VernacPrintOption _ + | VernacGlobalCheck _ + | VernacDeclareReduction _ + | VernacDeclareClass _ | VernacDeclareInstances _ + | VernacRegister _ + | VernacComments _ -> VtSideff [], VtLater + (* Who knows *) + | VernacList _ + | VernacLoad _ -> VtSideff [], VtNow + (* (Local) Notations have to disappear *) + | VernacEndSegment _ -> VtSideff [], VtNow + (* Modules with parameters have to be executed: can import notations *) + | VernacDeclareModule (exp,(_,id),bl,_) + | VernacDefineModule (exp,(_,id),bl,_,_) -> + VtSideff [id], if bl = [] && exp = None then VtLater else VtNow + | VernacDeclareModuleType ((_,id),bl,_,_) -> + VtSideff [id], if bl = [] then VtLater else VtNow + (* These commands alter the parser *) + | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _ + | VernacInfix _ | VernacNotation _ | VernacSyntaxExtension _ + | VernacSyntacticDefinition _ + | VernacDeclareTacticDefinition _ | VernacTacticNotation _ + | VernacRequire _ | VernacImport _ | VernacInclude _ + | VernacDeclareMLModule _ + | VernacContext _ (* TASSI: unsure *) + | VernacProofMode _ + (* These are ambiguous *) + | VernacInstance _ -> VtUnknown, VtNow + (* Stm will install a new classifier to handle these *) + | VernacBack _ | VernacAbortAll + | VernacUndoTo _ | VernacUndo _ + | VernacResetName _ | VernacResetInitial + | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> !undo_classifier e + (* What are these? *) + | VernacNop + | VernacToplevelControl _ + | VernacRestoreState _ + | VernacWriteState _ -> VtUnknown, VtNow + (* Plugins should classify their commands *) + | VernacExtend (s,l) -> + try List.assoc s !classifiers l () + with Not_found -> anomaly(str"No classifier for"++spc()++str s) + in + static_classifier e + +let classify_as_query = VtQuery true, VtLater +let classify_as_sideeff = VtSideff [], VtLater diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli new file mode 100644 index 0000000000..bc0c0c2b30 --- /dev/null +++ b/stm/vernac_classifier.mli @@ -0,0 +1,27 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* string + +(** What does a vernacular do *) +val classify_vernac : vernac_expr -> vernac_classification + +(** Install a vernacular classifier for VernacExtend *) +val declare_vernac_classifier : + string -> (raw_generic_argument list -> unit -> vernac_classification) -> unit + +(** Set by Stm *) +val set_undo_classifier : (vernac_expr -> vernac_classification) -> unit + +(** Standard constant classifiers *) +val classify_as_query : vernac_classification +val classify_as_sideeff : vernac_classification + diff --git a/stm/vi_checking.ml b/stm/vi_checking.ml new file mode 100644 index 0000000000..cb6e601362 --- /dev/null +++ b/stm/vi_checking.ml @@ -0,0 +1,152 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Stm.check_task f tasks ids && acc) true ts + +module Worker = Spawn.Sync(struct + let add_timeout ~sec f = + ignore(Thread.create (fun () -> + while true do + Unix.sleep sec; + if not (f ()) then Thread.exit () + done) + ()) +end) + +module IntOT = struct + type t = int + let compare = compare +end + +module Pool = Map.Make(IntOT) + +let schedule_vi_checking j fs = + if j < 1 then Errors.error "The number of workers must be bigger than 0"; + let jobs = ref [] in + List.iter (fun f -> + let f = + if Filename.check_suffix f ".vi" then Filename.chop_extension f + else f in + let long_f_dot_v, _,_,_, tasks, _ = Library.load_library_todo f in + Stm.set_compilation_hints long_f_dot_v; + let infos = Stm.info_tasks tasks in + let eta = List.fold_left (fun a (_,t,_) -> a +. t) 0.0 infos in + if infos <> [] then jobs := (f, eta, infos) :: !jobs) + fs; + let cmp_job (_,t1,_) (_,t2,_) = compare t2 t1 in + jobs := List.sort cmp_job !jobs; + let eta = ref (List.fold_left (fun a j -> a +. pi2 j) 0.0 !jobs) in + let pool : Worker.process Pool.t ref = ref Pool.empty in + let rec filter_argv b = function + | [] -> [] + | "-schedule-vi-checking" :: rest -> filter_argv true rest + | s :: rest when s.[0] = '-' && b -> filter_argv false (s :: rest) + | _ :: rest when b -> filter_argv b rest + | s :: rest -> s :: filter_argv b rest in + let pack = function + | [] -> [] + | ((f,_),_,_) :: _ as l -> + let rec aux last acc = function + | [] -> [last,acc] + | ((f',id),_,_) :: tl when last = f' -> aux last (id::acc) tl + | ((f',id),_,_) :: _ as l -> (last,acc) :: aux f' [] l in + aux f [] l in + let prog = Sys.argv.(0) in + let stdargs = filter_argv false (List.tl (Array.to_list Sys.argv)) in + let make_job () = + let cur = ref 0.0 in + let what = ref [] in + let j_left = j - Pool.cardinal !pool in + let take_next_file () = + let f, t, tasks = List.hd !jobs in + jobs := List.tl !jobs; + cur := !cur +. t; + what := (List.map (fun (n,t,id) -> (f,id),n,t) tasks) @ !what in + if List.length !jobs >= j_left then take_next_file () + else while !jobs <> [] && + !cur < max 0.0 (min 60.0 (!eta /. float_of_int j_left)) do + let f, t, tasks = List.hd !jobs in + jobs := List.tl !jobs; + let n, tt, id = List.hd tasks in + if List.length tasks > 1 then + jobs := (f, t -. tt, List.tl tasks) :: !jobs; + cur := !cur +. tt; + what := ((f,id),n,tt) :: !what; + done; + if !what = [] then take_next_file (); + eta := !eta -. !cur; + let cmp_job (f1,_,_) (f2,_,_) = compare f1 f2 in + List.flatten + (List.map (fun (f, tl) -> + "-check-vi-tasks" :: + String.concat "," (List.map string_of_int tl) :: [f]) + (pack (List.sort cmp_job !what))) in + let rc = ref 0 in + while !jobs <> [] || Pool.cardinal !pool > 0 do + while Pool.cardinal !pool < j && !jobs <> [] do + let args = Array.of_list (stdargs @ make_job ()) in + let proc, _, _ = Worker.spawn prog args in + pool := Pool.add (Worker.unixpid proc) proc !pool; + done; + let pid, ret = Unix.wait () in + if ret <> Unix.WEXITED 0 then rc := 1; + pool := Pool.remove pid !pool; + done; + exit !rc + +let schedule_vi_compilation j fs = + if j < 1 then Errors.error "The number of workers must be bigger than 0"; + let jobs = ref [] in + List.iter (fun f -> + let f = + if Filename.check_suffix f ".vi" then Filename.chop_extension f + else f in + let paths = Loadpath.get_paths () in + let _, long_f_dot_v = + System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in + let aux = Aux_file.load_aux_file_for long_f_dot_v in + let eta = + try float_of_string (Aux_file.get aux Loc.ghost "vo_compile_time") + with Not_found -> 0.0 in + jobs := (f, eta) :: !jobs) + fs; + let cmp_job (_,t1) (_,t2) = compare t2 t1 in + jobs := List.sort cmp_job !jobs; + let pool : Worker.process Pool.t ref = ref Pool.empty in + let rec filter_argv b = function + | [] -> [] + | "-schedule-vi2vo" :: rest -> filter_argv true rest + | s :: rest when s.[0] = '-' && b -> filter_argv false (s :: rest) + | _ :: rest when b -> filter_argv b rest + | s :: rest -> s :: filter_argv b rest in + let prog = Sys.argv.(0) in + let stdargs = filter_argv false (List.tl (Array.to_list Sys.argv)) in + let make_job () = + let f, t = List.hd !jobs in + jobs := List.tl !jobs; + [ "-vi2vo"; f ] in + let rc = ref 0 in + while !jobs <> [] || Pool.cardinal !pool > 0 do + while Pool.cardinal !pool < j && !jobs <> [] do + let args = Array.of_list (stdargs @ make_job ()) in + let proc, _, _ = Worker.spawn prog args in + pool := Pool.add (Worker.unixpid proc) proc !pool; + done; + let pid, ret = Unix.wait () in + if ret <> Unix.WEXITED 0 then rc := 1; + pool := Pool.remove pid !pool; + done; + exit !rc + + diff --git a/stm/vi_checking.mli b/stm/vi_checking.mli new file mode 100644 index 0000000000..65414eda41 --- /dev/null +++ b/stm/vi_checking.mli @@ -0,0 +1,13 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* bool +val schedule_vi_checking : int -> string list -> unit + +val schedule_vi_compilation : int -> string list -> unit diff --git a/stm/workerPool.ml b/stm/workerPool.ml new file mode 100644 index 0000000000..fcae4f20d6 --- /dev/null +++ b/stm/workerPool.ml @@ -0,0 +1,73 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* ?env:string array -> string -> string array -> + process * in_channel * out_channel +end) = struct + +type worker_id = int +type spawn = + args:string array -> env:string array -> unit -> + in_channel * out_channel * Worker.process + +let slave_managers = ref None + +let n_workers () = match !slave_managers with + | None -> 0 + | Some managers -> Array.length managers +let is_empty () = !slave_managers = None + +let magic_no = 17 + +let master_handshake worker_id ic oc = + try + Marshal.to_channel oc magic_no []; flush oc; + let n = (Marshal.from_channel ic : int) in + if n <> magic_no then begin + Printf.eprintf "Handshake with %d failed: protocol mismatch\n" worker_id; + exit 1; + end + with e when Errors.noncritical e -> + Printf.eprintf "Handshake with %d failed: %s\n" + worker_id (Printexc.to_string e); + exit 1 + +let respawn n ~args ~env () = + let proc, ic, oc = Worker.spawn ~env Sys.argv.(0) args in + master_handshake n ic oc; + ic, oc, proc + +let init ~size:n ~manager:manage_slave = + slave_managers := Some + (Array.init n (fun x -> + let cancel = ref false in + cancel, Thread.create (manage_slave ~cancel (x+1)) (respawn (x+1)))) + +let cancel n = + match !slave_managers with + | None -> () + | Some a -> + let switch, _ = a.(n) in + switch := true + +let worker_handshake slave_ic slave_oc = + try + let v = (Marshal.from_channel slave_ic : int) in + if v <> magic_no then begin + prerr_endline "Handshake failed: protocol mismatch\n"; + exit 1; + end; + Marshal.to_channel slave_oc v []; flush slave_oc; + with e when Errors.noncritical e -> + prerr_endline ("Handshake failed: " ^ Printexc.to_string e); + exit 1 + +end diff --git a/stm/workerPool.mli b/stm/workerPool.mli new file mode 100644 index 0000000000..d7a546929f --- /dev/null +++ b/stm/workerPool.mli @@ -0,0 +1,30 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* ?env:string array -> string -> string array -> + process * in_channel * out_channel +end) : sig + +type worker_id = int +type spawn = + args:string array -> env:string array -> unit -> + in_channel * out_channel * Worker.process + +val init : + size:int -> manager:(cancel:bool ref -> worker_id -> spawn -> unit) -> unit +val is_empty : unit -> bool +val n_workers : unit -> int +val cancel : worker_id -> unit + +(* The worker should call this function *) +val worker_handshake : in_channel -> out_channel -> unit + +end diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml deleted file mode 100644 index 8f16ad5a4b..0000000000 --- a/toplevel/lemmas.ml +++ /dev/null @@ -1,431 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - (pi2 (Global.lookup_named id),variable_opacity id) - | ConstRef cst -> - let cb = Global.lookup_constant cst in - (body_of_constant cb, is_opaque cb) - | _ -> assert false - -let adjust_guardness_conditions const = function - | [] -> const (* Not a recursive statement *) - | possible_indexes -> - (* Try all combinations... not optimal *) - let env = Global.env() in - { const with const_entry_body = - Future.chain ~greedy:true ~pure:true const.const_entry_body - (fun (body, eff) -> - match kind_of_term body with - | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> -(* let possible_indexes = - List.map2 (fun i c -> match i with Some i -> i | None -> - List.interval 0 (List.length ((lam_assum c)))) - lemma_guard (Array.to_list fixdefs) in -*) - let indexes = - search_guard Loc.ghost env - possible_indexes fixdecls in - mkFix ((indexes,0),fixdecls), eff - | _ -> body, eff) } - -let find_mutually_recursive_statements thms = - let n = List.length thms in - let inds = List.map (fun (id,(t,impls,annot)) -> - let (hyps,ccl) = decompose_prod_assum t in - let x = (id,(t,impls)) in - match annot with - (* Explicit fixpoint decreasing argument is given *) - | Some (Some (_,id),CStructRec) -> - let i,b,typ = lookup_rel_id id hyps in - (match kind_of_term t with - | Ind (kn,_ as ind) when - let mind = Global.lookup_mind kn in - mind.mind_finite && Option.is_empty b -> - [ind,x,i],[] - | _ -> - error "Decreasing argument is not an inductive assumption.") - (* Unsupported cases *) - | Some (_,(CWfRec _|CMeasureRec _)) -> - error "Only structural decreasing is supported for mutual statements." - (* Cofixpoint or fixpoint w/o explicit decreasing argument *) - | None | Some (None, CStructRec) -> - let whnf_hyp_hds = map_rel_context_in_env - (fun env c -> fst (whd_betadeltaiota_stack env Evd.empty c)) - (Global.env()) hyps in - let ind_hyps = - List.flatten (List.map_i (fun i (_,b,t) -> - match kind_of_term t with - | Ind (kn,_ as ind) when - let mind = Global.lookup_mind kn in - mind.mind_finite && Option.is_empty b -> - [ind,x,i] - | _ -> - []) 0 (List.rev whnf_hyp_hds)) in - let ind_ccl = - let cclenv = push_rel_context hyps (Global.env()) in - let whnf_ccl,_ = whd_betadeltaiota_stack cclenv Evd.empty ccl in - match kind_of_term whnf_ccl with - | Ind (kn,_ as ind) when - let mind = Global.lookup_mind kn in - Int.equal mind.mind_ntypes n && not mind.mind_finite -> - [ind,x,0] - | _ -> - [] in - ind_hyps,ind_ccl) thms in - let inds_hyps,ind_ccls = List.split inds in - let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> eq_mind kn kn' in - (* Check if all conclusions are coinductive in the same type *) - (* (degenerated cartesian product since there is at most one coind ccl) *) - let same_indccl = - List.cartesians_filter (fun hyp oks -> - if List.for_all (of_same_mutind hyp) oks - then Some (hyp::oks) else None) [] ind_ccls in - let ordered_same_indccl = - List.filter (List.for_all_i (fun i ((kn,j),_,_) -> Int.equal i j) 0) same_indccl in - (* Check if some hypotheses are inductive in the same type *) - let common_same_indhyp = - List.cartesians_filter (fun hyp oks -> - if List.for_all (of_same_mutind hyp) oks - then Some (hyp::oks) else None) [] inds_hyps in - let ordered_inds,finite,guard = - match ordered_same_indccl, common_same_indhyp with - | indccl::rest, _ -> - assert (List.is_empty rest); - (* One occ. of common coind ccls and no common inductive hyps *) - if not (List.is_empty common_same_indhyp) then - if_verbose msg_info (str "Assuming mutual coinductive statements."); - flush_all (); - indccl, true, [] - | [], _::_ -> - let () = match same_indccl with - | ind :: _ -> - if List.distinct_f ind_ord (List.map pi1 ind) - then - if_verbose msg_info - (strbrk - ("Coinductive statements do not follow the order of "^ - "definition, assuming the proof to be by induction.")); - flush_all () - | _ -> () - in - let possible_guards = List.map (List.map pi3) inds_hyps in - (* assume the largest indices as possible *) - List.last common_same_indhyp, false, possible_guards - | _, [] -> - error - ("Cannot find common (mutual) inductive premises or coinductive" ^ - " conclusions in the statements.") - in - (finite,guard,None), ordered_inds - -let look_for_possibly_mutual_statements = function - | [id,(t,impls,None)] -> - (* One non recursively proved theorem *) - None,[id,(t,impls)],None - | _::_ as thms -> - (* More than one statement and/or an explicit decreasing mark: *) - (* we look for a common inductive hyp or a common coinductive conclusion *) - let recguard,ordered_inds = find_mutually_recursive_statements thms in - let thms = List.map pi2 ordered_inds in - Some recguard,thms, Some (List.map (fun (_,_,i) -> succ i) ordered_inds) - | [] -> anomaly (Pp.str "Empty list of theorems.") - -(* Saving a goal *) - -let save id const do_guard (locality,kind) hook = - let const = adjust_guardness_conditions const do_guard in - let k = Kindops.logical_kind_of_goal_kind kind in - let l,r = match locality with - | Discharge when Lib.sections_are_opened () -> - let c = SectionLocalDef const in - let _ = declare_variable id (Lib.cwd(), c, k) in - (Local, VarRef id) - | Local | Global | Discharge -> - let local = match locality with - | Local | Discharge -> true - | Global -> false - in - let kn = declare_constant id ~local (DefinitionEntry const, k) in - (locality, ConstRef kn) in - definition_message id; - hook l r - -let default_thm_id = Id.of_string "Unnamed_thm" - -let compute_proof_name locality = function - | Some (loc,id) -> - (* We check existence here: it's a bit late at Qed time *) - if Nametab.exists_cci (Lib.make_path id) || is_section_variable id || - locality == Global && Nametab.exists_cci (Lib.make_path_except_section id) - then - user_err_loc (loc,"",pr_id id ++ str " already exists."); - id - | None -> - next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()) - -let save_remaining_recthms (locality,kind) body opaq i (id,(t_i,(_,imps))) = - match body with - | None -> - (match locality with - | Discharge -> - let impl = false in (* copy values from Vernacentries *) - let k = IsAssumption Conjectural in - let c = SectionLocalAssum (t_i,impl) in - let _ = declare_variable id (Lib.cwd(),c,k) in - (Discharge, VarRef id,imps) - | Local | Global -> - let k = IsAssumption Conjectural in - let local = match locality with - | Local -> true - | Global -> false - | Discharge -> assert false - in - let decl = (ParameterEntry (None,t_i,None), k) in - let kn = declare_constant id ~local decl in - (locality,ConstRef kn,imps)) - | Some body -> - let k = Kindops.logical_kind_of_goal_kind kind in - let body_i = match kind_of_term body with - | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) - | CoFix (0,decls) -> mkCoFix (i,decls) - | _ -> anomaly (Pp.str "Not a proof by induction") in - match locality with - | Discharge -> - let const = { const_entry_body = - Future.from_val (body_i,Declareops.no_seff); - const_entry_secctx = None; - const_entry_type = Some t_i; - const_entry_opaque = opaq; - const_entry_inline_code = false; - const_entry_feedback = None; - } in - let c = SectionLocalDef const in - let _ = declare_variable id (Lib.cwd(), c, k) in - (Discharge,VarRef id,imps) - | Local | Global -> - let local = match locality with - | Local -> true - | Global -> false - | Discharge -> assert false - in - let const = { const_entry_body = - Future.from_val (body_i,Declareops.no_seff); - const_entry_secctx = None; - const_entry_type = Some t_i; - const_entry_opaque = opaq; - const_entry_inline_code = false; - const_entry_feedback = None; - } in - let kn = declare_constant id ~local (DefinitionEntry const, k) in - (locality,ConstRef kn,imps) - -let save_hook = ref ignore -let set_save_hook f = save_hook := f - -let save_named proof = - let id,const,do_guard,persistence,hook = proof in - save id const do_guard persistence hook - -let check_anonymity id save_ident = - if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then - error "This command can only be used for unnamed theorem." - - -let save_anonymous proof save_ident = - let id,const,do_guard,persistence,hook = proof in - check_anonymity id save_ident; - save save_ident const do_guard persistence hook - -let save_anonymous_with_strength proof kind save_ident = - let id,const,do_guard,_,hook = proof in - check_anonymity id save_ident; - (* we consider that non opaque behaves as local for discharge *) - save save_ident const do_guard (Global, Proof kind) hook - -(* Admitted *) - -let admit hook () = - let (id,k,typ) = Pfedit.current_proof_statement () in - let e = Pfedit.get_used_variables(), typ, None in - let kn = declare_constant id (ParameterEntry e,IsAssumption Conjectural) in - let () = match fst k with - | Global -> () - | Local | Discharge -> - msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++ - str "declared as an axiom.") - in - let () = assumption_message id in - hook Global (ConstRef kn) - -(* Starting a goal *) - -let start_hook = ref ignore -let set_start_hook = (:=) start_hook - - -let get_proof proof do_guard hook opacity = - let (id,(const,persistence)) = - Pfedit.cook_this_proof proof - in - id,{const with const_entry_opaque = opacity},do_guard,persistence,hook - -let standard_proof_terminator compute_guard hook = - let open Proof_global in function - | Admitted -> - admit hook (); - Pp.feedback Interface.AddedAxiom - | Proved (is_opaque,idopt,proof) -> - let proof = get_proof proof compute_guard hook is_opaque in - begin match idopt with - | None -> save_named proof - | Some ((_,id),None) -> save_anonymous proof id - | Some ((_,id),Some kind) -> - save_anonymous_with_strength proof kind id - end - -let start_proof id kind ?sign c ?init_tac ?(compute_guard=[]) hook = - let terminator = standard_proof_terminator compute_guard hook in - let sign = - match sign with - | Some sign -> sign - | None -> initialize_named_context_for_proof () - in - !start_hook c; - Pfedit.start_proof id kind sign c ?init_tac terminator - - -let rec_tac_initializer finite guard thms snl = - if finite then - match List.map (fun (id,(t,_)) -> (id,t)) thms with - | (id,_)::l -> Tactics.mutual_cofix id l 0 - | _ -> assert false - else - (* nl is dummy: it will be recomputed at Qed-time *) - let nl = match snl with - | None -> List.map succ (List.map List.last guard) - | Some nl -> nl - in match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with - | (id,n,_)::l -> Tactics.mutual_fix id n l 0 - | _ -> assert false - -let start_proof_with_initialization kind recguard thms snl hook = - let intro_tac (_, (_, (ids, _))) = - Tacticals.New.tclMAP (function - | Name id -> Tactics.intro_mustbe_force id - | Anonymous -> Tactics.intro) (List.rev ids) in - let init_tac,guard = match recguard with - | Some (finite,guard,init_tac) -> - let rec_tac = Proofview.V82.tactic (rec_tac_initializer finite guard thms snl) in - Some (match init_tac with - | None -> - if Flags.is_auto_intros () then - Tacticals.New.tclTHENS rec_tac (List.map intro_tac thms) - else - rec_tac - | Some tacl -> - Tacticals.New.tclTHENS rec_tac - (if Flags.is_auto_intros () then - List.map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms - else - tacl)),guard - | None -> - let () = match thms with [_] -> () | _ -> assert false in - (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in - match thms with - | [] -> anomaly (Pp.str "No proof to start") - | (id,(t,(_,imps)))::other_thms -> - let hook strength ref = - let other_thms_data = - if List.is_empty other_thms then [] else - (* there are several theorems defined mutually *) - let body,opaq = retrieve_first_recthm ref in - List.map_i (save_remaining_recthms kind body opaq) 1 other_thms in - let thms_data = (strength,ref,imps)::other_thms_data in - List.iter (fun (strength,ref,imps) -> - maybe_declare_manual_implicits false ref imps; - hook strength ref) thms_data in - start_proof id kind t ?init_tac hook ~compute_guard:guard - -let start_proof_com kind thms hook = - let evdref = ref Evd.empty in - let env0 = Global.env () in - let thms = List.map (fun (sopt,(bl,t,guard)) -> - let impls, ((env, ctx), imps) = interp_context_evars evdref env0 bl in - let t', imps' = interp_type_evars_impls ~impls evdref env t in - check_evars_are_solved env Evd.empty !evdref; - let ids = List.map pi1 ctx in - (compute_proof_name (fst kind) sopt, - (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), - (ids, imps @ lift_implicits (List.length ids) imps'), - guard))) - thms in - let recguard,thms,snl = look_for_possibly_mutual_statements thms in - start_proof_with_initialization kind recguard thms snl hook - - -(* Saving a proof *) - -let save_proof ?proof = function - | Vernacexpr.Admitted -> - Proof_global.get_terminator() Proof_global.Admitted - | Vernacexpr.Proved (is_opaque,idopt) -> - let (proof_obj,terminator) = - match proof with - | None -> Proof_global.close_proof (fun x -> x) - | Some proof -> proof - in - (* if the proof is given explicitly, nothing has to be deleted *) - if Option.is_empty proof then Pfedit.delete_current_proof (); - terminator (Proof_global.Proved (is_opaque,idopt,proof_obj)) - -(* Miscellaneous *) - -let get_current_context () = - try Pfedit.get_current_goal_context () - with e when Logic.catchable_exception e -> - (Evd.empty, Global.env()) - - - - - - - - - - diff --git a/toplevel/lemmas.mli b/toplevel/lemmas.mli deleted file mode 100644 index bbe383a857..0000000000 --- a/toplevel/lemmas.mli +++ /dev/null @@ -1,50 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit) -> unit - -val start_proof : Id.t -> goal_kind -> ?sign:Environ.named_context_val -> types -> - ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> - unit declaration_hook -> unit - -val start_proof_com : goal_kind -> - (lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)) list -> - unit declaration_hook -> unit - -val start_proof_with_initialization : - goal_kind -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option -> - (Id.t * (types * (Name.t list * Impargs.manual_explicitation list))) list - -> int list option -> unit declaration_hook -> unit - -val standard_proof_terminator : - Proof_global.lemma_possible_guards -> unit declaration_hook -> - Proof_global.proof_terminator - -(** {6 ... } *) - -(** A hook the next three functions pass to cook_proof *) -val set_save_hook : (Proof.proof -> unit) -> unit - -val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit - - -(** [get_current_context ()] returns the evar context and env of the - current open proof if any, otherwise returns the empty evar context - and the current global env *) - -val get_current_context : unit -> Evd.evar_map * Environ.env - diff --git a/toplevel/stm.ml b/toplevel/stm.ml deleted file mode 100644 index cc6b7d0c40..0000000000 --- a/toplevel/stm.ml +++ /dev/null @@ -1,2072 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - "master" ^ string_of_int (Thread.id (Thread.self ())) - | Flags.APonParallel n -> "worker" ^ string_of_int n - -let pr_err s = Printf.eprintf "%s] %s\n" (process_id ()) s; flush stderr - -let prerr_endline s = if !Flags.debug then begin pr_err s end else () - -open Vernacexpr -open Errors -open Pp -open Names -open Util -open Ppvernac -open Vernac_classifier - -(* During interactive use we cache more states so that Undoing is fast *) -let interactive () = - if !Flags.ide_slave || !Flags.print_emacs || not !Flags.batch_mode then `Yes - else `No - -let fallback_to_lazy_if_marshal_error = ref true -let fallback_to_lazy_if_slave_dies = ref true -let async_proofs_workers_extra_env = ref [||] - -type ast = { verbose : bool; loc : Loc.t; mutable expr : vernac_expr } -let pr_ast { expr } = pr_vernac expr - -(* Wrapper for Vernacentries.interp to set the feedback id *) -let vernac_interp ?proof id { verbose; loc; expr } = - let internal_command = function - | VernacResetName _ | VernacResetInitial | VernacBack _ - | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _ - | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true | _ -> false in - if internal_command expr then begin - prerr_endline ("ignoring " ^ string_of_ppcmds(pr_vernac expr)) - end else begin - Pp.set_id_for_feedback (Interface.State id); - Aux_file.record_in_aux_set_at loc; - prerr_endline ("interpreting " ^ string_of_ppcmds(pr_vernac expr)); - try Vernacentries.interp ~verbosely:verbose ?proof (loc, expr) - with e -> - let e = Errors.push e in - raise (Cerrors.process_vernac_interp_error e) - end - -(* Wrapper for Vernac.parse_sentence to set the feedback id *) -let vernac_parse eid s = - set_id_for_feedback (Interface.Edit eid); - let pa = Pcoq.Gram.parsable (Stream.of_string s) in - Flags.with_option Flags.we_are_parsing (fun () -> - match Pcoq.Gram.entry_parse Pcoq.main_entry pa with - | None -> raise (Invalid_argument "vernac_parse") - | Some ast -> ast) - () - -module Vcs_ = Vcs.Make(Stateid) -type future_proof = Entries.proof_output list Future.computation -type proof_mode = string -type depth = int -type cancel_switch = bool ref -type branch_type = - [ `Master - | `Proof of proof_mode * depth - | `Edit of proof_mode * Stateid.t * Stateid.t ] -type cmd_t = ast * Id.t list -type fork_t = ast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Id.t list -type qed_t = { - qast : ast; - keep : vernac_qed_type; - mutable fproof : (future_proof * cancel_switch) option; - brname : Vcs_.Branch.t; - brinfo : branch_type Vcs_.branch_info -} -type seff_t = ast option -type alias_t = Stateid.t -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 - | `Qed of qed_t * Stateid.t - | `Sideff of [ `Ast of ast * Stateid.t | `Id of Stateid.t ] - | `Alias of alias_t ] -type visit = { step : step; next : Stateid.t } - -type state = { - system : States.state; - proof : Proof_global.state; - shallow : bool -} -type branch = Vcs_.Branch.t * branch_type Vcs_.branch_info -type backup = { mine : branch; others : branch list } -type 'vcs state_info = { (* Make private *) - mutable n_reached : int; - mutable n_goals : int; - mutable state : state option; - mutable vcs_backup : 'vcs option * backup option; -} -let default_info () = - { n_reached = 0; n_goals = 0; state = None; vcs_backup = None,None } - -(* Functions that work on a Vcs with a specific branch type *) -module Vcs_aux : sig - - val proof_nesting : (branch_type, 't,'i) Vcs_.t -> int - val find_proof_at_depth : - (branch_type, 't, 'i) Vcs_.t -> int -> - Vcs_.Branch.t * branch_type Vcs_.branch_info - exception Expired - val visit : (branch_type, transaction,'i) Vcs_.t -> Vcs_.Dag.node -> visit - -end = struct (* {{{ *) - - let proof_nesting vcs = - List.fold_left max 0 - (List.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(m, n) } -> Int.equal n pl - | _, { Vcs_.kind = `Edit _ } -> anomaly(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(str"Visiting the initial state id") - else if Stateid.equal id Stateid.dummy then - anomaly(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; next = n } - | [n, Qed x; p, Noop] - | [p, Noop; n, Qed x] -> { step = `Qed (x,p); next = n } - | [n, Sideff None; p, Noop] - | [p, Noop; n, Sideff None]-> { step = `Sideff (`Id p); next = n } - | [n, Sideff (Some x); p, Noop] - | [p, Noop; n, Sideff (Some x)]-> { step = `Sideff(`Ast (x,p)); next = n } - | [n, Sideff (Some x)]-> {step = `Sideff(`Ast (x,Stateid.dummy)); next=n} - | _ -> anomaly (str ("Malformed VCS at node "^Stateid.to_string id)) - with Not_found -> raise Expired - -end (* }}} *) - -(* Imperative wrap around VCS to obtain _the_ VCS *) -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) Vcs_.t - - val init : id -> unit - - 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 : 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 : ast -> 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 -> Vcs_.NodeSet.t - val cur_tip : unit -> id - - val get_info : id -> vcs state_info - val reached : id -> bool -> unit - val goals : id -> int -> unit - val set_state : id -> state -> unit - val get_state : id -> state option - val forget_state : id -> unit - - (* cuts from start -> stop, raising Expired if some nodes are not there *) - val slice : start:id -> stop:id -> vcs - - val create_cluster : id list -> tip:id -> unit - val cluster_of : id -> id option - val delete_cluster_of : id -> unit - - val proof_nesting : unit -> int - val checkout_shallowest_proof_branch : unit -> unit - val propagate_sideff : ast option -> 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 - - module StateidSet = Set.Make(Stateid) - open Printf - - let print_dag vcs () = (* {{{ *) - let fname = "stm_" ^ process_id () in - let string_of_transaction = function - | Cmd (t, _) | Fork (t, _,_,_) -> - (try string_of_ppcmds (pr_ast t) with _ -> "ERR") - | Sideff (Some t) -> - sprintf "Sideff(%s)" - (try string_of_ppcmds (pr_ast t) with _ -> "ERR") - | Sideff None -> "EnvChange" - | Noop -> " " - | Alias id -> sprintf "Alias(%s)" (Stateid.to_string id) - | Qed { qast } -> string_of_ppcmds (pr_ast qast) in - let is_green id = - match get_info vcs id with - | Some { state = Some _ } -> true - | _ -> false in - let is_red id = - match get_info vcs id with - | Some s -> Int.equal s.n_reached ~-1 - | _ -> 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 "<%s>" - (quote (string_of_transaction tr)) in - let ids = ref StateidSet.empty in - let clus = Hashtbl.create 13 in - let node_info id = - match get_info vcs id with - | None -> "" - | Some info -> - sprintf "<%s" (Stateid.to_string id) ^ - sprintf " 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 add_to_clus_or_ids from cf = - match cf with - | None -> ids := StateidSet.add from !ids; false - | Some c -> Hashtbl.replace clus c - (try let n = Hashtbl.find clus c in from::n - with Not_found -> [from]); true in - let oc = open_out fname_dot in - output_string oc "digraph states {\nsplines=ortho\n"; - Dag.iter graph (fun from cf _ l -> - let c1 = add_to_clus_or_ids from cf in - List.iter (fun (dest, trans) -> - let c2 = add_to_clus_or_ids dest (Dag.cluster_of graph dest) in - fprintf oc "%s -> %s [label=%s,labelfloat=%b];\n" - (node from) (node dest) (edge trans) (c1 && c2)) l - ); - StateidSet.iter (nodefmt oc) !ids; - Hashtbl.iter (fun c nodes -> - fprintf oc "subgraph cluster_%s {\n" (Dag.Cluster.to_string c); - List.iter (nodefmt oc) nodes; - fprintf oc "color=blue; }\n" - ) clus; - 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) t - let vcs : vcs ref = ref (empty Stateid.dummy) - - let init id = - vcs := empty id; - vcs := set_info !vcs id (default_info ()) - - 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 () = - let id = Stateid.fresh () in - vcs := set_info !vcs id (default_info ()); - 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 x with - | VernacDefinition (_,(_,i),_) -> string_of_id i - | VernacStartTheoremProof (_,[Some (_,i),_],_) -> string_of_id 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 = (get_info id).state <- Some s - let get_state id = (get_info id).state - let forget_state id = (get_info id).state <- None - let reached id b = - let info = get_info id in - if b then info.n_reached <- info.n_reached + 1 - else 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; - match get_branch edit_branch with - | { kind = `Edit (mode, _, _) } -> Proof_global.activate_proof_mode mode - | _ -> assert false - end else - let pl = proof_nesting () in - try - let branch, mode = match Vcs_aux.find_proof_at_depth !vcs pl with - | h, { Vcs_.kind = `Proof (m, _) } -> h, m | _ -> assert false in - checkout branch; - prerr_endline ("mode:" ^ mode); - Proof_global.activate_proof_mode mode - with Failure _ -> - checkout Branch.master; - Proof_global.disactivate_proof_mode "Classic" - - (* copies the transaction on every open branch *) - let propagate_sideff t = - List.iter (fun b -> - checkout b; - let id = new_node () in - merge id ~ours:(Sideff t) ~into:b Branch.master) - (List.filter (fun b -> not (Branch.equal b Branch.master)) (branches ())) - - let visit id = Vcs_aux.visit !vcs id - - let slice ~start ~stop = - let l = - let rec aux id = - if Stateid.equal id stop 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 (`Ast (x,_)) } -> - (id,Sideff (Some x)) :: aux n - | _ -> anomaly(str("Cannot slice from "^ Stateid.to_string start ^ - " to "^Stateid.to_string stop)) - in aux start in - let copy_info v id = - Vcs_.set_info v id - { (get_info id) with state = None; vcs_backup = None,None } in - let copy_info_w_state v id = - Vcs_.set_info v id { (get_info id) with vcs_backup = None,None } in - let v = Vcs_.empty stop in - let v = copy_info v stop 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 (not (Option.is_empty (get_info stop).state)); - (* We put in the new dag the most recent state known to master *) - let rec fill id = - if (get_info id).state = None then fill (Vcs_aux.visit v id).next - else copy_info_w_state v id in - fill start - - let create_cluster l ~tip = vcs := create_cluster !vcs l tip - let cluster_of id = Option.map Dag.Cluster.data (cluster_of !vcs id) - let delete_cluster_of id = - Option.iter (fun x -> vcs := delete_cluster !vcs x) (Vcs_.cluster_of !vcs id) - - let gc () = - let old_vcs = !vcs in - let new_vcs, erased_nodes = gc old_vcs in - Vcs_.NodeSet.iter (fun id -> - match (Vcs_aux.visit old_vcs id).step with - | `Qed ({ fproof = Some (_, 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 (Thread.create run_command ()) - end - - end (* }}} *) - - let print ?(now=false) () = - if not !Flags.debug && not now then () else NB.command ~now (print_dag !vcs) - - let backup () = !vcs - let restore v = vcs := v - -end (* }}} *) - -(* Fills in the nodes of the VCS *) -module State : sig - - (** 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 : - ?redefine:bool -> ?cache:Summary.marshallable -> (unit -> unit) -> Stateid.t -> unit - - val install_cached : Stateid.t -> unit - val is_cached : Stateid.t -> bool - - - val exn_on : Stateid.t -> ?valid:Stateid.t -> exn -> exn - (* to send states across worker/master *) - type frozen_state - val get_cached : Stateid.t -> frozen_state - val assign : Stateid.t -> frozen_state -> unit - -end = struct (* {{{ *) - - (* 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 - - (* helpers *) - let freeze_global_state marshallable = - { system = States.freeze ~marshallable; - proof = Proof_global.freeze ~marshallable; - shallow = (marshallable = `Shallow) } - let unfreeze_global_state { system; proof } = - States.unfreeze system; Proof_global.unfreeze proof - - (* hack to make futures functional *) - let in_t, out_t = Dyn.create "state4future" - let () = Future.set_freeze - (fun () -> in_t (freeze_global_state `No, !cur_id)) - (fun t -> let s,i = out_t t in unfreeze_global_state s; cur_id := i) - - let is_cached id = - Stateid.equal id !cur_id || - match VCS.get_info id with - | { state = Some _ } -> true - | _ -> false - - let install_cached id = - if Stateid.equal id !cur_id then () else (* optimization *) - let s = - match VCS.get_info id with - | { state = Some s } -> s - | _ -> anomaly (str "unfreezing a non existing state") in - unfreeze_global_state s; cur_id := id - - type frozen_state = state - - let get_cached id = - try match VCS.get_info id with - | { state = Some s } -> s - | _ -> anomaly (str "not a cached state") - with VCS.Expired -> anomaly (str "not a cached state (expired)") - - let assign id s = - try if VCS.get_state id = None then VCS.set_state id s - with VCS.Expired -> () - - let freeze marhallable id = VCS.set_state id (freeze_global_state marhallable) - - let exn_on id ?valid e = - match Stateid.get e with - | Some _ -> e - | None -> - let loc = Option.default Loc.ghost (Loc.get_loc e) in - let msg = string_of_ppcmds (print e) in - Pp.feedback ~state_id:id (Interface.ErrorMsg (loc, msg)); - Stateid.add (Cerrors.process_vernac_interp_error e) ?valid id - - let define ?(redefine=false) ?(cache=`No) f id = - let str_id = Stateid.to_string id in - if is_cached id && not redefine then - anomaly (str"defining state "++str str_id++str" twice"); - try - prerr_endline("defining "^str_id^" (cache="^ - if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)"); - f (); - if cache = `Yes then freeze `No id - else if cache = `Shallow then freeze `Shallow id; - prerr_endline ("setting cur id to "^str_id); - cur_id := id; - feedback ~state_id:id Interface.Processed; - VCS.reached id true; - if Proof_global.there_are_pending_proofs () then - VCS.goals id (Proof_global.get_open_goals ()); - with e -> - let e = Errors.push e in - let good_id = !cur_id in - cur_id := Stateid.dummy; - VCS.reached id false; - match Stateid.get e with - | Some _ -> raise e - | None -> raise (exn_on id ~valid:good_id e) - -end -(* }}} *) - -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 !hints loc "context_used" in - let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") s) in - let ids = List.map (fun id -> Loc.ghost, id) ids in - SsExpr (SsSet ids) - -let get_hint_bp_time proof_name = - try float_of_string (Aux_file.get !hints Loc.ghost proof_name) - with Not_found -> 1.0 - -module Worker = Spawn.Sync(struct - let add_timeout ~sec f = - ignore(Thread.create (fun () -> - while true do - Unix.sleep sec; - if not (f ()) then Thread.exit () - done) - ()) -end) - -module WorkersPool = WorkerPool.Make(Worker) - -let record_pb_time proof_name loc 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 Loc.ghost proof_name proof_build_time; - hints := Aux_file.set !hints Loc.ghost proof_name proof_build_time - end - -(* Slave processes (if initialized, otherwise local lazy evaluation) *) -module Slaves : sig - - (* (eventually) remote calls *) - val build_proof : loc:Loc.t -> - exn_info:(Stateid.t * Stateid.t) -> start:Stateid.t -> stop:Stateid.t -> - name:string -> future_proof * 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 - - (* slave process main loop *) - val slave_main_loop : (unit -> unit) -> unit - val slave_init_stdout : unit -> unit - - (* to disentangle modules *) - val set_reach_known_state : - (?redefine_qed:bool -> cache:Summary.marshallable -> Stateid.t -> unit) -> unit - - type tasks - val dump : (Future.UUID.t * int) list -> tasks - val check_task : string -> tasks -> int -> bool - val info_tasks : tasks -> (string * float * int) list - val finish_task : - string -> - Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs -> - tasks -> int -> Library.seg_univ - - val cancel_worker : int -> unit - - val set_perspective : Stateid.t list -> unit - -end = struct (* {{{ *) - - - let cancel_worker n = WorkersPool.cancel (n-1) - - let reach_known_state = ref (fun ?redefine_qed ~cache id -> ()) - let set_reach_known_state f = reach_known_state := f - - type 'a request = - ReqBuildProof of - (Stateid.t * Stateid.t) * Stateid.t * VCS.vcs * Loc.t * 'a * string - - let name_of_request (ReqBuildProof (_,_,_,_,_,s)) = s - - type response = - | RespBuiltProof of Entries.proof_output list * float - | RespError of (* err, safe, msg, safe_states *) - Stateid.t * Stateid.t * std_ppcmds * - (Stateid.t * State.frozen_state) list - | RespFeedback of Interface.feedback - | RespGetCounterFreshLocalUniv - | RespGetCounterNewUnivLevel - let pr_response = function - | RespBuiltProof _ -> "Sucess" - | RespError _ -> "Error" - | RespFeedback { Interface.id = Interface.State id } -> - "Feedback on " ^ Stateid.to_string id - | RespFeedback _ -> assert false - | RespGetCounterFreshLocalUniv -> "GetCounterFreshLocalUniv" - | RespGetCounterNewUnivLevel -> "GetCounterNewUnivLevel" - - type more_data = - | MoreDataLocalUniv of Univ.universe list - | MoreDataUnivLevel of Univ.universe_level list - - type task = - | TaskBuildProof of (Stateid.t * Stateid.t) * Stateid.t * Stateid.t * - (Entries.proof_output list Future.assignement -> unit) * cancel_switch - * Loc.t * Future.UUID.t * string - let pr_task = function - | TaskBuildProof(_,bop,eop,_,_,_,_,s) -> - "TaskBuilProof("^Stateid.to_string bop^","^Stateid.to_string eop^ - ","^s^")" - - let request_of_task task : Future.UUID.t request = - match task with - | TaskBuildProof (exn_info,bop,eop,_,_,loc,uuid,s) -> - ReqBuildProof(exn_info,eop,VCS.slice ~start:eop ~stop:bop,loc,uuid,s) - - let cancel_switch_of_task = function - | TaskBuildProof (_,_,_,_,c,_,_,_) -> c - - let build_proof_here_core loc eop () = - let wall_clock1 = Unix.gettimeofday () in - if !Flags.batch_mode then !reach_known_state ~cache:`No eop - else !reach_known_state ~cache:`Shallow eop; - let wall_clock2 = Unix.gettimeofday () in - Aux_file.record_in_aux_at loc "proof_build_time" - (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); - Proof_global.return_proof () - let build_proof_here (id,valid) loc eop = - Future.create (State.exn_on id ~valid) (build_proof_here_core loc eop) - - let slave_respond msg = - match msg with - | ReqBuildProof(exn_info,eop,vcs,loc,_,_) -> - VCS.restore vcs; - VCS.print (); - let rc, time = - let wall_clock = Unix.gettimeofday () in - let l = Future.force (build_proof_here exn_info loc eop) in - List.iter (fun (_,se) -> Declareops.iter_side_effects (function - | Declarations.SEsubproof(_, - { Declarations.const_body = Declarations.OpaqueDef f } ) -> - Opaqueproof.join_opaque f - | _ -> ()) - se) l; - l, Unix.gettimeofday () -. wall_clock in - VCS.print (); - RespBuiltProof(rc,time) - - let check_task_aux extra name l i = - match List.nth l i with - | ReqBuildProof ((id,valid),eop,vcs,loc,_,s) -> - Pp.msg_info( - str(Printf.sprintf "Checking task %d (%s%s) of %s" i s extra name)); - VCS.restore vcs; - try - !reach_known_state ~cache:`No eop; - (* The original terminator, a hook, has not been saved in the .vi*) - Proof_global.set_terminator - (Lemmas.standard_proof_terminator [] (fun _ _ -> ())); - let proof = Proof_global.close_proof (fun x -> x) in - vernac_interp eop ~proof - { verbose = false; loc; - expr = (VernacEndProof (Proved (true,None))) }; - Some proof - with e -> - let e = Errors.push e in - (try match Stateid.get e with - | None -> - Pp.pperrnl Pp.( - str"File " ++ str name ++ str ": proof of " ++ str s ++ - spc () ++ print e) - | Some (_, cur) -> - match VCS.visit cur with - | { step = `Cmd ( { loc }, _) } - | { step = `Fork ( { loc }, _, _, _) } - | { step = `Qed ( { qast = { loc } }, _) } - | { step = `Sideff (`Ast ( { loc }, _)) } -> - let start, stop = Loc.unloc loc in - Pp.pperrnl Pp.( - str"File " ++ str name ++ str ": proof of " ++ str s ++ - str ": chars " ++ int start ++ str "-" ++ int stop ++ - spc () ++ print e) - | _ -> - Pp.pperrnl Pp.( - str"File " ++ str name ++ str ": proof of " ++ str s ++ - spc () ++ print e) - with e -> - Pp.msg_error (str"unable to print error message: " ++ - str (Printexc.to_string e))); None - - let finish_task name (u,cst,_) d p l i = - let bucket = - match List.nth l i with ReqBuildProof (_,_,_,_,bucket,_) -> bucket in - match check_task_aux (Printf.sprintf ", bucket %d" bucket) name l i with - | None -> exit 1 - | Some (po,pt) -> - let discharge c = List.fold_right Cooking.cook_constr d.(bucket) c in - let con = - Nametab.locate_constant - (Libnames.qualid_of_ident po.Proof_global.id) in - let c = Global.lookup_constant con in - match c.Declarations.const_body with - | Declarations.OpaqueDef lc -> - let uc = Option.get (Opaqueproof.get_constraints lc) in - let uc = - Future.chain ~greedy:true ~pure:true uc Univ.hcons_constraints in - let pr = Opaqueproof.get_proof lc in - let pr = Future.chain ~greedy:true ~pure:true pr discharge in - let pr = Future.chain ~greedy:true ~pure:true pr Constr.hcons in - Future.sink pr; - let extra = Future.join uc in - u.(bucket) <- uc; - p.(bucket) <- pr; - u, Univ.union_constraints cst extra, false - | _ -> assert false - - let check_task name l i = - match check_task_aux "" name l i with - | Some _ -> true - | None -> false - - let info_tasks l = - CList.map_i (fun i (ReqBuildProof(_,_,_,loc,_,s)) -> - let time1 = - try float_of_string (Aux_file.get !hints loc "proof_build_time") - with Not_found -> 0.0 in - let time2 = - try float_of_string (Aux_file.get !hints loc "proof_check_time") - with Not_found -> 0.0 in - s,max (time1 +. time2) 0.0001,i) 0 l - - open Interface - - exception MarshalError of string - - let marshal_to_channel oc data = - Marshal.to_channel oc data []; - flush oc - - let marshal_err s = raise (MarshalError s) - - let marshal_request oc (req : Future.UUID.t request) = - try marshal_to_channel oc req - with Failure s | Invalid_argument s | Sys_error s -> - marshal_err ("marshal_request: "^s) - - let unmarshal_request ic = - try (Marshal.from_channel ic : Future.UUID.t request) - with Failure s | Invalid_argument s | Sys_error s -> - marshal_err ("unmarshal_request: "^s) - - let marshal_response oc (res : response) = - try marshal_to_channel oc res - with Failure s | Invalid_argument s | Sys_error s -> - marshal_err ("marshal_response: "^s) - - let unmarshal_response ic = - try (CThread.thread_friendly_input_value ic : response) - with Failure s | Invalid_argument s | Sys_error s -> - marshal_err ("unmarshal_response: "^s) - - let marshal_more_data oc (res : more_data) = - try marshal_to_channel oc res - with Failure s | Invalid_argument s | Sys_error s -> - marshal_err ("marshal_more_data: "^s) - - let unmarshal_more_data ic = - try (Marshal.from_channel ic : more_data) - with Failure s | Invalid_argument s | Sys_error s -> - marshal_err ("unmarshal_more_data: "^s) - - let queue : task TQueue.t = TQueue.create () - - let set_perspective idl = - let open Stateid in - let p = List.fold_right Set.add idl Set.empty in - TQueue.reorder queue (fun task1 task2 -> - let TaskBuildProof (_, a1, b1, _, _,_,_,_) = task1 in - let TaskBuildProof (_, a2, b2, _, _,_,_,_) = task2 in - match Set.mem a1 p || Set.mem b1 p, Set.mem a2 p || Set.mem b2 p with - | true, true | false, false -> 0 - | true, false -> -1 - | false, true -> 1) - - let wait_all_done () = - if not (WorkersPool.is_empty ()) then - TQueue.wait_until_n_are_waiting_and_queue_empty - (WorkersPool.n_workers ()) queue - - let build_proof ~loc ~exn_info:(id,valid as exn_info) ~start ~stop ~name = - let cancel_switch = ref false in - if WorkersPool.is_empty () then - if !Flags.compilation_mode = Flags.BuildVi then begin - let force () : Entries.proof_output list Future.assignement = - try `Val (build_proof_here_core loc stop ()) - with e -> let e = Errors.push e in `Exn e in - let f,assign = Future.create_delegate ~force (State.exn_on id ~valid) in - let uuid = Future.uuid f in - TQueue.push queue (TaskBuildProof - (exn_info,start,stop,assign,cancel_switch,loc,uuid,name)); - f, cancel_switch - end else - build_proof_here exn_info loc stop, cancel_switch - else - let f, assign = Future.create_delegate (State.exn_on id ~valid) in - let uuid = Future.uuid f in - Pp.feedback (Interface.InProgress 1); - TQueue.push queue (TaskBuildProof - (exn_info,start,stop,assign,cancel_switch,loc,uuid,name)); - f, cancel_switch - - exception RemoteException of std_ppcmds - let _ = Errors.register_handler (function - | RemoteException ppcmd -> ppcmd - | _ -> raise Unhandled) - - exception KillRespawn - - let report_status ?id s = - let id = - match id with - | Some n -> n - | None -> - match !Flags.async_proofs_mode with - | Flags.APonParallel n -> n - | _ -> assert false in - Pp.feedback ~state_id:Stateid.initial (Interface.SlaveStatus(id, s)) - - let rec manage_slave ~cancel:cancel_user_req id_slave respawn = - let ic, oc, proc = - let rec set_slave_opt = function - | [] -> ["-async-proofs"; "worker"; string_of_int id_slave; "-feedback-glob"] - | ("-ideslave"|"-emacs"|"-emacs-U")::tl -> set_slave_opt tl - | ("-async-proofs" - |"-compile" - |"-compile-verbose")::_::tl -> set_slave_opt tl - | x::tl -> x :: set_slave_opt tl in - let args = - Array.of_list (set_slave_opt (List.tl (Array.to_list Sys.argv))) in - let env = - Array.append !async_proofs_workers_extra_env (Unix.environment ()) in - respawn ~args ~env () in - let last_task = ref None in - let task_expired = ref false in - let task_cancelled = ref false in - CThread.prepare_in_channel_for_thread_friendly_io ic; - try - while true do - prerr_endline "waiting for a task"; - report_status ~id:id_slave "Idle"; - let task = TQueue.pop queue in - prerr_endline ("got task: "^pr_task task); - last_task := Some task; - try - marshal_request oc (request_of_task task); - let cancel_switch = cancel_switch_of_task task in - Worker.kill_if proc ~sec:1 (fun () -> - task_expired := !cancel_switch; - task_cancelled := !cancel_user_req; - if !cancel_user_req then cancel_user_req := false; - !task_expired || !task_cancelled); - let rec loop () = - let response = unmarshal_response ic in - match task, response with - | TaskBuildProof(_,_,_, assign,_,loc,_,s), - RespBuiltProof(pl, time)-> - assign (`Val pl); - (* We restart the slave, to avoid memory leaks. We could just - Pp.feedback (Interface.InProgress ~-1) *) - record_pb_time s loc time; - last_task := None; - raise KillRespawn - | TaskBuildProof(_,_,_, assign,_,_,_,_), - RespError(err_id,valid,e,valid_states) -> - let e = Stateid.add ~valid (RemoteException e) err_id in - assign (`Exn e); - List.iter (fun (id,s) -> State.assign id s) valid_states; - (* We restart the slave, to avoid memory leaks. We could just - Pp.feedback (Interface.InProgress ~-1) *) - last_task := None; - raise KillRespawn - | _, RespGetCounterFreshLocalUniv -> - marshal_more_data oc (MoreDataLocalUniv - (CList.init 10 (fun _ -> Univ.fresh_local_univ ()))); - if !cancel_switch then raise KillRespawn else loop () - | _, RespGetCounterNewUnivLevel -> - marshal_more_data oc (MoreDataUnivLevel - (CList.init 10 (fun _ -> Termops.new_univ_level ()))); - loop () - | _, RespFeedback {id = State state_id; content = msg} -> - Pp.feedback ~state_id msg; - loop () - | _, RespFeedback _ -> assert false (* Parsing in master process *) - in - loop () - with - | VCS.Expired -> (* task cancelled: e.g. the user did backtrack *) - Pp.feedback (Interface.InProgress ~-1); - prerr_endline ("Task expired: " ^ pr_task task) - | (Sys_error _ | Invalid_argument _ | End_of_file | KillRespawn) as e -> - raise e (* we pass the exception to the external handler *) - | MarshalError s when !fallback_to_lazy_if_marshal_error -> - msg_warning(strbrk("Marshalling error: "^s^". "^ - "The system state could not be sent to the worker process. "^ - "Falling back to local, lazy, evaluation.")); - let TaskBuildProof (exn_info, _, stop, assign,_,loc,_,_) = task in - assign(`Comp(build_proof_here exn_info loc stop)); - Pp.feedback (Interface.InProgress ~-1) - | MarshalError s -> - pr_err ("Fatal marshal error: " ^ s); - flush_all (); exit 1 - | e -> - pr_err ("Uncaught exception in worker manager: "^ - string_of_ppcmds (print e)); - flush_all () - done - with - | KillRespawn -> - Pp.feedback (Interface.InProgress ~-1); - Worker.kill proc; ignore(Worker.wait proc); - manage_slave ~cancel:cancel_user_req id_slave respawn - | Sys_error _ | Invalid_argument _ | End_of_file when !task_expired -> - Pp.feedback (Interface.InProgress ~-1); - ignore(Worker.wait proc); - manage_slave ~cancel:cancel_user_req id_slave respawn - | Sys_error _ | Invalid_argument _ | End_of_file when !task_cancelled -> - msg_warning(strbrk "The worker was cancelled."); - Option.iter (fun task -> - let TaskBuildProof (_, start, _, assign, _,_,_,_) = task in - let s = "Worker cancelled by the user" in - let e = Stateid.add ~valid:start (RemoteException (strbrk s)) start in - assign (`Exn e); - Pp.feedback ~state_id:start (Interface.ErrorMsg (Loc.ghost, s)); - Pp.feedback (Interface.InProgress ~-1); - ) !last_task; - Worker.kill proc; ignore(Worker.wait proc); - manage_slave ~cancel:cancel_user_req id_slave respawn - | Sys_error _ | Invalid_argument _ | End_of_file - when !fallback_to_lazy_if_slave_dies -> - msg_warning(strbrk "The worker process died badly."); - Option.iter (fun task -> - msg_warning(strbrk "Falling back to local, lazy, evaluation."); - let TaskBuildProof (exn_info, _, stop, assign,_,loc,_,_) = task in - assign(`Comp(build_proof_here exn_info loc stop)); - Pp.feedback (Interface.InProgress ~-1); - ) !last_task; - Worker.kill proc; ignore(Worker.wait proc); - manage_slave ~cancel:cancel_user_req id_slave respawn - | Sys_error _ | Invalid_argument _ | End_of_file -> - Worker.kill proc; - let exit_status proc = match Worker.wait proc with - | Unix.WEXITED 0x400 -> "exit code unavailable" - | Unix.WEXITED i -> Printf.sprintf "exit(%d)" i - | Unix.WSIGNALED sno -> Printf.sprintf "signalled(%d)" sno - | Unix.WSTOPPED sno -> Printf.sprintf "stopped(%d)" sno in - pr_err ("Fatal worker error: " ^ (exit_status proc)); - flush_all (); exit 1 - - let init () = WorkersPool.init !Flags.async_proofs_n_workers manage_slave - - let slave_ic = ref stdin - let slave_oc = ref stdout - - let slave_init_stdout () = - let ic, oc = Spawned.get_channels () in - slave_oc := oc; slave_ic := ic - - let bufferize f = - let l = ref [] in - fun () -> - match !l with - | [] -> let data = f () in l := List.tl data; List.hd data - | x::tl -> l := tl; x - - let slave_handshake () = WorkersPool.worker_handshake !slave_ic !slave_oc - - let slave_main_loop reset = - let slave_feeder oc fb = - Marshal.to_channel oc (RespFeedback fb) []; - flush oc in - Pp.set_feeder (slave_feeder !slave_oc); - Termops.set_remote_new_univ_level (bufferize (fun () -> - marshal_response !slave_oc RespGetCounterNewUnivLevel; - match unmarshal_more_data !slave_ic with - | MoreDataUnivLevel l -> l | _ -> assert false)); - Univ.set_remote_fresh_local_univ (bufferize (fun () -> - marshal_response !slave_oc RespGetCounterFreshLocalUniv; - match unmarshal_more_data !slave_ic with - | MoreDataLocalUniv l -> l | _ -> assert false)); - let working = ref false in - slave_handshake (); - while true do - try - working := false; - let request = unmarshal_request !slave_ic in - working := true; - report_status (name_of_request request); - let response = slave_respond request in - report_status "Idle"; - marshal_response !slave_oc response; - reset () - with - | MarshalError s -> - pr_err ("Fatal marshal error: " ^ s); flush_all (); exit 2 - | End_of_file -> - prerr_endline "connection lost"; flush_all (); exit 2 - | e when Errors.noncritical e -> - (* This can happen if the proof is broken. The error has also been - * signalled as a feedback, hence we can silently recover *) - let err_id, safe_id = match Stateid.get e with - | Some (safe, err) -> err, safe - | None -> Stateid.dummy, Stateid.dummy in - prerr_endline "failed with the following exception:"; - prerr_endline (string_of_ppcmds (print e)); - prerr_endline ("last safe id is: " ^ Stateid.to_string safe_id); - prerr_endline ("cached? " ^ string_of_bool (State.is_cached safe_id)); - let prog old_v n = - if n < 3 then n else old_v + n/3 + if n mod 3 > 0 then 1 else 0 in - let states = - let open State in - let rec aux n m prev_id = - let next = - try Some (VCS.visit prev_id).next - with VCS.Expired -> None in - match next with - | None -> [] - | Some id when n = m -> - prerr_endline ("sending back state " ^ string_of_int m); - let tail = aux (n+1) (prog m (n+1)) id in - if is_cached id then (id, get_cached id) :: tail else tail - | Some id -> aux (n+1) m id in - (if is_cached safe_id then [safe_id,get_cached safe_id] else []) - @ aux 1 (prog 1 1) safe_id in - marshal_response !slave_oc (RespError(err_id, safe_id, print e, states)) - | e -> - pr_err ("Slave: critical exception: " ^ Pp.string_of_ppcmds (print e)); - flush_all (); exit 1 - done - - (* For external users this name is nicer than request *) - type tasks = int request list - let dump f2t_map = - assert(WorkersPool.is_empty ()); (* ATM, we allow that only if no slaves *) - let tasks = TQueue.dump queue in - prerr_endline (Printf.sprintf "dumping %d\n" (List.length tasks)); - let tasks = List.map request_of_task tasks in - List.map (function ReqBuildProof(a,b,c,d,x,e) -> - ReqBuildProof(a,b,c,d,List.assoc x f2t_map,e)) tasks - -end (* }}} *) - -(* Runs all transactions needed to reach a state *) -module Reach : sig - - val known_state : - ?redefine_qed:bool -> cache:Summary.marshallable -> Stateid.t -> unit - -end = struct (* {{{ *) - -let pstate = ["meta counter"; "evar counter"; "program-tcc-table"] - -let delegate_policy_check time = - if interactive () = `Yes then - (!Flags.async_proofs_mode = Flags.APonParallel 0 || - !Flags.async_proofs_mode = Flags.APonLazy) && time >= 1.0 - else if !Flags.compilation_mode = Flags.BuildVi then true - else !Flags.async_proofs_mode <> Flags.APoff && time >= 1.0 - -let collect_proof cur hd brkind id = - prerr_endline ("Collecting proof ending at "^Stateid.to_string id); - let no_name = "" in - let name = function - | [] -> no_name - | id :: _ -> Id.to_string id in - let loc = (snd cur).loc in - let is_defined = function - | _, { expr = VernacEndProof (Proved (false,_)) } -> true - | _ -> false in - let rec collect last accn id = - let view = VCS.visit id in - match last, view.step with - | _, `Cmd (x, _) -> collect (Some (id,x)) (id::accn) view.next - | _, `Alias _ -> `Sync (no_name,`Alias) - | _, `Fork(_,_,_,_::_::_)-> `Sync (no_name,`MutualProofs) - | _, `Fork(_,_,Doesn'tGuaranteeOpacity,_) -> - `Sync (no_name,`Doesn'tGuaranteeOpacity) - | Some (parent, ({ expr = VernacProof(_,Some _)} as v)), - `Fork (_, hd', GuaranteesOpacity, ids) -> - let name = name ids in - let time = get_hint_bp_time name in - assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch); - if delegate_policy_check time - then `ASync (parent,Some v,accn,name) - else `Sync (name,`Policy) - | Some (parent, ({ expr = VernacProof(t,None)} as v)), - `Fork (_, hd', GuaranteesOpacity, ids) when - not (State.is_cached parent) && - !Flags.compilation_mode = Flags.BuildVi -> - (try - let name = name ids in - let hint, time = get_hint_ctx loc, get_hint_bp_time name in - assert (VCS.Branch.equal hd hd'||VCS.Branch.equal hd VCS.edit_branch); - v.expr <- VernacProof(t, Some hint); - if delegate_policy_check time - then `ASync (parent,Some v,accn,name) - else `Sync (name,`Policy) - with Not_found -> `Sync (no_name,`NoHint)) - | Some (parent, _), `Fork (_, hd', GuaranteesOpacity, ids) -> - assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch); - let name = name ids in - let time = get_hint_bp_time name in - if delegate_policy_check time - then `MaybeASync (parent, accn, name) - else `Sync (name,`Policy) - | _, `Sideff _ -> `Sync (no_name,`NestedProof) - | _ -> `Sync (no_name,`Unknown) in - match cur, (VCS.visit id).step, brkind with - |( parent, { expr = VernacExactProof _ }), `Fork _, _ -> - `Sync (no_name,`Immediate) - | _, _, { VCS.kind = `Edit _ } -> collect (Some cur) [] id - | _ -> - if is_defined cur then `Sync (no_name,`Transparent) - else - let rc = collect (Some cur) [] id in - if not (State.is_cached id) then rc - else (* we already have the proof, no gain in delaying *) - match rc with - | `Sync(name,_) -> `Sync (name,`AlreadyEvaluated) - | `MaybeASync(_,_,name) -> `Sync (name,`AlreadyEvaluated) - | `ASync(_,_,_,name) -> `Sync (name,`AlreadyEvaluated) - -let string_of_reason = function - | `Transparent -> "Transparent" - | `AlreadyEvaluated -> "AlreadyEvaluated" - | `Policy -> "Policy" - | `NestedProof -> "NestedProof" - | `Immediate -> "Immediate" - | `Alias -> "Alias" - | `NoHint -> "NoHint" - | `Doesn'tGuaranteeOpacity -> "Doesn'tGuaranteeOpacity" - | _ -> "Unknown Reason" - -let wall_clock_last_fork = ref 0.0 - -let known_state ?(redefine_qed=false) ~cache id = - - (* ugly functions to process nested lemmas, i.e. hard to reproduce - * side effects *) - let cherry_pick_non_pstate () = - Summary.freeze_summary ~marshallable:`No ~complement:true pstate, - Lib.freeze ~marshallable:`No in - let inject_non_pstate (s,l) = Summary.unfreeze_summary s; Lib.unfreeze l in - - let rec pure_cherry_pick_non_pstate id = Future.purify (fun id -> - prerr_endline ("cherry-pick non pstate " ^ Stateid.to_string id); - reach id; - cherry_pick_non_pstate ()) id - - (* traverses the dag backward from nodes being already calculated *) - and reach ?(redefine_qed=false) ?(cache=cache) id = - prerr_endline ("reaching: " ^ Stateid.to_string id); - if not redefine_qed && State.is_cached id then begin - State.install_cached id; - feedback ~state_id:id Interface.Processed; - prerr_endline ("reached (cache)") - end else - let step, cache_step = - let view = VCS.visit id in - match view.step with - | `Alias id -> (fun () -> - reach view.next; reach id - ), cache - | `Cmd (x,_) -> (fun () -> - reach view.next; vernac_interp id x - ), cache - | `Fork (x,_,_,_) -> (fun () -> - reach view.next; vernac_interp id x; - wall_clock_last_fork := Unix.gettimeofday () - ), `Yes - | `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) -> - let rec aux = function - | `ASync (start, proof_using_ast, nodes, name) -> (fun () -> - prerr_endline ("Asynchronous " ^ Stateid.to_string id); - VCS.create_cluster nodes ~tip:id; - begin match keep, brinfo, qed.fproof with - | VtKeep, { VCS.kind = `Edit _ }, None -> assert false - | VtKeep, { VCS.kind = `Edit _ }, Some (ofp, cancel) -> - assert(redefine_qed = true); - VCS.create_cluster nodes ~tip:id; - let fp, cancel = Slaves.build_proof - ~loc:x.loc ~exn_info:(id,eop) ~start ~stop:eop ~name in - Future.replace ofp fp; - qed.fproof <- Some (fp, cancel) - | VtKeep, { VCS.kind = `Proof _ }, Some _ -> assert false - | VtKeep, { VCS.kind = `Proof _ }, None -> - reach ~cache:`Shallow start; - let fp, cancel = Slaves.build_proof - ~loc:x.loc ~exn_info:(id,eop) ~start ~stop:eop ~name in - qed.fproof <- Some (fp, cancel); - let proof = - Proof_global.close_future_proof ~feedback_id:id fp in - reach view.next; - vernac_interp id ~proof x; - feedback ~state_id:id Interface.Incomplete - | VtDrop, _, _ -> - reach view.next; - Option.iter (vernac_interp start) proof_using_ast; - vernac_interp id x - | _, { VCS.kind = `Master }, _ -> assert false - end; - Proof_global.discard_all () - ), if redefine_qed then `No else `Yes - | `Sync (name, `Immediate) -> (fun () -> - assert (Stateid.equal view.next eop); - reach eop; vernac_interp id x; Proof_global.discard_all () - ), `Yes - | `Sync (name, reason) -> (fun () -> - prerr_endline ("Synchronous " ^ Stateid.to_string id ^ " " ^ - string_of_reason reason); - reach eop; - let wall_clock = Unix.gettimeofday () in - record_pb_time name x.loc (wall_clock -. !wall_clock_last_fork); - begin match keep with - | VtKeep -> - let proof = - Proof_global.close_proof (State.exn_on id ~valid:eop) in - reach view.next; - let wall_clock2 = Unix.gettimeofday () in - vernac_interp id ~proof x; - let wall_clock3 = Unix.gettimeofday () in - Aux_file.record_in_aux_at x.loc "proof_check_time" - (Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2)) - | VtDrop -> - reach view.next; - vernac_interp id x - end; - Proof_global.discard_all () - ), `Yes - | `MaybeASync (start, nodes, name) -> (fun () -> - prerr_endline ("MaybeAsynchronous " ^ Stateid.to_string id); - reach ~cache:`Shallow start; - (* no sections *) - if List.is_empty (Environ.named_context (Global.env ())) - then fst (aux (`ASync (start, None, nodes, name))) () - else fst (aux (`Sync (name, `Unknown))) () - ), if redefine_qed then `No else `Yes - in - aux (collect_proof (view.next, x) brname brinfo eop) - | `Sideff (`Ast (x,_)) -> (fun () -> - reach view.next; vernac_interp id x - ), cache - | `Sideff (`Id origin) -> (fun () -> - let s = pure_cherry_pick_non_pstate origin in - reach view.next; - inject_non_pstate s - ), cache - in - if !Flags.async_proofs_mode = Flags.APonParallel 0 then - Pp.feedback ~state_id:id Interface.ProcessingInMaster; - State.define ~cache:cache_step ~redefine:redefine_qed step id; - prerr_endline ("reached: "^ Stateid.to_string id) in - reach ~redefine_qed id - -end (* }}} *) -let _ = Slaves.set_reach_known_state Reach.known_state - -(* The backtrack module simulates the classic behavior of a linear document *) -module Backtrack : sig - - val record : unit -> unit - val backto : Stateid.t -> unit - val back_safe : unit -> unit - - (* we could navigate the dag, but this ways easy *) - val branches_of : Stateid.t -> backup - - (* To be installed during initialization *) - val undo_vernac_classifier : vernac_expr -> vernac_classification - -end = struct (* {{{ *) - - let record () = - let current_branch = VCS.current_branch () in - 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 - info.vcs_backup <- Some (VCS.backup ()), Some { mine; others } - - let backto oid = - let info = VCS.get_info oid in - match info.vcs_backup with - | None, _ -> - anomaly(str"Backtrack.backto "++str(Stateid.to_string oid)++ - str": a state with no vcs_backup") - | Some vcs, _ -> - VCS.restore vcs; - let id = VCS.get_branch_pos (VCS.current_branch ()) in - if not (Stateid.equal id oid) then - anomaly (str "Backtrack.backto did not jump to the right state") - - let branches_of id = - let info = VCS.get_info id in - match info.vcs_backup with - | _, None -> - anomaly(str"Backtrack.backto "++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 = - if id = Stateid.initial || id = Stateid.dummy then [] else - match VCS.visit id with - | { step = `Fork (_,_,_,l) } -> l - | { step = `Cmd (_,l) } -> l - | _ -> [] in - match f acc (id, vcs, ids) with - | `Stop x -> x - | `Cont acc -> next acc - - let back_safe () = - let id = - fold_until (fun n (id,_,_) -> - if n >= 0 && State.is_cached id then `Stop id else `Cont (succ n)) - 0 (VCS.get_branch_pos (VCS.current_branch ())) in - backto id - - let undo_vernac_classifier v = - try - match v with - | VernacResetInitial -> - VtStm (VtBack Stateid.initial, true), VtNow - | VernacResetName (_,name) -> - msg_warning - (str"Reset not implemented for automatically generated constants"); - let id = VCS.get_branch_pos (VCS.current_branch ()) in - (try - let oid = - fold_until (fun b (id,_,label) -> - if b then `Stop id else `Cont (List.mem name label)) - false id in - VtStm (VtBack oid, true), VtNow - with Not_found -> - VtStm (VtBack id, true), VtNow) - | VernacBack n -> - let id = VCS.get_branch_pos (VCS.current_branch ()) in - let oid = fold_until (fun n (id,_,_) -> - if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in - VtStm (VtBack oid, true), VtNow - | VernacUndo n -> - let id = VCS.get_branch_pos (VCS.current_branch ()) in - let oid = fold_until (fun n (id,_,_) -> - if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in - VtStm (VtBack oid, true), VtLater - | VernacUndoTo _ - | VernacRestart as e -> - let m = match e with VernacUndoTo m -> m | _ -> 0 in - let id = VCS.get_branch_pos (VCS.current_branch ()) in - let vcs = - match (VCS.get_info id).vcs_backup with - | None, _ -> anomaly(str"Backtrack: tip with no vcs_backup") - | Some vcs, _ -> vcs in - let cb, _ = - Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs) 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 - VtStm (VtBack oid, true), VtLater - | VernacAbortAll -> - let id = VCS.get_branch_pos (VCS.current_branch ()) in - let oid = fold_until (fun () (id,vcs,_) -> - match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ()) - () id in - VtStm (VtBack oid, true), VtLater - | VernacBacktrack (id,_,_) - | VernacBackTo id -> - VtStm (VtBack (Stateid.of_int id), true), VtNow - | _ -> VtUnknown, VtNow - with - | Not_found -> - msg_warning(str"undo_vernac_classifier: going back to the initial state."); - VtStm (VtBack Stateid.initial, true), VtNow - -end (* }}} *) - -let init () = - VCS.init Stateid.initial; - set_undo_classifier Backtrack.undo_vernac_classifier; - State.define ~cache:`Yes (fun () -> ()) Stateid.initial; - Backtrack.record (); - if !Flags.async_proofs_mode = Flags.APonParallel 0 then begin - Slaves.init (); - let opts = match !Flags.async_proofs_worker_flags with - | None -> [] - | Some s -> Str.split_delim (Str.regexp ",") s in - if String.List.mem "fallback-to-lazy-if-marshal-error=no" opts then - fallback_to_lazy_if_marshal_error := false; - if String.List.mem "fallback-to-lazy-if-slave-dies=no" opts then - fallback_to_lazy_if_slave_dies := false; - begin try - let env_opt = Str.regexp "^extra-env=" in - let env = List.find (fun s -> Str.string_match env_opt s 0) opts in - async_proofs_workers_extra_env := Array.of_list - (Str.split_delim (Str.regexp ";") (Str.replace_first env_opt "" env)) - with Not_found -> () end; - end - -let slave_main_loop () = Slaves.slave_main_loop Ephemeron.clear - -let slave_init_stdout () = Slaves.slave_init_stdout () - -let observe id = - let vcs = VCS.backup () in - try - Reach.known_state ~cache:(interactive ()) id; - VCS.print () - with e -> - let e = Errors.push e in - VCS.print (); - VCS.restore vcs; - raise e - -let finish () = - observe (VCS.get_branch_pos (VCS.current_branch ())); - VCS.print () - -let wait () = - Slaves.wait_all_done (); - VCS.print () - -let join () = - let rec jab id = - if Stateid.equal id Stateid.initial then () - else - let view = VCS.visit id in - match view.step with - | `Qed ({ keep = VtDrop }, eop) -> - Future.purify observe eop; jab view.next - | _ -> jab view.next in - finish (); - wait (); - prerr_endline "Joining the environment"; - Global.join_safe_environment (); - VCS.print (); - prerr_endline "Joining the aborted proofs"; - jab (VCS.get_branch_pos VCS.Branch.master); - VCS.print () - -type tasks = Slaves.tasks * RemoteCounter.remote_counters_status -let dump x = Slaves.dump x, RemoteCounter.backup () -let check_task name (tasks,_) i = - let vcs = VCS.backup () in - try - let rc = Future.purify (Slaves.check_task name tasks) i in - Pp.pperr_flush (); - VCS.restore vcs; - rc - with e when Errors.noncritical e -> VCS.restore vcs; false -let info_tasks (tasks,_) = Slaves.info_tasks tasks -let finish_tasks name u d p (t,rcbackup as tasks) = - RemoteCounter.restore rcbackup; - let finish_task u (_,_,i) = - let vcs = VCS.backup () in - let u = Future.purify (Slaves.finish_task name u d p t) i in - Pp.pperr_flush (); - VCS.restore vcs; - u in - try - let u, a, _ = List.fold_left finish_task u (info_tasks tasks) in - (u,a,true), p - with e -> - let e = Errors.push e in - Pp.pperrnl Pp.(str"File " ++ str name ++ str ":" ++ spc () ++ print e); - exit 1 - -let merge_proof_branch qast keep brname = - let brinfo = VCS.get_branch brname in - let qed fproof = { qast; keep; brname; brinfo; fproof } in - match brinfo with - | { VCS.kind = `Proof _ } -> - VCS.checkout VCS.Branch.master; - let id = VCS.new_node () in - VCS.merge id ~ours:(Qed (qed None)) brname; - VCS.delete_branch brname; - if keep == VtKeep then VCS.propagate_sideff None; - `Ok - | { VCS.kind = `Edit (mode, qed_id, master_id) } -> - let ofp = - match VCS.visit qed_id with - | { step = `Qed ({ fproof }, _) } -> fproof - | _ -> assert false in - VCS.rewrite_merge qed_id ~ours:(Qed (qed ofp)) ~at:master_id brname; - VCS.delete_branch brname; - VCS.gc (); - Reach.known_state ~redefine_qed:true ~cache:`No qed_id; - VCS.checkout VCS.Branch.master; - `Unfocus qed_id - | { VCS.kind = `Master } -> - raise (State.exn_on Stateid.dummy Proof_global.NoCurrentProof) - -(* When tty is true, this code also does some of the job of the user interface: - jump back to a state that is valid *) -let handle_failure e vcs tty = - match Stateid.get e with - | None -> - VCS.restore vcs; - VCS.print (); - if tty && interactive () = `Yes then begin - (* Hopefully the 1 to last state is valid *) - Backtrack.back_safe (); - VCS.checkout_shallowest_proof_branch (); - end; - VCS.print (); - anomaly(str"error with no safe_id attached:" ++ spc() ++ - Errors.print_no_report e) - | Some (safe_id, id) -> - prerr_endline ("Failed at state " ^ Stateid.to_string id); - VCS.restore vcs; - if tty && interactive () = `Yes then begin - (* We stay on a valid state *) - Backtrack.backto safe_id; - VCS.checkout_shallowest_proof_branch (); - Reach.known_state ~cache:(interactive ()) safe_id; - end; - VCS.print (); - raise e - -let process_transaction ~tty verbose c (loc, expr) = - let warn_if_pos a b = - if b then msg_warning(pr_ast a ++ str" should not be part of a script") in - let v, x = expr, { verbose = verbose && Flags.is_verbose(); loc; expr } in - prerr_endline ("{{{ processing: "^ string_of_ppcmds (pr_ast x)); - let vcs = VCS.backup () in - try - let head = VCS.current_branch () in - VCS.checkout head; - let rc = begin - prerr_endline (" classified as: " ^ string_of_vernac_classification c); - match c with - (* PG stuff *) - | VtStm(VtPG,false), VtNow -> vernac_interp Stateid.dummy x; `Ok - | VtStm(VtPG,_), _ -> anomaly(str "PG command in script or VtLater") - (* Joining various parts of the document *) - | VtStm (VtJoinDocument, b), VtNow -> warn_if_pos x b; join (); `Ok - | VtStm (VtFinish, b), VtNow -> warn_if_pos x b; finish (); `Ok - | VtStm (VtWait, b), VtNow -> warn_if_pos x b; finish (); wait (); `Ok - | VtStm (VtPrintDag, b), VtNow -> - warn_if_pos x b; VCS.print ~now:true (); `Ok - | VtStm (VtObserve id, b), VtNow -> warn_if_pos x b; observe id; `Ok - | VtStm ((VtObserve _ | VtFinish | VtJoinDocument - |VtPrintDag |VtWait),_), VtLater -> - anomaly(str"classifier: join actions cannot be classified as VtLater") - - (* Back *) - | VtStm (VtBack oid, true), w -> - let id = VCS.new_node () in - let { mine; others } = Backtrack.branches_of oid in - List.iter (fun branch -> - if not (List.mem_assoc branch (mine::others)) then - ignore(merge_proof_branch x VtDrop branch)) - (VCS.branches ()); - VCS.checkout_shallowest_proof_branch (); - let head = VCS.current_branch () in - List.iter (fun b -> - if not(VCS.Branch.equal b head) then begin - VCS.checkout b; - VCS.commit (VCS.new_node ()) (Alias oid); - end) - (VCS.branches ()); - VCS.checkout_shallowest_proof_branch (); - VCS.commit id (Alias oid); - Backtrack.record (); if w == VtNow then finish (); `Ok - | VtStm (VtBack id, false), VtNow -> - prerr_endline ("undo to state " ^ Stateid.to_string id); - Backtrack.backto id; - VCS.checkout_shallowest_proof_branch (); - Reach.known_state ~cache:(interactive ()) id; `Ok - | VtStm (VtBack id, false), VtLater -> - anomaly(str"classifier: VtBack + VtLater must imply part_of_script") - - (* Query *) - | VtQuery false, VtNow when tty = true -> - finish (); - (try Future.purify (vernac_interp Stateid.dummy) - { verbose = true; loc; expr } - with e when Errors.noncritical e -> - let e = Errors.push e in - raise(State.exn_on Stateid.dummy e)); `Ok - | VtQuery false, VtNow -> - (try vernac_interp Stateid.dummy x - with e when Errors.noncritical e -> - let e = Errors.push e in - raise(State.exn_on Stateid.dummy e)); `Ok - | VtQuery true, w -> - let id = VCS.new_node () in - VCS.commit id (Cmd (x,[])); - Backtrack.record (); if w == VtNow then finish (); `Ok - | VtQuery false, VtLater -> - anomaly(str"classifier: VtQuery + VtLater must imply part_of_script") - - (* Proof *) - | VtStartProof (mode, guarantee, names), w -> - let id = VCS.new_node () in - let bname = VCS.mk_branch_name x in - VCS.checkout VCS.Branch.master; - VCS.commit id (Fork (x, bname, guarantee, names)); - VCS.branch bname (`Proof (mode, VCS.proof_nesting () + 1)); - Proof_global.activate_proof_mode mode; - Backtrack.record (); if w == VtNow then finish (); `Ok - | VtProofMode _, VtLater -> - anomaly(str"VtProofMode must be executed VtNow") - | VtProofMode mode, VtNow -> - let id = VCS.new_node () in - VCS.checkout VCS.Branch.master; - VCS.commit id (Cmd (x,[])); - VCS.propagate_sideff (Some x); - List.iter - (fun bn -> match VCS.get_branch bn with - | { VCS.root; kind = `Master; pos } -> () - | { VCS.root; kind = `Proof(_,d); pos } -> - VCS.delete_branch bn; - VCS.branch ~root ~pos bn (`Proof(mode,d)) - | { VCS.root; kind = `Edit(_,f,q); pos } -> - VCS.delete_branch bn; - VCS.branch ~root ~pos bn (`Edit(mode,f,q))) - (VCS.branches ()); - VCS.checkout_shallowest_proof_branch (); - Backtrack.record (); - finish (); - `Ok - | VtProofStep, w -> - let id = VCS.new_node () in - VCS.commit id (Cmd (x,[])); - Backtrack.record (); if w == VtNow then finish (); `Ok - | VtQed keep, w -> - let rc = merge_proof_branch x keep head in - VCS.checkout_shallowest_proof_branch (); - Backtrack.record (); if w == VtNow then finish (); - rc - - (* Side effect on all branches *) - | VtSideff l, w -> - let id = VCS.new_node () in - VCS.checkout VCS.Branch.master; - VCS.commit id (Cmd (x,l)); - VCS.propagate_sideff (Some x); - VCS.checkout_shallowest_proof_branch (); - Backtrack.record (); if w == VtNow then finish (); `Ok - - (* Unknown: we execute it, check for open goals and propagate sideeff *) - | VtUnknown, VtNow -> - let id = VCS.new_node () in - let step () = - VCS.checkout VCS.Branch.master; - let mid = VCS.get_branch_pos VCS.Branch.master in - Reach.known_state ~cache:(interactive ()) mid; - vernac_interp id x; - (* Vernac x may or may not start a proof *) - if VCS.Branch.equal head VCS.Branch.master && - Proof_global.there_are_pending_proofs () - then begin - let bname = VCS.mk_branch_name x in - VCS.commit id (Fork (x,bname,Doesn'tGuaranteeOpacity,[])); - VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1)); - Proof_global.activate_proof_mode "Classic"; - end else begin - VCS.commit id (Cmd (x,[])); - VCS.propagate_sideff (Some x); - VCS.checkout_shallowest_proof_branch (); - end in - State.define ~cache:`Yes step id; - Backtrack.record (); `Ok - - | VtUnknown, VtLater -> - anomaly(str"classifier: VtUnknown must imply VtNow") - end in - (* Proof General *) - begin match v with - | VernacStm (PGLast _) -> - if not (VCS.Branch.equal head VCS.Branch.master) then - vernac_interp Stateid.dummy - { verbose = true; loc = Loc.ghost; - expr = VernacShow (ShowGoal OpenSubgoals) } - | _ -> () - end; - prerr_endline "processed }}}"; - VCS.print (); - rc - with e -> - let e = Errors.push e in - handle_failure e vcs tty - -(** STM interface {{{******************************************************* **) - -let stop_worker n = Slaves.cancel_worker n - -let query ~at s = - Future.purify (fun s -> - if Stateid.equal at Stateid.dummy then finish () - else Reach.known_state ~cache:`Yes at; - let _, ast as loc_ast = vernac_parse 0 s in - let clas = classify_vernac ast in - match clas with - | VtStm (w,_), _ -> - ignore(process_transaction - ~tty:false true (VtStm (w,false), VtNow) loc_ast) - | _ -> - ignore(process_transaction - ~tty:false true (VtQuery false, VtNow) loc_ast)) - s - -let add ~ontop ?(check=ignore) verb eid s = - let cur_tip = VCS.cur_tip () in - if Stateid.equal ontop cur_tip then begin - let _, ast as loc_ast = vernac_parse eid s in - check(loc_ast); - let clas = classify_vernac ast in - match process_transaction ~tty:false verb clas loc_ast with - | `Ok -> VCS.cur_tip (), `NewTip - | `Unfocus qed_id -> qed_id, `Unfocus (VCS.cur_tip ()) - end else begin - (* For now, arbitrary edits should be announced with edit_at *) - anomaly(str"Not yet implemented, the GUI should not try this") - end - -let set_perspective id_list = Slaves.set_perspective id_list - -type focus = { - start : Stateid.t; - stop : Stateid.t; - tip : Stateid.t -} - -let edit_at id = - if Stateid.equal id Stateid.dummy then anomaly(str"edit_at dummy") else - let vcs = VCS.backup () in - let on_cur_branch id = - let rec aux cur = - if id = cur then true - else match VCS.visit cur with - | { step = `Fork _ } -> false - | { next } -> aux next in - aux (VCS.get_branch_pos (VCS.current_branch ())) in - let is_ancestor_of_cur_branch id = - Vcs_.NodeSet.mem id - (VCS.reachable (VCS.get_branch_pos (VCS.current_branch ()))) in - let has_failed qed_id = - match VCS.visit qed_id with - | { step = `Qed ({ fproof = Some (fp,_) }, _) } -> Future.is_exn fp - | _ -> false in - let rec master_for_br root tip = - if Stateid.equal tip Stateid.initial then tip else - match VCS.visit tip with - | { next } when next = root -> root - | { step = `Fork _ } -> tip - | { step = `Sideff (`Ast(_,id)|`Id id) } -> id - | { next } -> master_for_br root next in - let reopen_branch at_id mode qed_id tip = - VCS.delete_cluster_of id; - let master_id = - match VCS.visit qed_id with - | { step = `Qed _; next = master_id } -> master_id - | _ -> anomaly (str "Cluster not ending with Qed") in - VCS.branch ~root:master_id ~pos:id - VCS.edit_branch (`Edit (mode, qed_id, master_id)); - Reach.known_state ~cache:(interactive ()) id; - VCS.checkout_shallowest_proof_branch (); - `Focus { stop = qed_id; start = master_id; tip } in - let backto id = - List.iter VCS.delete_branch (VCS.branches ()); - let ancestors = VCS.reachable id in - let { mine = brname, brinfo; others } = Backtrack.branches_of id in - List.iter (fun (name,{ VCS.kind = k; root; pos }) -> - if not(VCS.Branch.equal name VCS.Branch.master) && - Vcs_.NodeSet.mem root ancestors then - VCS.branch ~root ~pos name k) - others; - VCS.reset_branch VCS.Branch.master (master_for_br brinfo.VCS.root id); - VCS.branch ~root:brinfo.VCS.root ~pos:brinfo.VCS.pos brname brinfo.VCS.kind; - VCS.delete_cluster_of id; - VCS.gc (); - Reach.known_state ~cache:(interactive ()) id; - VCS.checkout_shallowest_proof_branch (); - `NewTip in - try - let rc = - let focused = List.exists ((=) VCS.edit_branch) (VCS.branches ()) in - let branch_info = - match snd (VCS.get_info id).vcs_backup with - | Some{ mine = _, { VCS.kind = (`Proof(m,_)|`Edit(m,_,_)) }} -> Some m - | _ -> None in - match focused, VCS.cluster_of id, branch_info with - | _, Some _, None -> assert false - | false, Some qed_id, Some mode -> - let tip = VCS.cur_tip () in - if has_failed qed_id then reopen_branch id mode qed_id tip - else backto id - | true, Some qed_id, Some mode -> - if on_cur_branch id then begin - assert false - end else if is_ancestor_of_cur_branch id then begin - backto id - end else begin - anomaly(str"Cannot leave an `Edit branch open") - end - | true, None, _ -> - if on_cur_branch id then begin - VCS.reset_branch (VCS.current_branch ()) id; - Reach.known_state ~cache:(interactive ()) id; - VCS.checkout_shallowest_proof_branch (); - `NewTip - end else if is_ancestor_of_cur_branch id then begin - backto id - end else begin - anomaly(str"Cannot leave an `Edit branch open") - end - | false, None, _ -> backto id - in - VCS.print (); - rc - with e -> - let e = Errors.push e in - match Stateid.get e with - | None -> - VCS.print (); - anomaly (str ("edit_at: "^string_of_ppcmds (Errors.print_no_report e))) - | Some (_, id) -> - prerr_endline ("Failed at state " ^ Stateid.to_string id); - VCS.restore vcs; - VCS.print (); - raise e -(* }}} *) - -(** Old tty interface {{{*************************************************** **) - -let interp verb (_,e as lexpr) = - let clas = classify_vernac e in - let rc = process_transaction ~tty:true verb clas lexpr in - if rc <> `Ok then anomaly(str"tty loop can't be mixed with the STM protocol"); - if interactive () = `Yes || - (!Flags.async_proofs_mode = Flags.APoff && - !Flags.compilation_mode = Flags.BuildVo) then - let vcs = VCS.backup () in - try finish () - with e -> - let e = Errors.push e in - handle_failure e vcs true - -let get_current_state () = VCS.cur_tip () - -let current_proof_depth () = - let head = VCS.current_branch () in - match VCS.get_branch head with - | { VCS.kind = `Master } -> 0 - | { VCS.pos = cur; VCS.kind = (`Proof _ | `Edit _); VCS.root = root } -> - let rec distance root = - if Stateid.equal cur root then 0 - else 1 + distance (VCS.visit cur).next in - distance cur - -let unmangle n = - let n = VCS.Branch.to_string n in - let idx = String.index n '_' + 1 in - Names.id_of_string (String.sub n idx (String.length n - idx)) - -let proofname b = match VCS.get_branch b with - | { VCS.kind = (`Proof _| `Edit _) } -> Some b - | _ -> None - -let get_all_proof_names () = - List.map unmangle (List.map_filter proofname (VCS.branches ())) - -let get_current_proof_name () = - Option.map unmangle (proofname (VCS.current_branch ())) - -let get_script prf = - let branch, test = - match prf with - | None -> VCS.Branch.master, fun _ -> true - | Some name -> VCS.current_branch (), List.mem name 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 (`Ast (x,_)) -> - find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next - | `Sideff (`Id id) -> find acc id - | `Cmd (x,_) -> find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next - | `Alias id -> find acc id - | `Fork _ -> find acc view.next - in - find [] (VCS.get_branch_pos branch) - -(* indentation code for Show Script, initially contributed - by D. de Rauglaudre *) - -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 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 = - (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 show_script ?proof () = - try - let prf = - try match proof with - | None -> Some (Pfedit.get_current_proof_name ()) - | Some (p,_) -> Some (p.Proof_global.id) - with Proof_global.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 (v 0 (Pp.prlist_with_sep Pp.fnl (fun x -> x) indented_cmds)) - with Vcs_aux.Expired -> () - -let () = Vernacentries.show_script := show_script - -(* }}} *) - -(* vim:set foldmethod=marker: *) diff --git a/toplevel/stm.mli b/toplevel/stm.mli deleted file mode 100644 index 3414ba4f41..0000000000 --- a/toplevel/stm.mli +++ /dev/null @@ -1,80 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* ?check:(located_vernac_expr -> unit) -> - bool -> edit_id -> string -> - Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] - -(* parses and xecutes a command at a given state, throws away its side effects - but for the printings *) -val query : at:Stateid.t -> string -> unit - -(* [edit_at id] is issued to change the editing zone. [`NewTip] is returned if - the requested id is the new document tip hence the document portion following - [id] is dropped by Coq. [`Focus fo] is returned to say that [fo.tip] is the - new document tip, the document between [id] and [fo.stop] has been dropped. - The portion between [fo.stop] and [fo.tip] has been kept. [fo.start] is - just to tell the gui where the editing zone starts, in case it wants to - graphically denote it. All subsequent [add] happen on top of [id]. *) -type focus = { start : Stateid.t; stop : Stateid.t; tip : Stateid.t } -val edit_at : Stateid.t -> [ `NewTip | `Focus of focus ] - -(* Evaluates the tip of the current branch *) -val finish : unit -> unit - -val stop_worker : int -> unit - -(* Joins the entire document. Implies finish, but also checks proofs *) -val join : unit -> unit -(* To save to disk an incomplete document *) -type tasks -val dump : (Future.UUID.t * int) list -> tasks - -val check_task : string -> tasks -> int -> bool -val info_tasks : tasks -> (string * float * int) list -val finish_tasks : string -> - Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs -> - tasks -> Library.seg_univ * Library.seg_proofs - -(* Id of the tip of the current branch *) -val get_current_state : unit -> Stateid.t - -(* Misc *) -val init : unit -> unit -val slave_main_loop : unit -> unit -val slave_init_stdout : unit -> unit - -(* Filename *) -val set_compilation_hints : string -> unit - -(* Reorders the task queue putting forward what is in the perspective *) -val set_perspective : Stateid.t list -> unit - -(** read-eval-print loop compatible interface ****************************** **) - -(* Adds a new line to the document. It replaces the core of Vernac.interp. - [finish] is called as the last bit of this function is the system - is running interactively (-emacs or coqtop). *) -val interp : bool -> located_vernac_expr -> unit - -(* Queries for backward compatibility *) -val current_proof_depth : unit -> int -val get_all_proof_names : unit -> Id.t list -val get_current_proof_name : unit -> Id.t option - diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index d348ce7472..a5519d5860 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -5,7 +5,6 @@ Locality Metasyntax Auto_ind_decl Search -Lemmas Indschemes Obligations Command @@ -14,10 +13,7 @@ Record Vernacinterp Mltop Vernacentries -Vernac_classifier -Stm Whelp -Vi_checking Vernac Ide_slave Usage diff --git a/toplevel/vernac_classifier.ml b/toplevel/vernac_classifier.ml deleted file mode 100644 index 49cbcd246b..0000000000 --- a/toplevel/vernac_classifier.ml +++ /dev/null @@ -1,189 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* "Unknown" - | VtStartProof _ -> "StartProof" - | VtSideff _ -> "Sideff" - | VtQed VtKeep -> "Qed(keep)" - | VtQed VtDrop -> "Qed(drop)" - | VtProofStep -> "ProofStep" - | VtProofMode s -> "ProofMode " ^ s - | VtQuery b -> "Query" ^ string_of_in_script b - | VtStm ((VtFinish|VtJoinDocument|VtObserve _|VtPrintDag|VtWait), b) -> - "Stm" ^ string_of_in_script b - | VtStm (VtPG, b) -> "Stm PG" ^ string_of_in_script b - | VtStm (VtBack _, b) -> "Stm Back" ^ string_of_in_script b - -let string_of_vernac_when = function - | VtLater -> "Later" - | VtNow -> "Now" - -let string_of_vernac_classification (t,w) = - string_of_vernac_type t ^ " " ^ string_of_vernac_when w - -let classifiers = ref [] -let declare_vernac_classifier - (s : string) - (f : Genarg.raw_generic_argument list -> unit -> vernac_classification) -= - classifiers := !classifiers @ [s,f] - -let elide_part_of_script_and_now (a, _) = - match a with - | VtQuery _ -> VtQuery false, VtNow - | VtStm (x, _) -> VtStm (x, false), VtNow - | x -> x, VtNow - -let undo_classifier = ref (fun _ -> assert false) -let set_undo_classifier f = undo_classifier := f - -let rec classify_vernac e = - let static_classifier e = match e with - (* PG compatibility *) - | VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"]) - | VernacSetOption ((["Silent"]|["Undo"]|["Printing";"Depth"]),_) - when !Flags.print_emacs -> VtStm(VtPG,false), VtNow - (* Stm *) - | VernacStm Finish -> VtStm (VtFinish, true), VtNow - | VernacStm Wait -> VtStm (VtWait, true), VtNow - | VernacStm JoinDocument -> VtStm (VtJoinDocument, true), VtNow - | VernacStm PrintDag -> VtStm (VtPrintDag, true), VtNow - | VernacStm (Observe id) -> VtStm (VtObserve id, true), VtNow - | VernacStm (Command x) -> elide_part_of_script_and_now (classify_vernac x) - | VernacStm (PGLast x) -> fst (classify_vernac x), VtNow - (* Nested vernac exprs *) - | VernacProgram e -> classify_vernac e - | VernacLocal (_,e) -> classify_vernac e - | VernacTimeout (_,e) -> classify_vernac e - | VernacTime e -> classify_vernac e - | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) - (match classify_vernac e with - | ( VtQuery _ | VtProofStep | VtSideff _ - | VtStm _ | VtProofMode _ ), _ as x -> x - | VtQed _, _ -> VtProofStep, VtNow - | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow) - (* Qed *) - | VernacEndProof Admitted | VernacAbort _ -> VtQed VtDrop, VtLater - | VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater - (* Query *) - | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _ - | VernacCheckMayEval _ -> VtQuery true, VtLater - (* ProofStep *) - | VernacProof _ - | VernacBullet _ - | VernacFocus _ | VernacUnfocus - | VernacSubproof _ | VernacEndSubproof - | VernacSolve _ | VernacError _ - | VernacCheckGuard - | VernacUnfocused - | VernacSolveExistential _ -> VtProofStep, VtLater - (* Options changing parser *) - | VernacUnsetOption (["Default";"Proof";"Using"]) - | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow - (* StartProof *) - | VernacDefinition (_,(_,i),ProveBody _) -> - VtStartProof("Classic",GuaranteesOpacity,[i]), VtLater - | VernacStartTheoremProof (_,l,_) -> - let ids = - CList.map_filter (function (Some(_,i), _) -> Some i | _ -> None) l in - VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater - | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater - | VernacFixpoint (_,l) -> - let ids, open_proof = - List.fold_left (fun (l,b) (((_,id),_,_,_,p),_) -> - id::l, b || p = None) ([],false) l in - if open_proof then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater - else VtSideff ids, VtLater - | VernacCoFixpoint (_,l) -> - let ids, open_proof = - List.fold_left (fun (l,b) (((_,id),_,_,p),_) -> - id::l, b || p = None) ([],false) l in - if open_proof then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater - else VtSideff ids, VtLater - (* Sideff: apply to all open branches. usually run on master only *) - | VernacAssumption (_,_,l) -> - let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd l) l) in - VtSideff ids, VtLater - | VernacDefinition (_,(_,id),DefineBody _) -> VtSideff [id], VtLater - | VernacInductive (_,_,l) -> - let ids = List.map (fun (((_,(_,id)),_,_,_,cl),_) -> id :: match cl with - | Constructors l -> List.map (fun (_,((_,id),_)) -> id) l - | RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @ - CList.map_filter (function - | ((_,AssumExpr((_,Names.Name n),_)),_),_ -> Some n - | _ -> None) l) l in - VtSideff (List.flatten ids), VtLater - | VernacScheme l -> - let ids = List.map snd (CList.map_filter (fun (x,_) -> x) l) in - VtSideff ids, VtLater - | VernacCombinedScheme ((_,id),_) -> VtSideff [id], VtLater - | VernacBeginSection _ - | VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _ - | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _ - | VernacChdir _ - | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _ - | VernacDeclareImplicits _ | VernacArguments _ | VernacArgumentsScope _ - | VernacReserve _ - | VernacGeneralizable _ - | VernacSetOpacity _ | VernacSetStrategy _ - | VernacUnsetOption _ | VernacSetOption _ - | VernacAddOption _ | VernacRemoveOption _ - | VernacMemOption _ | VernacPrintOption _ - | VernacGlobalCheck _ - | VernacDeclareReduction _ - | VernacDeclareClass _ | VernacDeclareInstances _ - | VernacRegister _ - | VernacComments _ -> VtSideff [], VtLater - (* Who knows *) - | VernacList _ - | VernacLoad _ -> VtSideff [], VtNow - (* (Local) Notations have to disappear *) - | VernacEndSegment _ -> VtSideff [], VtNow - (* Modules with parameters have to be executed: can import notations *) - | VernacDeclareModule (exp,(_,id),bl,_) - | VernacDefineModule (exp,(_,id),bl,_,_) -> - VtSideff [id], if bl = [] && exp = None then VtLater else VtNow - | VernacDeclareModuleType ((_,id),bl,_,_) -> - VtSideff [id], if bl = [] then VtLater else VtNow - (* These commands alter the parser *) - | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _ - | VernacInfix _ | VernacNotation _ | VernacSyntaxExtension _ - | VernacSyntacticDefinition _ - | VernacDeclareTacticDefinition _ | VernacTacticNotation _ - | VernacRequire _ | VernacImport _ | VernacInclude _ - | VernacDeclareMLModule _ - | VernacContext _ (* TASSI: unsure *) - | VernacProofMode _ - (* These are ambiguous *) - | VernacInstance _ -> VtUnknown, VtNow - (* Stm will install a new classifier to handle these *) - | VernacBack _ | VernacAbortAll - | VernacUndoTo _ | VernacUndo _ - | VernacResetName _ | VernacResetInitial - | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> !undo_classifier e - (* What are these? *) - | VernacNop - | VernacToplevelControl _ - | VernacRestoreState _ - | VernacWriteState _ -> VtUnknown, VtNow - (* Plugins should classify their commands *) - | VernacExtend (s,l) -> - try List.assoc s !classifiers l () - with Not_found -> anomaly(str"No classifier for"++spc()++str s) - in - static_classifier e - -let classify_as_query = VtQuery true, VtLater -let classify_as_sideeff = VtSideff [], VtLater diff --git a/toplevel/vernac_classifier.mli b/toplevel/vernac_classifier.mli deleted file mode 100644 index bc0c0c2b30..0000000000 --- a/toplevel/vernac_classifier.mli +++ /dev/null @@ -1,27 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* string - -(** What does a vernacular do *) -val classify_vernac : vernac_expr -> vernac_classification - -(** Install a vernacular classifier for VernacExtend *) -val declare_vernac_classifier : - string -> (raw_generic_argument list -> unit -> vernac_classification) -> unit - -(** Set by Stm *) -val set_undo_classifier : (vernac_expr -> vernac_classification) -> unit - -(** Standard constant classifiers *) -val classify_as_query : vernac_classification -val classify_as_sideeff : vernac_classification - diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 22e2f0c545..d5559f9762 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -495,12 +495,11 @@ let vernac_start_proof kind l lettop = start_proof_and_print (Global, Proof kind) l no_hook let qed_display_script = ref true -let show_script = ref (fun ?proof () -> ()) let vernac_end_proof ?proof = function | Admitted -> save_proof ?proof Admitted | Proved (_,_) as e -> - if is_verbose () && !qed_display_script then !show_script ?proof (); + if is_verbose () && !qed_display_script then Stm.show_script ?proof (); save_proof ?proof e (* A stupid macro that should be replaced by ``Exact c. Save.'' all along @@ -1594,7 +1593,7 @@ let vernac_show = function Constrextern.with_implicits msg_notice (pr_nth_open_subgoal n) | ShowProof -> show_proof () | ShowNode -> show_node () - | ShowScript -> !show_script () + | ShowScript -> Stm.show_script () | ShowExistentials -> show_top_evars () | ShowTree -> show_prooftree () | ShowProofNames -> @@ -1956,3 +1955,5 @@ let interp ?(verbosely=true) ?proof (loc,c) = if verbosely then Flags.verbosely (aux false) c else aux false c +let () = Hook.set Stm.interp_hook interp +let () = Hook.set Stm.process_error_hook Cerrors.process_vernac_interp_error diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index 9b49e57720..3fb3d001dc 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -12,7 +12,6 @@ val dump_global : Libnames.reference or_by_notation -> unit (** Vernacular entries *) -val show_script : (?proof:Proof_global.closed_proof -> unit -> unit) ref val show_prooftree : unit -> unit val show_node : unit -> unit diff --git a/toplevel/vi_checking.ml b/toplevel/vi_checking.ml deleted file mode 100644 index cb6e601362..0000000000 --- a/toplevel/vi_checking.ml +++ /dev/null @@ -1,152 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Stm.check_task f tasks ids && acc) true ts - -module Worker = Spawn.Sync(struct - let add_timeout ~sec f = - ignore(Thread.create (fun () -> - while true do - Unix.sleep sec; - if not (f ()) then Thread.exit () - done) - ()) -end) - -module IntOT = struct - type t = int - let compare = compare -end - -module Pool = Map.Make(IntOT) - -let schedule_vi_checking j fs = - if j < 1 then Errors.error "The number of workers must be bigger than 0"; - let jobs = ref [] in - List.iter (fun f -> - let f = - if Filename.check_suffix f ".vi" then Filename.chop_extension f - else f in - let long_f_dot_v, _,_,_, tasks, _ = Library.load_library_todo f in - Stm.set_compilation_hints long_f_dot_v; - let infos = Stm.info_tasks tasks in - let eta = List.fold_left (fun a (_,t,_) -> a +. t) 0.0 infos in - if infos <> [] then jobs := (f, eta, infos) :: !jobs) - fs; - let cmp_job (_,t1,_) (_,t2,_) = compare t2 t1 in - jobs := List.sort cmp_job !jobs; - let eta = ref (List.fold_left (fun a j -> a +. pi2 j) 0.0 !jobs) in - let pool : Worker.process Pool.t ref = ref Pool.empty in - let rec filter_argv b = function - | [] -> [] - | "-schedule-vi-checking" :: rest -> filter_argv true rest - | s :: rest when s.[0] = '-' && b -> filter_argv false (s :: rest) - | _ :: rest when b -> filter_argv b rest - | s :: rest -> s :: filter_argv b rest in - let pack = function - | [] -> [] - | ((f,_),_,_) :: _ as l -> - let rec aux last acc = function - | [] -> [last,acc] - | ((f',id),_,_) :: tl when last = f' -> aux last (id::acc) tl - | ((f',id),_,_) :: _ as l -> (last,acc) :: aux f' [] l in - aux f [] l in - let prog = Sys.argv.(0) in - let stdargs = filter_argv false (List.tl (Array.to_list Sys.argv)) in - let make_job () = - let cur = ref 0.0 in - let what = ref [] in - let j_left = j - Pool.cardinal !pool in - let take_next_file () = - let f, t, tasks = List.hd !jobs in - jobs := List.tl !jobs; - cur := !cur +. t; - what := (List.map (fun (n,t,id) -> (f,id),n,t) tasks) @ !what in - if List.length !jobs >= j_left then take_next_file () - else while !jobs <> [] && - !cur < max 0.0 (min 60.0 (!eta /. float_of_int j_left)) do - let f, t, tasks = List.hd !jobs in - jobs := List.tl !jobs; - let n, tt, id = List.hd tasks in - if List.length tasks > 1 then - jobs := (f, t -. tt, List.tl tasks) :: !jobs; - cur := !cur +. tt; - what := ((f,id),n,tt) :: !what; - done; - if !what = [] then take_next_file (); - eta := !eta -. !cur; - let cmp_job (f1,_,_) (f2,_,_) = compare f1 f2 in - List.flatten - (List.map (fun (f, tl) -> - "-check-vi-tasks" :: - String.concat "," (List.map string_of_int tl) :: [f]) - (pack (List.sort cmp_job !what))) in - let rc = ref 0 in - while !jobs <> [] || Pool.cardinal !pool > 0 do - while Pool.cardinal !pool < j && !jobs <> [] do - let args = Array.of_list (stdargs @ make_job ()) in - let proc, _, _ = Worker.spawn prog args in - pool := Pool.add (Worker.unixpid proc) proc !pool; - done; - let pid, ret = Unix.wait () in - if ret <> Unix.WEXITED 0 then rc := 1; - pool := Pool.remove pid !pool; - done; - exit !rc - -let schedule_vi_compilation j fs = - if j < 1 then Errors.error "The number of workers must be bigger than 0"; - let jobs = ref [] in - List.iter (fun f -> - let f = - if Filename.check_suffix f ".vi" then Filename.chop_extension f - else f in - let paths = Loadpath.get_paths () in - let _, long_f_dot_v = - System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in - let aux = Aux_file.load_aux_file_for long_f_dot_v in - let eta = - try float_of_string (Aux_file.get aux Loc.ghost "vo_compile_time") - with Not_found -> 0.0 in - jobs := (f, eta) :: !jobs) - fs; - let cmp_job (_,t1) (_,t2) = compare t2 t1 in - jobs := List.sort cmp_job !jobs; - let pool : Worker.process Pool.t ref = ref Pool.empty in - let rec filter_argv b = function - | [] -> [] - | "-schedule-vi2vo" :: rest -> filter_argv true rest - | s :: rest when s.[0] = '-' && b -> filter_argv false (s :: rest) - | _ :: rest when b -> filter_argv b rest - | s :: rest -> s :: filter_argv b rest in - let prog = Sys.argv.(0) in - let stdargs = filter_argv false (List.tl (Array.to_list Sys.argv)) in - let make_job () = - let f, t = List.hd !jobs in - jobs := List.tl !jobs; - [ "-vi2vo"; f ] in - let rc = ref 0 in - while !jobs <> [] || Pool.cardinal !pool > 0 do - while Pool.cardinal !pool < j && !jobs <> [] do - let args = Array.of_list (stdargs @ make_job ()) in - let proc, _, _ = Worker.spawn prog args in - pool := Pool.add (Worker.unixpid proc) proc !pool; - done; - let pid, ret = Unix.wait () in - if ret <> Unix.WEXITED 0 then rc := 1; - pool := Pool.remove pid !pool; - done; - exit !rc - - diff --git a/toplevel/vi_checking.mli b/toplevel/vi_checking.mli deleted file mode 100644 index 65414eda41..0000000000 --- a/toplevel/vi_checking.mli +++ /dev/null @@ -1,13 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* bool -val schedule_vi_checking : int -> string list -> unit - -val schedule_vi_compilation : int -> string list -> unit -- cgit v1.2.3