From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- stm/asyncTaskQueue.ml | 344 +++++++ stm/asyncTaskQueue.mli | 82 ++ stm/coqworkmgrApi.ml | 140 +++ stm/coqworkmgrApi.mli | 44 + stm/dag.ml | 134 +++ stm/dag.mli | 52 + stm/lemmas.ml | 478 +++++++++ stm/lemmas.mli | 62 ++ stm/proofworkertop.ml | 18 + stm/proofworkertop.mllib | 1 + stm/queryworkertop.ml | 18 + stm/queryworkertop.mllib | 1 + stm/spawned.ml | 86 ++ stm/spawned.mli | 22 + stm/stm.ml | 2407 +++++++++++++++++++++++++++++++++++++++++++++ stm/stm.mli | 132 +++ stm/stm.mllib | 12 + stm/tQueue.ml | 133 +++ stm/tQueue.mli | 28 + stm/tacworkertop.ml | 18 + stm/tacworkertop.mllib | 1 + stm/texmacspp.ml | 763 ++++++++++++++ stm/texmacspp.mli | 12 + stm/vcs.ml | 193 ++++ stm/vcs.mli | 90 ++ stm/vernac_classifier.ml | 227 +++++ stm/vernac_classifier.mli | 28 + stm/vio_checking.ml | 144 +++ stm/vio_checking.mli | 13 + stm/workerPool.ml | 128 +++ stm/workerPool.mli | 46 + 31 files changed, 5857 insertions(+) create mode 100644 stm/asyncTaskQueue.ml create mode 100644 stm/asyncTaskQueue.mli create mode 100644 stm/coqworkmgrApi.ml create mode 100644 stm/coqworkmgrApi.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/proofworkertop.ml create mode 100644 stm/proofworkertop.mllib create mode 100644 stm/queryworkertop.ml create mode 100644 stm/queryworkertop.mllib 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/tacworkertop.ml create mode 100644 stm/tacworkertop.mllib create mode 100644 stm/texmacspp.ml create mode 100644 stm/texmacspp.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/vio_checking.ml create mode 100644 stm/vio_checking.mli create mode 100644 stm/workerPool.ml create mode 100644 stm/workerPool.mli (limited to 'stm') diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml new file mode 100644 index 00000000..672527d9 --- /dev/null +++ b/stm/asyncTaskQueue.ml @@ -0,0 +1,344 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* string array + + (* run by the master, on a thread *) + val request_of_task : competence worker_status -> task -> request option + val task_match : competence worker_status -> task -> bool + val use_response : + competence worker_status -> task -> response -> + [ `Stay of competence * task list | `End ] + val on_marshal_error : string -> task -> unit + val on_task_cancellation_or_expiration_or_slave_death : task option -> unit + val forward_feedback : Feedback.feedback -> unit + + (* run by the worker *) + val perform : request -> response + + (* debugging *) + val name_of_task : task -> string + val name_of_request : request -> string + +end + +type expiration = bool ref + +module Make(T : Task) = struct + + exception Die + type response = + | Response of T.response + | RespFeedback of Feedback.feedback + | RespGetCounterNewUnivLevel + type request = Request of T.request + + type more_data = + | MoreDataUnivLevel of Univ.universe_level list + + let request_expiry_of_task (t, c) = T.request_of_task t, c + + let slave_respond (Request r) = + let res = T.perform r in + Response res + + 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 : 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 (CThread.thread_friendly_input_value ic : 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 (CThread.thread_friendly_input_value ic : more_data) + with Failure s | Invalid_argument s | Sys_error s -> + marshal_err ("unmarshal_more_data: "^s) + + let report_status ?(id = !Flags.async_proofs_worker_id) s = + Pp.feedback ~state_id:Stateid.initial (Feedback.WorkerStatus(id, s)) + + module Worker = Spawn.Sync(struct end) + + module Model = struct + + type process = Worker.process + type extra = (T.task * expiration) TQueue.t + + let spawn id = + let name = Printf.sprintf "%s:%d" !T.name id in + let proc, ic, oc = + let rec set_slave_opt = function + | [] -> !Flags.async_proofs_flags_for_workers @ + ["-toploop"; !T.name^"top"; + "-worker-id"; name; + "-async-proofs-worker-priority"; + Flags.string_of_priority !Flags.async_proofs_worker_priority] + | ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl + | ("-async-proofs" |"-toploop" |"-vi2vo" |"-compile" + |"-load-vernac-source" |"-compile-verbose" + |"-async-proofs-worker-priority" |"-worker-id") :: _ :: 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 (T.extra_env ()) (Unix.environment ()) in + Worker.spawn ~env Sys.argv.(0) args in + name, proc, CThread.prepare_in_channel_for_thread_friendly_io ic, oc + + let manager cpanel (id, proc, ic, oc) = + let { WorkerPool.extra = queue; exit; cancelled } = cpanel in + let exit () = report_status ~id "Dead"; exit () in + let last_task = ref None in + let worker_age = ref `Fresh in + let got_token = ref false in + let giveback_exec_token () = + if !got_token then (CoqworkmgrApi.giveback 1; got_token := false) in + let stop_waiting = ref false in + let expiration_date = ref (ref false) in + let pick_task () = + prerr_endline "waiting for a task"; + let pick age (t, c) = not !c && T.task_match age t in + let task, task_expiration = + TQueue.pop ~picky:(pick !worker_age) ~destroy:stop_waiting queue in + expiration_date := task_expiration; + last_task := Some task; + prerr_endline ("got task: "^T.name_of_task task); + task in + let add_tasks l = + List.iter (fun t -> TQueue.push queue (t,!expiration_date)) l in + let get_exec_token () = + ignore(CoqworkmgrApi.get 1); + got_token := true; + prerr_endline ("got execution token") in + let kill proc = + Worker.kill proc; + prerr_endline ("Worker exited: " ^ + 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 + let more_univs n = + CList.init 10 (fun _ -> + Universes.new_univ_level (Global.current_dirpath ())) in + + let rec kill_if () = + if not (Worker.is_alive proc) then () + else if cancelled () || !(!expiration_date) then + let () = stop_waiting := true in + let () = TQueue.signal_destruction queue in + Worker.kill proc + else + let () = Unix.sleep 1 in + kill_if () + in + let _ = Thread.create kill_if () in + + try while true do + report_status ~id "Idle"; + let task = pick_task () in + match T.request_of_task !worker_age task with + | None -> prerr_endline ("Task expired: " ^ T.name_of_task task) + | Some req -> + try + get_exec_token (); + marshal_request oc (Request req); + let rec continue () = + match unmarshal_response ic with + | RespGetCounterNewUnivLevel -> + marshal_more_data oc (MoreDataUnivLevel (more_univs 10)); + continue () + | RespFeedback fbk -> T.forward_feedback fbk; continue () + | Response resp -> + match T.use_response !worker_age task resp with + | `End -> raise Die + | `Stay(competence, new_tasks) -> + last_task := None; + giveback_exec_token (); + worker_age := `Old competence; + add_tasks new_tasks + in + continue () + with + | (Sys_error _|Invalid_argument _|End_of_file|Die) as e -> + raise e (* we pass the exception to the external handler *) + | MarshalError s -> T.on_marshal_error s task; raise Die + | e -> + pr_err ("Uncaught exception in worker manager: "^ + string_of_ppcmds (print e)); + flush_all (); raise Die + done with + | (Die | TQueue.BeingDestroyed) -> + giveback_exec_token (); kill proc; exit () + | Sys_error _ | Invalid_argument _ | End_of_file -> + giveback_exec_token (); + T.on_task_cancellation_or_expiration_or_slave_death !last_task; + kill proc; + exit () + end + + module Pool = WorkerPool.Make(Model) + + type queue = { + active : Pool.pool; + queue : (T.task * expiration) TQueue.t; + cleaner : Thread.t; + } + + let create size = + let cleaner queue = + while true do + try ignore(TQueue.pop ~picky:(fun (_,cancelled) -> !cancelled) queue) + with TQueue.BeingDestroyed -> Thread.exit () + done in + let queue = TQueue.create () in + { + active = Pool.create queue ~size; + queue; + cleaner = Thread.create cleaner queue; + } + + let destroy { active; queue } = + Pool.destroy active; + TQueue.destroy queue + + let enqueue_task { queue; active } (t, _ as item) = + prerr_endline ("Enqueue task "^T.name_of_task t); + TQueue.push queue item + + let cancel_worker { active } n = Pool.cancel n active + + let name_of_request (Request r) = T.name_of_request r + + let set_order { queue } cmp = + TQueue.set_order queue (fun (t1,_) (t2,_) -> cmp t1 t2) + + let join { queue; active } = + if not (Pool.is_empty active) then + TQueue.wait_until_n_are_waiting_and_queue_empty + (Pool.n_workers active + 1(*cleaner*)) + queue + + let cancel_all { queue; active } = + TQueue.clear queue; + Pool.cancel_all active + + let slave_ic = ref None + let slave_oc = ref None + + let init_stdout () = + let ic, oc = Spawned.get_channels () in + slave_oc := Some oc; slave_ic := Some 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 () = + Pool.worker_handshake (Option.get !slave_ic) (Option.get !slave_oc) + + let main_loop () = + let slave_feeder oc fb = + Marshal.to_channel oc (RespFeedback fb) []; flush oc in + Pp.set_feeder (fun x -> slave_feeder (Option.get !slave_oc) x); + Pp.log_via_feedback (); + Universes.set_remote_new_univ_level (bufferize (fun () -> + marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel; + match unmarshal_more_data (Option.get !slave_ic) with + | MoreDataUnivLevel l -> l)); + let working = ref false in + slave_handshake (); + while true do + try + working := false; + let request = unmarshal_request (Option.get !slave_ic) in + working := true; + report_status (name_of_request request); + let response = slave_respond request in + report_status "Idle"; + marshal_response (Option.get !slave_oc) response; + Ephemeron.clear () + 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 -> + pr_err ("Slave: critical exception: " ^ Pp.string_of_ppcmds (print e)); + flush_all (); exit 1 + done + + let clear { queue; active } = + assert(Pool.is_empty active); (* We allow that only if no slaves *) + TQueue.clear queue + + let snapshot { queue; active } = + List.map fst + (TQueue.wait_until_n_are_waiting_then_snapshot + (Pool.n_workers active) queue) + + let with_n_workers n f = + let q = create n in + try let rc = f q in destroy q; rc + with e -> let e = Errors.push e in destroy q; iraise e + + let n_workers { active } = Pool.n_workers active + +end + +module MakeQueue(T : Task) = struct include Make(T) end +module MakeWorker(T : Task) = struct include Make(T) end diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli new file mode 100644 index 00000000..78f295d3 --- /dev/null +++ b/stm/asyncTaskQueue.mli @@ -0,0 +1,82 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* string array + + (* run by the master, on a thread *) + val request_of_task : competence worker_status -> task -> request option + val task_match : competence worker_status -> task -> bool + val use_response : + competence worker_status -> task -> response -> + [ `Stay of competence * task list | `End ] + val on_marshal_error : string -> task -> unit + val on_task_cancellation_or_expiration_or_slave_death : task option -> unit + val forward_feedback : Feedback.feedback -> unit + + (* run by the worker *) + val perform : request -> response + + (* debugging *) + val name_of_task : task -> string + val name_of_request : request -> string + +end + +type expiration = bool ref + +module MakeQueue(T : Task) : sig + + type queue + + (* Number of workers, 0 = lazy local *) + val create : int -> queue + val destroy : queue -> unit + + val n_workers : queue -> int + + val enqueue_task : queue -> T.task * expiration -> unit + + (* blocking function that waits for the task queue to be empty *) + val join : queue -> unit + val cancel_all : queue -> unit + + val cancel_worker : queue -> WorkerPool.worker_id -> unit + + val set_order : queue -> (T.task -> T.task -> int) -> unit + + (* Take a snapshot (non destructive but waits until all workers are + * enqueued) *) + val snapshot : queue -> T.task list + + (* Clears the queue, only if the worker prool is empty *) + val clear : queue -> unit + + (* create a queue, run the function, destroy the queue. + * the user should call join *) + val with_n_workers : int -> (queue -> 'a) -> 'a + +end + +module MakeWorker(T : Task) : sig + + val main_loop : unit -> unit + val init_stdout : unit -> unit + +end diff --git a/stm/coqworkmgrApi.ml b/stm/coqworkmgrApi.ml new file mode 100644 index 00000000..c34d447e --- /dev/null +++ b/stm/coqworkmgrApi.ml @@ -0,0 +1,140 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* '\r' then s else String.sub s 0 (len - 1) + +let positive_int_of_string n = + try + let n = int_of_string n in + if n <= 0 then raise ParseError else n + with Invalid_argument _ | Failure _ -> raise ParseError + +let parse_request s = + if debug then Printf.eprintf "parsing '%s'\n" s; + match Str.split (Str.regexp " ") (strip_r s) with + | [ "HELLO"; "LOW" ] -> Hello Flags.Low + | [ "HELLO"; "HIGH" ] -> Hello Flags.High + | [ "GET"; n ] -> Get (positive_int_of_string n) + | [ "TRYGET"; n ] -> TryGet (positive_int_of_string n) + | [ "GIVEBACK"; n ] -> GiveBack (positive_int_of_string n) + | [ "PING" ] -> Ping + | _ -> raise ParseError + +let parse_response s = + if debug then Printf.eprintf "parsing '%s'\n" s; + match Str.split (Str.regexp " ") (strip_r s) with + | [ "TOKENS"; n ] -> Tokens (positive_int_of_string n) + | [ "NOLUCK" ] -> Noluck + | [ "PONG"; n; m; p ] -> + let n = try int_of_string n with _ -> raise ParseError in + let m = try int_of_string m with _ -> raise ParseError in + let p = try int_of_string p with _ -> raise ParseError in + Pong (n,m,p) + | _ -> raise ParseError + +let print_request = function + | Hello Flags.Low -> "HELLO LOW\n" + | Hello Flags.High -> "HELLO HIGH\n" + | Get n -> Printf.sprintf "GET %d\n" n + | TryGet n -> Printf.sprintf "TRYGET %d\n" n + | GiveBack n -> Printf.sprintf "GIVEBACK %d\n" n + | Ping -> "PING\n" + +let print_response = function + | Tokens n -> Printf.sprintf "TOKENS %d\n" n + | Noluck -> "NOLUCK\n" + | Pong (n,m,p) -> Printf.sprintf "PONG %d %d %d\n" n m p + +let connect s = + try + match Str.split (Str.regexp ":") s with + | [ h; p ] -> + let open Unix in + let s = socket PF_INET SOCK_STREAM 0 in + connect s (ADDR_INET (inet_addr_of_string h,int_of_string p)); + Some s + | _ -> None + with Unix.Unix_error _ -> None + +let manager = ref None + +let option_map f = function None -> None | Some x -> Some (f x) + +let init p = + try + let sock = Sys.getenv "COQWORKMGR_SOCK" in + manager := option_map (fun s -> + let cout = Unix.out_channel_of_descr s in + set_binary_mode_out cout true; + let cin = Unix.in_channel_of_descr s in + set_binary_mode_in cin true; + output_string cout (print_request (Hello p)); flush cout; + cin, cout) (connect sock) + with Not_found | End_of_file -> () + +let with_manager f g = + try + match !manager with + | None -> f () + | Some (cin, cout) -> g cin cout + with + | ParseError | End_of_file -> manager := None; f () + +let get n = + with_manager + (fun () -> + min n (min !Flags.async_proofs_n_workers !Flags.async_proofs_n_tacworkers)) + (fun cin cout -> + output_string cout (print_request (Get n)); + flush cout; + let l = input_line cin in + match parse_response l with + | Tokens m -> m + | _ -> raise (Failure "coqworkmgr protocol error")) + +let tryget n = + with_manager + (fun () -> + Some + (min n + (min !Flags.async_proofs_n_workers !Flags.async_proofs_n_tacworkers))) + (fun cin cout -> + output_string cout (print_request (TryGet n)); + flush cout; + let l = input_line cin in + match parse_response l with + | Tokens m -> Some m + | Noluck -> None + | _ -> raise (Failure "coqworkmgr protocol error")) + +let giveback n = + with_manager + (fun () -> ()) + (fun cin cout -> + output_string cout (print_request (GiveBack n)); + flush cout) + diff --git a/stm/coqworkmgrApi.mli b/stm/coqworkmgrApi.mli new file mode 100644 index 00000000..42dd39b9 --- /dev/null +++ b/stm/coqworkmgrApi.mli @@ -0,0 +1,44 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit + +(* blocking *) +val get : int -> int + +(* not blocking *) +val tryget : int -> int option +val giveback : int -> unit + +(* Low level *) +type request = + | Hello of Flags.priority + | Get of int + | TryGet of int + | GiveBack of int + | Ping + +type response = + | Tokens of int + | Noluck + | Pong of int * int * int (* cur, max, pid *) + +val connect : string -> Unix.file_descr option + +exception ParseError + +(* Intended to be used with input_line and output_string *) +val parse_request : string -> request +val parse_response : string -> response + +val print_request : request -> string +val print_response : response -> string diff --git a/stm/dag.ml b/stm/dag.ml new file mode 100644 index 00000000..d0515d3f --- /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 00000000..14ccdc9f --- /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 00000000..f2e68779 --- /dev/null +++ b/stm/lemmas.ml @@ -0,0 +1,478 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Globnames.global_reference -> 'a +let mk_hook hook = hook +let call_hook fix_exn hook l c = + try hook l c + with e when Errors.noncritical e -> + let e = Errors.push e in + iraise (fix_exn e) + +(* Support for mutually proved theorems *) + +let retrieve_first_recthm = function + | VarRef id -> + (pi2 (Global.lookup_named id),variable_opacity id) + | ConstRef cst -> + let cb = Global.lookup_constant cst in + (Global.body_of_constant_body 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, ctx), 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 add c cb e = + let exists c e = + try ignore(Environ.lookup_constant c e); true + with Not_found -> false in + if exists c e then e else Environ.add_constant c cb e in + let env = Declareops.fold_side_effects (fun env -> function + | SEsubproof (c, cb,_) -> add c cb env + | SEscheme (l,_) -> + List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l) + env (Declareops.uniquize_side_effects eff) in + let indexes = + search_guard Loc.ghost env + possible_indexes fixdecls in + (mkFix ((indexes,0),fixdecls), ctx), eff + | _ -> (body, ctx), 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), u) when + let mind = Global.lookup_mind kn in + mind.mind_finite == Decl_kinds.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),u) when + let mind = Global.lookup_mind kn in + mind.mind_finite <> Decl_kinds.CoFinite && 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),u) when + let mind = Global.lookup_mind kn in + Int.equal mind.mind_ntypes n && mind.mind_finite == Decl_kinds.CoFinite -> + [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 cstrs do_guard (locality,poly,kind) hook = + let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in + try + 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; + call_hook (fun exn -> exn) hook l r + with e when Errors.noncritical e -> + let e = Errors.push e in + iraise (fix_exn e) + +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,p,kind) norm ctx body opaq i (id,(t_i,(_,imps))) = + let t_i = norm t_i in + 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,ctx),p,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 ctx = Univ.ContextSet.to_context ctx in + let decl = (ParameterEntry (None,p,(t_i,ctx),None), k) in + let kn = declare_constant id ~local decl in + (locality,ConstRef kn,imps)) + | Some body -> + let body = norm body in + 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: " ++ Printer.pr_constr body) in + match locality with + | Discharge -> + let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p + ~univs:(Univ.ContextSet.to_context ctx) body_i in + let c = SectionLocalDef const in + let _ = declare_variable id (Lib.cwd(), c, k) in + (Discharge,VarRef id,imps) + | Local | Global -> + let ctx = Univ.ContextSet.to_context ctx in + let local = match locality with + | Local -> true + | Global -> false + | Discharge -> assert false + in + let const = + Declare.definition_entry ~types:t_i ~poly:p ~univs:ctx ~opaque:opaq body_i + 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,cstrs,do_guard,persistence,hook = proof in + save id const cstrs 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,cstrs,do_guard,persistence,hook = proof in + check_anonymity id save_ident; + save save_ident const cstrs do_guard persistence hook + +let save_anonymous_with_strength proof kind save_ident = + let id,const,cstrs,do_guard,_,hook = proof in + check_anonymity id save_ident; + (* we consider that non opaque behaves as local for discharge *) + save save_ident const cstrs do_guard (Global, const.const_entry_polymorphic, Proof kind) hook + +(* Admitted *) + +let admit hook () = + let (id,k,typ) = Pfedit.current_proof_statement () in + let ctx = + let evd = fst (Pfedit.get_current_goal_context ()) in + Evd.universe_context evd + in + let e = Pfedit.get_used_variables(), pi2 k, (typ, ctx), None in + let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in + let () = match 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 + call_hook (fun exn -> exn) 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,cstrs,persistence)) = + Pfedit.cook_this_proof proof + in + (** FIXME *) + id,{const with const_entry_opaque = opacity},cstrs,do_guard,persistence,hook + +let standard_proof_terminator compute_guard hook = + let open Proof_global in function + | Admitted -> + admit hook (); + Pp.feedback Feedback.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 universe_proof_terminator compute_guard hook = + let open Proof_global in function + | Admitted -> + admit (hook None) (); + Pp.feedback Feedback.AddedAxiom + | Proved (is_opaque,idopt,proof) -> + let proof = get_proof proof compute_guard + (hook (Some proof.Proof_global.universes)) 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 sigma ?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 sigma sign c ?init_tac terminator + +let start_proof_univs id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook = + let terminator = universe_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 sigma 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 ctx 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 ctx strength ref = + let ctx = match ctx with + | None -> Evd.empty_evar_universe_context + | Some ctx -> ctx + in + 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 + let subst = Evd.evar_universe_context_subst ctx in + let norm c = Universes.subst_opt_univs_constr subst c in + let ctx = Evd.evar_universe_context_set ctx in + let body = Option.map norm body in + List.map_i (save_remaining_recthms kind norm ctx 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; + call_hook (fun exn -> exn) hook strength ref) thms_data in + start_proof_univs id kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard + +let start_proof_com kind thms hook = + let env0 = Global.env () in + let evdref = ref (Evd.from_env env0) in + let thms = List.map (fun (sopt,(bl,t,guard)) -> + let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in + let t', imps' = interp_type_evars_impls ~impls env evdref t in + check_evars_are_solved env !evdref (Evd.empty,!evdref); + let ids = List.map pi1 ctx in + (compute_proof_name (pi1 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 + let evd, nf = Evarutil.nf_evars_and_universes !evdref in + let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in + start_proof_with_initialization kind evd + 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 ~keep_body_ucst_sepatate:false (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 00000000..d0669d7a --- /dev/null +++ b/stm/lemmas.mli @@ -0,0 +1,62 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Globnames.global_reference -> 'a) -> 'a declaration_hook + +val call_hook : + Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a + +(** A hook start_proof calls on the type of the definition being started *) +val set_start_hook : (types -> unit) -> unit + +val start_proof : Id.t -> goal_kind -> Evd.evar_map -> ?sign:Environ.named_context_val -> types -> + ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> + unit declaration_hook -> unit + +val start_proof_univs : Id.t -> goal_kind -> Evd.evar_map -> ?sign:Environ.named_context_val -> types -> + ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> + (Proof_global.proof_universes option -> 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 -> Evd.evar_map -> (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/proofworkertop.ml b/stm/proofworkertop.ml new file mode 100644 index 00000000..0e40c345 --- /dev/null +++ b/stm/proofworkertop.ml @@ -0,0 +1,18 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + Flags.make_silent true; + W.init_stdout (); + CoqworkmgrApi.init !Flags.async_proofs_worker_priority; + args) + +let () = Coqtop.toploop_run := W.main_loop + diff --git a/stm/proofworkertop.mllib b/stm/proofworkertop.mllib new file mode 100644 index 00000000..f9f6c22d --- /dev/null +++ b/stm/proofworkertop.mllib @@ -0,0 +1 @@ +Proofworkertop diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml new file mode 100644 index 00000000..c8e6432b --- /dev/null +++ b/stm/queryworkertop.ml @@ -0,0 +1,18 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + Flags.make_silent true; + W.init_stdout (); + CoqworkmgrApi.init !Flags.async_proofs_worker_priority; + args) + +let () = Coqtop.toploop_run := W.main_loop + diff --git a/stm/queryworkertop.mllib b/stm/queryworkertop.mllib new file mode 100644 index 00000000..c2f73089 --- /dev/null +++ b/stm/queryworkertop.mllib @@ -0,0 +1 @@ +Queryworkertop diff --git a/stm/spawned.ml b/stm/spawned.ml new file mode 100644 index 00000000..18159288 --- /dev/null +++ b/stm/spawned.ml @@ -0,0 +1,86 @@ +(************************************************************************) +(* 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; + let cin = CThread.prepare_in_channel_for_thread_friendly_io cin in + 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 CThread.thread_friendly_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.quick_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; + let stdin = CThread.prepare_in_channel_for_thread_friendly_io stdin in + 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 00000000..d9e7baff --- /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 -> CThread.thread_ic * out_channel + diff --git a/stm/stm.ml b/stm/stm.ml new file mode 100644 index 00000000..7b246854 --- /dev/null +++ b/stm/stm.ml @@ -0,0 +1,2407 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + feedback ~state_id Feedback.Processed) () + +let state_ready, state_ready_hook = Hook.make + ~default:(fun state_id -> ()) () + +let forward_feedback, forward_feedback_hook = Hook.make + ~default:(function + | { Feedback.id = Feedback.Edit edit_id; route; contents } -> + feedback ~edit_id ~route contents + | { Feedback.id = Feedback.State state_id; route; contents } -> + feedback ~state_id ~route contents) () + +let parse_error, parse_error_hook = Hook.make + ~default:(function + | Feedback.Edit edit_id -> fun loc msg -> + feedback ~edit_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg)) + | Feedback.State state_id -> fun loc msg -> + feedback ~state_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))) () + +let execution_error, execution_error_hook = Hook.make + ~default:(fun state_id loc msg -> + feedback ~state_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))) () + +let unreachable_state, unreachable_state_hook = Hook.make + ~default:(fun _ -> ()) () + +include Hook + +(* enables: Hooks.(call foo args) *) +let call = get + +let call_process_error_once = + let processed : unit Exninfo.t = Exninfo.make () in + fun (_, info as ei) -> + match Exninfo.get info processed with + | Some _ -> ei + | None -> + let e, info = call process_error ei in + let info = Exninfo.add info processed () in + e, info + +end + +(* 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 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 ?route { verbose; loc; expr } = + let rec internal_command = function + | VernacResetName _ | VernacResetInitial | VernacBack _ + | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _ + | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true + | VernacTime el -> List.for_all (fun (_,e) -> internal_command e) el + | _ -> false in + if internal_command expr then begin + prerr_endline ("ignoring " ^ string_of_ppcmds(pr_vernac expr)) + end else begin + set_id_for_feedback ?route (Feedback.State id); + Aux_file.record_in_aux_set_at loc; + prerr_endline ("interpreting " ^ string_of_ppcmds(pr_vernac expr)); + try Hooks.(call interp ?verbosely:(Some verbose) ?proof (loc, expr)) + with e -> + let e = Errors.push e in + iraise Hooks.(call_process_error_once e) + end + +(* Wrapper for Vernac.parse_sentence to set the feedback id *) +let vernac_parse ?newtip ?route eid s = + let feedback_id = + if Option.is_empty newtip then Feedback.Edit eid + else Feedback.State (Option.get newtip) in + set_id_for_feedback ?route feedback_id; + let pa = Pcoq.Gram.parsable (Stream.of_string s) in + Flags.with_option Flags.we_are_parsing (fun () -> + try + match Pcoq.Gram.entry_parse Pcoq.main_entry pa with + | None -> raise (Invalid_argument "vernac_parse") + | Some ast -> ast + with e when Errors.noncritical e -> + let (e, info) = Errors.push e in + let loc = Option.default Loc.ghost (Loc.get_loc info) in + Hooks.(call parse_error feedback_id loc (iprint (e, info))); + iraise (e, info)) + () + +let pr_open_cur_subgoals () = + try Printer.pr_open_subgoals () + with Proof_global.NoCurrentProof -> str"" + +module Vcs_ = Vcs.Make(Stateid) +type future_proof = Proof_global.closed_proof_output 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 = { + cast : ast; + cids : Id.t list; + cqueue : [ `MainQueue | `TacQueue of cancel_switch | `QueryQueue of cancel_switch ] } +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 * Stateid.t option + | `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,None); next = n } + | [n, Fork x; p, Noop] -> { step = `Fork (x,Some p); next = n } + | [p, Noop; n, Fork x] -> { step = `Fork (x,Some p); next = n } + | [n, Qed x; p, Noop] + | [p, Noop; n, Qed x] -> { step = `Qed (x,p); next = n } + | [n, Sideff 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 (* }}} *) + +(*************************** THE DOCUMENT *************************************) +(******************************************************************************) + +(* Imperative wrap around VCS to obtain _the_ VCS that is the + * representation of the document Coq is currently processing *) +module VCS : sig + + exception Expired + + module Branch : (module type of Vcs_.Branch with type t = Vcs_.Branch.t) + type id = Stateid.t + type 'branch_type branch_info = 'branch_type Vcs_.branch_info = { + kind : [> `Master] as 'branch_type; + root : id; + pos : id; + } + + type vcs = (branch_type, transaction, vcs state_info) 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 : ?id:Stateid.t -> 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 + + (* cuts from start -> stop, raising Expired if some nodes are not there *) + val slice : start:id -> stop:id -> vcs + val nodes_in_slice : start:id -> stop:id -> Stateid.t list + + val create_cluster : id list -> qed:id -> start:id -> unit + val cluster_of : id -> (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_" ^ Str.global_replace (Str.regexp " ") "_" (System.process_id ()) in + let string_of_transaction = function + | Cmd { cast = 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 [xlabel=%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 ?(id=Stateid.fresh ()) () = + assert(Vcs_.get_info !vcs id = None); + 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; + if Flags.async_proofs_is_master () then Hooks.(call state_ready id) + let get_state id = (get_info id).state + let reached id b = + let 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 nodes_in_slice ~start ~stop = + let rec aux id = + if Stateid.equal id start then [] else + match visit id with + | { next = n; step = `Cmd x } -> (id,Cmd x) :: aux n + | { next = n; step = `Alias x } -> (id,Alias x) :: aux n + | { next = n; step = `Sideff (`Ast (x,_)) } -> + (id,Sideff (Some x)) :: aux n + | _ -> anomaly(str("Cannot slice from "^ Stateid.to_string start ^ + " to "^Stateid.to_string stop)) + in aux stop + + let slice ~start ~stop = + let l = nodes_in_slice ~start ~stop in + let copy_info v id = + Vcs_.set_info v id + { (get_info id) with state = None; vcs_backup = None,None } in + let copy_info_w_state v id = + Vcs_.set_info v id { (get_info id) with vcs_backup = None,None } in + let v = Vcs_.empty start in + let v = copy_info v start in + let v = List.fold_right (fun (id,tr) v -> + let v = Vcs_.commit v id tr in + let v = copy_info v id in + v) l v in + (* Stm should have reached the beginning of proof *) + assert (not (Option.is_empty (get_info start).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 stop + + let nodes_in_slice ~start ~stop = + List.rev (List.map fst (nodes_in_slice ~start ~stop)) + + let create_cluster l ~qed ~start = vcs := create_cluster !vcs l (qed,start) + 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) }, _) + | `Cmd { cqueue = `TacQueue cancel_switch } + | `Cmd { cqueue = `QueryQueue cancel_switch } -> + cancel_switch := true + | _ -> ()) + erased_nodes; + vcs := new_vcs + + module NB : sig (* Non blocking Sys.command *) + + val command : now:bool -> (unit -> unit) -> unit + + end = struct + + let m = Mutex.create () + let c = Condition.create () + let job = ref None + let worker = ref None + + let set_last_job j = + Mutex.lock m; + job := Some j; + Condition.signal c; + Mutex.unlock m + + let get_last_job () = + Mutex.lock m; + while Option.is_empty !job do Condition.wait c m; done; + match !job with + | None -> assert false + | Some x -> job := None; Mutex.unlock m; x + + let run_command () = + try while true do get_last_job () () done + with e -> () (* No failure *) + + let command ~now job = + if now then job () + else begin + set_last_job job; + if Option.is_empty !worker then + worker := Some (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 (* }}} *) + +let state_of_id id = + try `Valid (VCS.get_info id).state + with VCS.Expired -> `Expired + + +(****** A cache: fills in the nodes of the VCS document with their value ******) +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 : + ?safe_id:Stateid.t -> + ?redefine:bool -> ?cache:Summary.marshallable -> + ?feedback_processed:bool -> (unit -> unit) -> Stateid.t -> unit + + val install_cached : Stateid.t -> unit + val is_cached : ?cache:Summary.marshallable -> Stateid.t -> bool + + + val exn_on : Stateid.t -> ?valid:Stateid.t -> iexn -> iexn + (* to send states across worker/master *) + type frozen_state + val get_cached : Stateid.t -> frozen_state + val same_env : frozen_state -> frozen_state -> bool + type partial_state = + [ `Full of frozen_state | `Proof of Stateid.t * Proof_global.state ] + val proof_part_of_frozen : frozen_state -> Proof_global.state + val assign : Stateid.t -> partial_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) + + type frozen_state = state + type partial_state = + [ `Full of frozen_state | `Proof of Stateid.t * Proof_global.state ] + let proof_part_of_frozen { proof } = proof + + let freeze marhallable id = VCS.set_state id (freeze_global_state marhallable) + + let is_cached ?(cache=`No) id = + if Stateid.equal id !cur_id then + try match VCS.get_info id with + | { state = None } when cache = `Yes -> freeze `No id; true + | { state = None } when cache = `Shallow -> freeze `Shallow id; true + | _ -> true + with VCS.Expired -> false + else + try match VCS.get_info id with + | { state = Some _ } -> true + | _ -> false + with VCS.Expired -> 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 + + 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 what = + if VCS.get_state id <> None then () else + try match what with + | `Full s -> VCS.set_state id s + | `Proof(ontop,p) -> + if is_cached ontop then ( + VCS.set_state id { (get_cached ontop) with proof = p }) + with VCS.Expired -> () + + let exn_on id ?valid (e, info) = + match Stateid.get info with + | Some _ -> (e, info) + | None -> + let loc = Option.default Loc.ghost (Loc.get_loc info) in + let (e, info) = Hooks.(call_process_error_once (e, info)) in + Hooks.(call execution_error id loc (iprint (e, info))); + (e, Stateid.add info ?valid id) + + let same_env { system = s1 } { system = s2 } = + let s1 = States.summary_of_state s1 in + let e1 = Summary.project_summary s1 [Global.global_env_summary_name] in + let s2 = States.summary_of_state s2 in + let e2 = Summary.project_summary s2 [Global.global_env_summary_name] in + Summary.pointer_equal e1 e2 + + let define ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true) + f id + = + feedback ~state_id:id Feedback.(ProcessingIn !Flags.async_proofs_worker_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; + if feedback_processed then + Hooks.(call state_computed id ~in_cache:false); + VCS.reached id true; + if Proof_global.there_are_pending_proofs () then + VCS.goals id (Proof_global.get_open_goals ()); + with e -> + let (e, info) = Errors.push e in + let good_id = !cur_id in + cur_id := Stateid.dummy; + VCS.reached id false; + Hooks.(call unreachable_state id); + match Stateid.get info, safe_id with + | None, None -> iraise (exn_on id ~valid:good_id (e, info)) + | None, Some good_id -> iraise (exn_on id ~valid:good_id (e, info)) + | Some _, None -> iraise (e, info) + | Some (_,at), Some id -> iraise (e, Stateid.add info ~valid:id at) + +end (* }}} *) + + +(****************************** CRUFT *****************************************) +(******************************************************************************) + +(* 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 () = + List.iter (fun current_branch -> + let mine = current_branch, VCS.get_branch current_branch in + let info = VCS.get_info (VCS.get_branch_pos current_branch) in + let others = + CList.map_filter (fun b -> + if Vcs_.Branch.equal b current_branch then None + else Some(b, VCS.get_branch b)) (VCS.branches ()) in + let backup = if fst info.vcs_backup <> None then fst info.vcs_backup + else Some (VCS.backup ()) in + let branches = if snd info.vcs_backup <> None then snd info.vcs_backup + else Some { mine; others } in + info.vcs_backup <- backup, branches) + [VCS.current_branch (); VCS.Branch.master] + + let 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 branches_of id = + let info = VCS.get_info id in + match info.vcs_backup with + | _, None -> + anomaly(str"Backtrack.branches_of "++str(Stateid.to_string id)++ + str": a state with no vcs_backup") + | _, Some x -> x + + let rec fold_until f acc id = + let next acc = + if id = Stateid.initial then raise Not_found + else fold_until f acc (VCS.visit id).next in + let info = VCS.get_info id in + match info.vcs_backup with + | None, _ -> next acc + | Some vcs, _ -> + let ids = + if id = Stateid.initial || id = Stateid.dummy then [] else + match VCS.visit id with + | { step = `Fork ((_,_,_,l),_) } -> l + | { step = `Cmd { cids = 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 + if n = 1 && !Flags.coqtop_ui && not !Flags.batch_mode && + not !Flags.print_emacs then + VtStm (VtBack oid, false), VtNow + else 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), not !Flags.print_emacs), 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 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 + +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 + +exception RemoteException of std_ppcmds +let _ = Errors.register_handler (function + | RemoteException ppcmd -> ppcmd + | _ -> raise Unhandled) + +(****************************** THE SCHEDULER *********************************) +(******************************************************************************) + +module rec ProofTask : sig + + type competence = Stateid.t list + type task_build_proof = { + t_exn_info : Stateid.t * Stateid.t; + t_start : Stateid.t; + t_stop : Stateid.t; + t_states : competence; + t_assign : Proof_global.closed_proof_output Future.assignement -> unit; + t_loc : Loc.t; + t_uuid : Future.UUID.t; + t_name : string } + + type task = + | BuildProof of task_build_proof + | States of Stateid.t list + + type request = + | ReqBuildProof of (Future.UUID.t,VCS.vcs) Stateid.request * competence + | ReqStates of Stateid.t list + + include AsyncTaskQueue.Task + with type task := task + and type competence := competence + and type request := request + + val build_proof_here : + Stateid.t * Stateid.t -> Loc.t -> Stateid.t -> + Proof_global.closed_proof_output Future.computation + +end = struct (* {{{ *) + + let forward_feedback msg = Hooks.(call forward_feedback msg) + + type competence = Stateid.t list + type task_build_proof = { + t_exn_info : Stateid.t * Stateid.t; + t_start : Stateid.t; + t_stop : Stateid.t; + t_states : competence; + t_assign : Proof_global.closed_proof_output Future.assignement -> unit; + t_loc : Loc.t; + t_uuid : Future.UUID.t; + t_name : string } + + type task = + | BuildProof of task_build_proof + | States of Stateid.t list + + type request = + | ReqBuildProof of (Future.UUID.t,VCS.vcs) Stateid.request * competence + | ReqStates of Stateid.t list + + type error = { + e_error_at : Stateid.t; + e_safe_id : Stateid.t; + e_msg : std_ppcmds; + e_safe_states : Stateid.t list } + + type response = + | RespBuiltProof of Proof_global.closed_proof_output * float + | RespError of error + | RespStates of (Stateid.t * State.partial_state) list + | RespDone + + let name = ref "proofworker" + let extra_env () = !async_proofs_workers_extra_env + + let task_match age t = + match age, t with + | `Fresh, BuildProof _ -> true + | `Old my_states, States l -> + List.for_all (fun x -> CList.mem_f Stateid.equal x my_states) l + | _ -> false + + let name_of_task = function + | BuildProof t -> "proof: " ^ t.t_name + | States l -> "states: " ^ String.concat "," (List.map Stateid.to_string l) + let name_of_request = function + | ReqBuildProof(r,_) -> "proof: " ^ r.Stateid.name + | ReqStates l -> "states: "^String.concat "," (List.map Stateid.to_string l) + + let request_of_task age = function + | States l -> Some (ReqStates l) + | BuildProof { t_exn_info;t_start;t_stop;t_loc;t_uuid;t_name;t_states } -> + assert(age = `Fresh); + try Some (ReqBuildProof ({ + Stateid.exn_info = t_exn_info; + stop = t_stop; + document = VCS.slice ~start:t_start ~stop:t_stop; + loc = t_loc; + uuid = t_uuid; + name = t_name }, t_states)) + with VCS.Expired -> None + + let use_response (s : competence AsyncTaskQueue.worker_status) t r = + match s, t, r with + | `Old c, States _, RespStates l -> + List.iter (fun (id,s) -> State.assign id s) l; `End + | `Fresh, BuildProof { t_assign; t_loc; t_name; t_states }, + RespBuiltProof (pl, time) -> + feedback (Feedback.InProgress ~-1); + t_assign (`Val pl); + record_pb_time t_name t_loc time; + if not !Flags.async_proofs_full then `End + else `Stay(t_states,[States t_states]) + | `Fresh, BuildProof { t_assign; t_loc; t_name; t_states }, + RespError { e_error_at; e_safe_id = valid; e_msg; e_safe_states } -> + feedback (Feedback.InProgress ~-1); + let info = Stateid.add ~valid Exninfo.null e_error_at in + let e = (RemoteException e_msg, info) in + t_assign (`Exn e); + `Stay(t_states,[States e_safe_states]) + | _ -> assert false + + let on_task_cancellation_or_expiration_or_slave_death = function + | None -> () + | Some (States _) -> () + | Some (BuildProof { t_start = start; t_assign }) -> + let s = "Worker dies or task expired" in + let info = Stateid.add ~valid:start Exninfo.null start in + let e = (RemoteException (strbrk s), info) in + t_assign (`Exn e); + Hooks.(call execution_error start Loc.ghost (strbrk s)); + feedback (Feedback.InProgress ~-1) + + let build_proof_here (id,valid) loc eop = + Future.create (State.exn_on id ~valid) (fun () -> + 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 perform_buildp { Stateid.exn_info; stop; document; loc } my_states = + try + VCS.restore document; + VCS.print (); + let proof, future_proof, time = + let wall_clock = Unix.gettimeofday () in + let fp = build_proof_here exn_info loc stop in + let proof = Future.force fp in + proof, fp, Unix.gettimeofday () -. wall_clock in + (* We typecheck the proof with the kernel (in the worker) to spot + * the few errors tactics don't catch, like the "fix" tactic building + * a bad fixpoint *) + let fix_exn = Future.fix_exn_of future_proof in + let checked_proof = Future.chain ~pure:false future_proof (fun p -> + let pobject, _ = + Proof_global.close_future_proof stop (Future.from_val ~fix_exn p) in + let terminator = (* The one sent by master is an InvalidKey *) + Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in + vernac_interp stop + ~proof:(pobject, terminator) + { verbose = false; loc; + expr = (VernacEndProof (Proved (true,None))) }) in + ignore(Future.join checked_proof); + RespBuiltProof(proof,time) + with + | e when Errors.noncritical e -> + let (e, info) = Errors.push e in + (* This can happen if the proof is broken. The error has also been + * signalled as a feedback, hence we can silently recover *) + let e_error_at, e_safe_id = match Stateid.get info with + | Some (safe, err) -> err, safe + | None -> Stateid.dummy, Stateid.dummy in + let e_msg = iprint (e, info) in + prerr_endline "failed with the following exception:"; + prerr_endline (string_of_ppcmds e_msg); + let e_safe_states = List.filter State.is_cached my_states in + RespError { e_error_at; e_safe_id; e_msg; e_safe_states } + + let perform_states query = + if query = [] then [] else + let initial = + let rec aux id = + try match VCS.visit id with { next } -> aux next + with VCS.Expired -> id in + aux (List.hd query) in + let get_state seen id = + let prev = + try + let { next = prev; step } = VCS.visit id in + if State.is_cached prev && List.mem prev seen + then Some (prev, State.get_cached prev, step) + else None + with VCS.Expired -> None in + let this = + if State.is_cached id then Some (State.get_cached id) else None in + match prev, this with + | _, None -> None + | Some (prev, o, `Cmd { cast = { expr = VernacSolve _ }}), Some n + when State.same_env o n -> (* A pure tactic *) + Some (id, `Proof (prev, State.proof_part_of_frozen n)) + | Some _, Some s -> + msg_warning (str "Sending back a fat state"); + Some (id, `Full s) + | _, Some s -> Some (id, `Full s) in + let rec aux seen = function + | [] -> [] + | id :: rest -> + match get_state seen id with + | None -> aux seen rest + | Some stuff -> stuff :: aux (id :: seen) rest in + aux [initial] query + + let perform = function + | ReqBuildProof (bp,states) -> perform_buildp bp states + | ReqStates sl -> RespStates (perform_states sl) + + let on_marshal_error s = function + | States _ -> msg_error(strbrk("Marshalling error: "^s^". "^ + "The system state could not be sent to the master process.")) + | BuildProof { t_exn_info; t_stop; t_assign; t_loc } -> + msg_error(strbrk("Marshalling error: "^s^". "^ + "The system state could not be sent to the worker process. "^ + "Falling back to local, lazy, evaluation.")); + t_assign(`Comp(build_proof_here t_exn_info t_loc t_stop)); + feedback (Feedback.InProgress ~-1) + +end (* }}} *) + +(* Slave processes (if initialized, otherwise local lazy evaluation) *) +and 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 + + type 'a tasks = ('a,VCS.vcs) Stateid.request list + val dump_snapshot : unit -> Future.UUID.t tasks + val check_task : string -> int tasks -> int -> bool + val info_tasks : 'a tasks -> (string * float * int) list + val finish_task : + string -> + Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs -> + int tasks -> int -> Library.seg_univ + + val cancel_worker : WorkerPool.worker_id -> unit + + val reset_task_queue : unit -> unit + + val set_perspective : Stateid.t list -> unit + +end = struct (* {{{ *) + + module TaskQueue = AsyncTaskQueue.MakeQueue(ProofTask) + + let queue = ref None + + let init () = + if Flags.async_proofs_is_master () then + queue := Some (TaskQueue.create !Flags.async_proofs_n_workers) + else + queue := Some (TaskQueue.create 0) + + let check_task_aux extra name l i = + let { Stateid.stop; document; loc; name = r_name } = List.nth l i in + msg_info( + str(Printf.sprintf "Checking task %d (%s%s) of %s" i r_name extra name)); + VCS.restore document; + let start = + let rec aux cur = + try aux (VCS.visit cur).next + with VCS.Expired -> cur in + aux stop in + try + Reach.known_state ~cache:`No stop; + (* The original terminator, a hook, has not been saved in the .vio*) + Proof_global.set_terminator + (Lemmas.standard_proof_terminator [] + (Lemmas.mk_hook (fun _ _ -> ()))); + let proof = + Proof_global.close_proof ~keep_body_ucst_sepatate:true (fun x -> x) in + (* We jump at the beginning since the kernel handles side effects by also + * looking at the ones that happen to be present in the current env *) + Reach.known_state ~cache:`No start; + vernac_interp stop ~proof + { verbose = false; loc; + expr = (VernacEndProof (Proved (true,None))) }; + Some proof + with e -> + let (e, info) = Errors.push e in + (try match Stateid.get info with + | None -> + pperrnl ( + str"File " ++ str name ++ str ": proof of " ++ str r_name ++ + spc () ++ iprint (e, info)) + | Some (_, cur) -> + match VCS.visit cur with + | { step = `Cmd { cast = { loc } } } + | { step = `Fork (( { loc }, _, _, _), _) } + | { step = `Qed ( { qast = { loc } }, _) } + | { step = `Sideff (`Ast ( { loc }, _)) } -> + let start, stop = Loc.unloc loc in + pperrnl ( + str"File " ++ str name ++ str ": proof of " ++ str r_name ++ + str ": chars " ++ int start ++ str "-" ++ int stop ++ + spc () ++ iprint (e, info)) + | _ -> + pperrnl ( + str"File " ++ str name ++ str ": proof of " ++ str r_name ++ + spc () ++ iprint (e, info)) + with e -> + 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 = (List.nth l i).Stateid.uuid in + match check_task_aux (Printf.sprintf ", bucket %d" bucket) name l i with + | None -> exit 1 + | Some (po,_) -> + 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 + let o = match c.Declarations.const_body with + | Declarations.OpaqueDef o -> o + | _ -> assert false in + let uc = + Option.get + (Opaqueproof.get_constraints (Global.opaque_tables ()) o) in + let pr = + Future.from_val (Option.get (Global.body_of_constant_body c)) in + let uc = + Future.chain + ~greedy:true ~pure:true uc Univ.hcons_universe_context_set 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.ContextSet.union cst extra, 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 { Stateid.loc; name } -> + 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 + name, max (time1 +. time2) 0.0001,i) 0 l + + let set_perspective idl = + let open Stateid in + let open ProofTask in + let overlap s1 s2 = + List.exists (fun x -> CList.mem_f Stateid.equal x s2) s1 in + let overlap_rel s1 s2 = + match overlap s1 idl, overlap s2 idl with + | true, true | false, false -> 0 + | true, false -> -1 + | false, true -> 1 in + TaskQueue.set_order (Option.get !queue) (fun task1 task2 -> + match task1, task2 with + | BuildProof { t_states = s1 }, + BuildProof { t_states = s2 } -> overlap_rel s1 s2 + | _ -> 0) + + let build_proof ~loc ~exn_info ~start ~stop ~name:pname = + let id, valid as t_exn_info = exn_info in + let cancel_switch = ref false in + if TaskQueue.n_workers (Option.get !queue) = 0 then + if !Flags.compilation_mode = Flags.BuildVio then begin + let f,assign = + Future.create_delegate ~blocking:true (State.exn_on id ~valid) in + let t_uuid = Future.uuid f in + let task = ProofTask.(BuildProof { + t_exn_info; t_start = start; t_stop = stop; + t_assign = assign; t_loc = loc; t_uuid; t_name = pname; + t_states = VCS.nodes_in_slice ~start ~stop }) in + TaskQueue.enqueue_task (Option.get !queue) (task,cancel_switch); + f, cancel_switch + end else + ProofTask.build_proof_here t_exn_info loc stop, cancel_switch + else + let f, t_assign = Future.create_delegate (State.exn_on id ~valid) in + let t_uuid = Future.uuid f in + feedback (Feedback.InProgress 1); + let task = ProofTask.(BuildProof { + t_exn_info; t_start = start; t_stop = stop; t_assign; + t_loc = loc; t_uuid; t_name = pname; + t_states = VCS.nodes_in_slice ~start ~stop }) in + TaskQueue.enqueue_task (Option.get !queue) (task,cancel_switch); + f, cancel_switch + + let wait_all_done () = TaskQueue.join (Option.get !queue) + + let cancel_worker n = TaskQueue.cancel_worker (Option.get !queue) n + + (* For external users this name is nicer than request *) + type 'a tasks = ('a,VCS.vcs) Stateid.request list + let dump_snapshot () = + let tasks = TaskQueue.snapshot (Option.get !queue) in + let reqs = + CList.map_filter + ProofTask.(fun x -> + match request_of_task `Fresh x with + | Some (ReqBuildProof (r, _)) -> Some r + | _ -> None) + tasks in + prerr_endline (Printf.sprintf "dumping %d tasks\n" (List.length reqs)); + reqs + + let reset_task_queue () = TaskQueue.clear (Option.get !queue) + +end (* }}} *) + +and TacTask : sig + + type output = Constr.constr * Evd.evar_universe_context + type task = { + t_state : Stateid.t; + t_state_fb : Stateid.t; + t_assign : output Future.assignement -> unit; + t_ast : ast; + t_goal : Goal.goal; + t_kill : unit -> unit; + t_name : string } + + include AsyncTaskQueue.Task with type task := task + +end = struct (* {{{ *) + + type output = Constr.constr * Evd.evar_universe_context + + let forward_feedback msg = Hooks.(call forward_feedback msg) + + type task = { + t_state : Stateid.t; + t_state_fb : Stateid.t; + t_assign : output Future.assignement -> unit; + t_ast : ast; + t_goal : Goal.goal; + t_kill : unit -> unit; + t_name : string } + + type request = { + r_state : Stateid.t; + r_state_fb : Stateid.t; + r_document : VCS.vcs option; + r_ast : ast; + r_goal : Goal.goal; + r_name : string } + + type response = + | RespBuiltSubProof of output + | RespError of std_ppcmds + + let name = ref "tacworker" + let extra_env () = [||] + type competence = unit + let task_match _ _ = true + + (* run by the master, on a thread *) + let request_of_task age { t_state; t_state_fb; t_ast; t_goal; t_name } = + try Some { + r_state = t_state; + r_state_fb = t_state_fb; + r_document = + if age <> `Fresh then None + else Some (VCS.slice ~start:t_state ~stop:t_state); + r_ast = t_ast; + r_goal = t_goal; + r_name = t_name } + with VCS.Expired -> None + + let use_response _ { t_assign; t_state; t_state_fb; t_kill } resp = + match resp with + | RespBuiltSubProof o -> t_assign (`Val o); `Stay ((),[]) + | RespError msg -> + let info = Stateid.add ~valid:t_state Exninfo.null t_state_fb in + let e = (RemoteException msg, info) in + t_assign (`Exn e); + t_kill (); + `Stay ((),[]) + + let on_marshal_error err { t_name } = + pr_err ("Fatal marshal error: " ^ t_name ); + flush_all (); exit 1 + + let on_task_cancellation_or_expiration_or_slave_death = function + | Some { t_kill } -> t_kill () + | _ -> () + + let perform { r_state = id; r_state_fb; r_document = vcs; r_ast; r_goal } = + Option.iter VCS.restore vcs; + try + Reach.known_state ~cache:`No id; + let t, uc = Future.purify (fun () -> + vernac_interp r_state_fb r_ast; + let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in + match Evd.(evar_body (find sigma r_goal)) with + | Evd.Evar_empty -> Errors.errorlabstrm "Stm" (str "no progress") + | Evd.Evar_defined t -> + let t = Evarutil.nf_evar sigma t in + if Evarutil.is_ground_term sigma t then + t, Evd.evar_universe_context sigma + else Errors.errorlabstrm "Stm" (str"The solution is not ground")) + () in + RespBuiltSubProof (t,uc) + with e when Errors.noncritical e -> RespError (Errors.print e) + + let name_of_task { t_name } = t_name + let name_of_request { r_name } = r_name + +end (* }}} *) + +and Partac : sig + + val vernac_interp : + cancel_switch -> int -> Stateid.t -> Stateid.t -> ast -> unit + +end = struct (* {{{ *) + + module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask) + + let vernac_interp cancel nworkers safe_id id { verbose; loc; expr = e } = + let e, etac, time, fail = + let rec find time fail = function + | VernacSolve(_,_,re,b) -> re, b, time, fail + | VernacTime [_,e] -> find true fail e + | VernacFail e -> find time true e + | _ -> errorlabstrm "Stm" (str"unsupported") in find false false e in + Hooks.call Hooks.with_fail fail (fun () -> + (if time then System.with_time false else (fun x -> x)) (fun () -> + ignore(TaskQueue.with_n_workers nworkers (fun queue -> + Proof_global.with_current_proof (fun _ p -> + let goals, _, _, _, _ = Proof.proof p in + let open TacTask in + let res = CList.map_i (fun i g -> + let f,assign= Future.create_delegate (State.exn_on id ~valid:safe_id) in + let t_ast = + { verbose;loc;expr = VernacSolve(SelectNth i,None,e,etac) } in + let t_name = Goal.uid g in + TaskQueue.enqueue_task queue + ({ t_state = safe_id; t_state_fb = id; + t_assign = assign; t_ast; t_goal = g; t_name; + t_kill = (fun () -> TaskQueue.cancel_all queue) }, cancel); + Goal.uid g,f) + 1 goals in + TaskQueue.join queue; + let assign_tac : unit Proofview.tactic = + Proofview.V82.tactic (fun gl -> + let open Tacmach in + let sigma, g = project gl, sig_it gl in + let gid = Goal.uid g in + let f = + try List.assoc gid res + with Not_found -> Errors.anomaly(str"Partac: wrong focus") in + if Future.is_over f then + let pt, uc = Future.join f in + prerr_endline (string_of_ppcmds(hov 0 ( + str"g=" ++ str gid ++ spc () ++ + str"t=" ++ (Printer.pr_constr pt) ++ spc () ++ + str"uc=" ++ Evd.pr_evar_universe_context uc))); + let sigma = Goal.V82.partial_solution sigma g pt in + let sigma = Evd.merge_universe_context sigma uc in + re_sig [] sigma + else (* One has failed and cancelled the others, but not this one *) + re_sig [g] sigma) in + Proof.run_tactic (Global.env()) assign_tac p)))) ()) + +end (* }}} *) + +and QueryTask : sig + + type task = { t_where : Stateid.t; t_for : Stateid.t ; t_what : ast } + include AsyncTaskQueue.Task with type task := task + +end = struct (* {{{ *) + + type task = + { t_where : Stateid.t; t_for : Stateid.t ; t_what : ast } + + type request = + { r_where : Stateid.t ; r_for : Stateid.t ; r_what : ast; r_doc : VCS.vcs } + type response = unit + + let name = ref "queryworker" + let extra_env _ = [||] + type competence = unit + let task_match _ _ = true + + let request_of_task _ { t_where; t_what; t_for } = + try Some { + r_where = t_where; + r_for = t_for; + r_doc = VCS.slice ~start:t_where ~stop:t_where; + r_what = t_what } + with VCS.Expired -> None + + let use_response _ _ _ = `End + + let on_marshal_error _ _ = + pr_err ("Fatal marshal error in query"); + flush_all (); exit 1 + + let on_task_cancellation_or_expiration_or_slave_death _ = () + + let forward_feedback msg = Hooks.(call forward_feedback msg) + + let perform { r_where; r_doc; r_what; r_for } = + VCS.restore r_doc; + VCS.print (); + Reach.known_state ~cache:`No r_where; + try + vernac_interp r_for { r_what with verbose = true }; + feedback ~state_id:r_for Feedback.Processed + with e when Errors.noncritical e -> + let msg = string_of_ppcmds (print e) in + feedback ~state_id:r_for (Feedback.ErrorMsg (Loc.ghost, msg)) + + let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what) + let name_of_request { r_what } = string_of_ppcmds (pr_ast r_what) + +end (* }}} *) + +and Query : sig + + val init : unit -> unit + val vernac_interp : cancel_switch -> Stateid.t -> Stateid.t -> ast -> unit + +end = struct (* {{{ *) + + module TaskQueue = AsyncTaskQueue.MakeQueue(QueryTask) + + let queue = ref None + + let vernac_interp switch prev id q = + assert(TaskQueue.n_workers (Option.get !queue) > 0); + TaskQueue.enqueue_task (Option.get !queue) + QueryTask.({ QueryTask.t_where = prev; t_for = id; t_what = q }, switch) + + let init () = queue := Some (TaskQueue.create + (if !Flags.async_proofs_full then 1 else 0)) + +end (* }}} *) + +(* Runs all transactions needed to reach a state *) +and 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 async_policy () = + let open Flags in + if interactive () = `Yes then + (async_proofs_is_master () || !async_proofs_mode = Flags.APonLazy) + else + (!compilation_mode = Flags.BuildVio || !async_proofs_mode <> Flags.APoff) + +let delegate name = + let time = get_hint_bp_time name in + time >= 1.0 || !Flags.compilation_mode = Flags.BuildVio + +let collect_proof keep 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 proof_using_ast = function + | Some (_, ({ expr = VernacProof(_,Some _) } as v)) -> Some v + | _ -> None in + let has_proof_using x = proof_using_ast x <> None in + let proof_no_using = function + | Some (_, ({ expr = VernacProof(t,None) } as v)) -> t,v + | _ -> assert false in + let has_proof_no_using = function + | Some (_, { expr = VernacProof(_,None) }) -> true + | _ -> false in + let parent = function Some (p, _) -> p | None -> assert false in + let rec collect last accn id = + let view = VCS.visit id in + match view.step with + | `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next + (* An Alias could jump everywhere... we hope we can ignore it*) + | `Alias _ -> `Sync (no_name,None,`Alias) + | `Fork((_,_,_,_::_::_), _) -> + `Sync (no_name,proof_using_ast last,`MutualProofs) + | `Fork((_,_,Doesn'tGuaranteeOpacity,_), _) -> + `Sync (no_name,proof_using_ast last,`Doesn'tGuaranteeOpacity) + | `Fork((_,hd',GuaranteesOpacity,ids), _) when has_proof_using last -> + assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch); + let name = name ids in + `ASync (parent last,proof_using_ast last,accn,name,delegate name) + | `Fork((_, hd', GuaranteesOpacity, ids), _) when + has_proof_no_using last && not (State.is_cached (parent last)) && + !Flags.compilation_mode = Flags.BuildVio -> + assert (VCS.Branch.equal hd hd'||VCS.Branch.equal hd VCS.edit_branch); + (try + let name, hint = name ids, get_hint_ctx loc in + let t, v = proof_no_using last in + v.expr <- VernacProof(t, Some hint); + `ASync (parent last,proof_using_ast last,accn,name,delegate name) + with Not_found -> `Sync (no_name,None,`NoHint)) + | `Fork((_, hd', GuaranteesOpacity, ids), _) -> + assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch); + let name = name ids in + `MaybeASync (parent last, None, accn, name, delegate name) + | `Sideff _ -> `Sync (no_name,None,`NestedProof) + | _ -> `Sync (no_name,None,`Unknown) in + let make_sync why = function + | `Sync(name,pua,_) -> `Sync (name,pua,why) + | `MaybeASync(_,pua,_,name,_) -> `Sync (name,pua,why) + | `ASync(_,pua,_,name,_) -> `Sync (name,pua,why) in + let check_policy rc = if async_policy () then rc else make_sync `Policy rc in + match cur, (VCS.visit id).step, brkind with + | (parent, { expr = VernacExactProof _ }), `Fork _, _ -> + `Sync (no_name,None,`Immediate) + | _, _, { VCS.kind = `Edit _ } -> check_policy (collect (Some cur) [] id) + | _ -> + if is_defined cur then `Sync (no_name,None,`Transparent) + else if keep == VtDrop then `Sync (no_name,None,`Aborted) + else + let rc = collect (Some cur) [] id in + if keep == VtKeep && + (not(State.is_cached id) || !Flags.async_proofs_full) + then check_policy rc + else make_sync `AlreadyEvaluated rc + +let string_of_reason = function + | `Transparent -> "Transparent" + | `AlreadyEvaluated -> "AlreadyEvaluated" + | `Policy -> "Policy" + | `NestedProof -> "NestedProof" + | `Immediate -> "Immediate" + | `Alias -> "Alias" + | `NoHint -> "NoHint" + | `Doesn'tGuaranteeOpacity -> "Doesn'tGuaranteeOpacity" + | `Aborted -> "Aborted" + | _ -> "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 ~cache id then begin + State.install_cached id; + Hooks.(call state_computed id ~in_cache:true); + prerr_endline ("reached (cache)") + end else + let step, cache_step, feedback_processed = + let view = VCS.visit id in + match view.step with + | `Alias id -> (fun () -> + reach view.next; reach id + ), cache, true + | `Cmd { cast = x; cqueue = `TacQueue cancel } -> (fun () -> + reach ~cache:`Shallow view.next; + Partac.vernac_interp + cancel !Flags.async_proofs_n_tacworkers view.next id x + ), cache, true + | `Cmd { cast = x; cqueue = `QueryQueue cancel } + when Flags.async_proofs_is_master () -> (fun () -> + reach ~cache:`Shallow view.next; + Query.vernac_interp cancel view.next id x + ), cache, false + | `Cmd { cast = x } -> (fun () -> + reach view.next; vernac_interp id x + ), cache, true + | `Fork ((x,_,_,_), None) -> (fun () -> + reach view.next; vernac_interp id x; + wall_clock_last_fork := Unix.gettimeofday () + ), `Yes, true + | `Fork ((x,_,_,_), Some prev) -> (fun () -> + reach ~cache:`Shallow prev; + reach view.next; + (try vernac_interp id x; + with e when Errors.noncritical e -> + let (e, info) = Errors.push e in + let info = Stateid.add info ~valid:prev id in + iraise (e, info)); + wall_clock_last_fork := Unix.gettimeofday () + ), `Yes, true + | `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) -> + let rec aux = function + | `ASync (start, pua, nodes, name, delegate) -> (fun () -> + assert(keep == VtKeep); + let stop, exn_info, loc = eop, (id, eop), x.loc in + prerr_endline ("Asynchronous " ^ Stateid.to_string id); + VCS.create_cluster nodes ~qed:id ~start; + begin match brinfo, qed.fproof with + | { VCS.kind = `Edit _ }, None -> assert false + | { VCS.kind = `Edit _ }, Some (ofp, cancel) -> + assert(redefine_qed = true); + let fp, cancel = + Slaves.build_proof ~loc ~exn_info ~start ~stop ~name in + Future.replace ofp fp; + qed.fproof <- Some (fp, cancel) + | { VCS.kind = `Proof _ }, Some _ -> assert false + | { VCS.kind = `Proof _ }, None -> + reach ~cache:`Shallow start; + let fp, cancel = + if delegate then + Slaves.build_proof ~loc ~exn_info ~start ~stop ~name + else + ProofTask.build_proof_here exn_info loc stop, ref false + in + qed.fproof <- Some (fp, cancel); + let proof = + Proof_global.close_future_proof ~feedback_id:id fp in + if not delegate then ignore(Future.compute fp); + reach view.next; + vernac_interp id ~proof x; + feedback ~state_id:id Feedback.Incomplete + | { VCS.kind = `Master }, _ -> assert false + end; + Proof_global.discard_all () + ), (if redefine_qed then `No else `Yes), true + | `Sync (name, _, `Immediate) -> (fun () -> + assert (Stateid.equal view.next eop); + reach eop; vernac_interp id x; Proof_global.discard_all () + ), `Yes, true + | `Sync (name, pua, 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); + let proof = + if keep != VtKeep then None + else Some(Proof_global.close_proof + ~keep_body_ucst_sepatate:false + (State.exn_on id ~valid:eop)) in + if proof = None then prerr_endline "NONE!!!!!"; + reach view.next; + if keep == VtKeepAsAxiom then + Option.iter (vernac_interp id) pua; + 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)); + Proof_global.discard_all () + ), `Yes, true + | `MaybeASync (start, pua, nodes, name, delegate) -> (fun () -> + prerr_endline ("MaybeAsynchronous " ^ Stateid.to_string id); + reach ~cache:`Shallow start; + (* no sections *) + if List.is_empty (Environ.named_context (Global.env ())) + then pi1 (aux (`ASync (start, pua, nodes, name, delegate))) () + else pi1 (aux (`Sync (name, pua, `Unknown))) () + ), (if redefine_qed then `No else `Yes), true + in + aux (collect_proof keep (view.next, x) brname brinfo eop) + | `Sideff (`Ast (x,_)) -> (fun () -> + reach view.next; vernac_interp id x; + ), cache, true + | `Sideff (`Id origin) -> (fun () -> + reach view.next; + inject_non_pstate (pure_cherry_pick_non_pstate origin); + ), cache, true + in + let cache_step = + if !Flags.async_proofs_cache = Some Flags.Force then `Yes + else cache_step in + State.define + ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id; + prerr_endline ("reached: "^ Stateid.to_string id) in + reach ~redefine_qed id + +end (* }}} *) + +(********************************* STM API ************************************) +(******************************************************************************) + +let init () = + VCS.init Stateid.initial; + set_undo_classifier Backtrack.undo_vernac_classifier; + State.define ~cache:`Yes (fun () -> ()) Stateid.initial; + Backtrack.record (); + Slaves.init (); + if Flags.async_proofs_is_master () then begin + prerr_endline "Initialising workers"; + Query.init (); + let opts = match !Flags.async_proofs_private_flags with + | None -> [] + | Some s -> Str.split_delim (Str.regexp ",") s in + 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 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; + iraise e + +let finish ?(print_goals=false) () = + observe (VCS.get_branch_pos (VCS.current_branch ())); + if print_goals then msg_notice (pr_open_cur_subgoals ()); + VCS.print () + +let wait () = + Slaves.wait_all_done (); + VCS.print () + +let join () = + finish (); + wait (); + prerr_endline "Joining the environment"; + Global.join_safe_environment (); + VCS.print (); + VCS.print () + +let dump_snapshot () = Slaves.dump_snapshot (), RemoteCounter.snapshot () +type document = VCS.vcs +type tasks = int Slaves.tasks * RemoteCounter.remote_counters_status +let check_task name (tasks,rcbackup) i = + RemoteCounter.restore rcbackup; + let vcs = VCS.backup () in + try + let rc = Future.purify (Slaves.check_task name tasks) i in + 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 + 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 + pperrnl (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e); + exit 1 + +let merge_proof_branch ?id 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 ?id () in + VCS.merge id ~ours:(Qed (qed None)) brname; + VCS.delete_branch brname; + if keep <> VtDrop 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 } -> + iraise (State.exn_on Stateid.dummy (Proof_global.NoCurrentProof, Exninfo.null)) + +(* 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, info) vcs tty = + if e = Errors.Drop then iraise (e, info) else + match Stateid.get info 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 (); + iraise (e, info) + +let snapshot_vio ldir long_f_dot_v = + finish (); + if List.length (VCS.branches ()) > 1 then + Errors.errorlabstrm "stm" (str"Cannot dump a vio with open proofs"); + Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_v + (Global.opaque_tables ()) + +let reset_task_queue = Slaves.reset_task_queue + +(* Document building *) +let process_transaction ?(newtip=Stateid.fresh ()) ~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; 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 ~id:newtip () 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,(report_id,route)), VtNow when tty = true -> + finish (); + (try Future.purify (vernac_interp report_id ~route) + { verbose = true; loc; expr } + with e when Errors.noncritical e -> + let e = Errors.push e in + iraise (State.exn_on report_id e)); `Ok + | VtQuery (false,(report_id,route)), VtNow -> + (try vernac_interp report_id ~route x + with e when Errors.noncritical e -> + let e = Errors.push e in + iraise (State.exn_on report_id e)); `Ok + | VtQuery (true,(report_id,_)), w -> + assert(Stateid.equal report_id Stateid.dummy); + let id = VCS.new_node ~id:newtip () in + let queue = + if !Flags.async_proofs_full then `QueryQueue (ref false) + else `MainQueue in + VCS.commit id (Cmd { cast = x; cids = []; cqueue = queue }); + 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 ~id:newtip () in + let bname = VCS.mk_branch_name x in + VCS.checkout VCS.Branch.master; + if VCS.Branch.equal head VCS.Branch.master then begin + VCS.commit id (Fork (x, bname, guarantee, names)); + VCS.branch bname (`Proof (mode, VCS.proof_nesting () + 1)) + end else begin + VCS.branch bname (`Proof (mode, VCS.proof_nesting () + 1)); + VCS.merge id ~ours:(Fork (x, bname, guarantee, names)) head + end; + 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 ~id:newtip () in + VCS.checkout VCS.Branch.master; + VCS.commit id (Cmd {cast = x; cids=[]; cqueue = `MainQueue}); + 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 paral, w -> + let id = VCS.new_node ~id:newtip () in + let queue = if paral then `TacQueue (ref false) else `MainQueue in + VCS.commit id (Cmd {cast = x; cids = []; cqueue = queue }); + Backtrack.record (); if w == VtNow then finish (); `Ok + | VtQed keep, w -> + let rc = merge_proof_branch ~id:newtip x keep head in + VCS.checkout_shallowest_proof_branch (); + Backtrack.record (); if w == VtNow then finish (); + rc + + (* Side effect on all branches *) + | VtUnknown, _ when expr = VernacToplevelControl Drop -> + vernac_interp (VCS.get_branch_pos head) x; `Ok + + | VtSideff l, w -> + let id = VCS.new_node ~id:newtip () in + VCS.checkout VCS.Branch.master; + VCS.commit id (Cmd { cast = x; cids = l; cqueue = `MainQueue}); + 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 ~id:newtip () in + let head_id = VCS.get_branch_pos head in + Reach.known_state ~cache:`Yes head_id; (* ensure it is ok *) + 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 { cast = x; cids = []; cqueue = `MainQueue}); + VCS.propagate_sideff (Some x); + VCS.checkout_shallowest_proof_branch (); + end in + State.define ~safe_id:head_id ~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 + +let print_ast id = + try + match VCS.visit id with + | { step = `Cmd { cast = { loc; expr } } } + | { step = `Fork (({ loc; expr }, _, _, _), _) } + | { step = `Qed ({ qast = { loc; expr } }, _) } -> + let xml = + try Texmacspp.tmpp expr loc + with e -> Xml_datatype.PCData ("ERROR " ^ Printexc.to_string e) in + xml; + | _ -> Xml_datatype.PCData "ERROR" + with _ -> Xml_datatype.PCData "ERROR" + +let stop_worker n = Slaves.cancel_worker n + +let add ~ontop ?newtip ?(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 ?newtip eid s in + check(loc_ast); + let clas = classify_vernac ast in + match process_transaction ?newtip ~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 query ~at ?(report_with=(Stateid.dummy,Feedback.default_route)) s = + Future.purify (fun s -> + if Stateid.equal at Stateid.dummy then finish () + else Reach.known_state ~cache:`Yes at; + let newtip, route = report_with in + let _, ast as loc_ast = vernac_parse ~newtip ~route 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,report_with), VtNow) loc_ast)) + s + +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 start at_id mode qed_id tip = + let master_id, cancel_switch = + (* Hum, this should be the real start_id in the clusted and not next *) + match VCS.visit qed_id with + | { step = `Qed ({ fproof = Some (_,cs)},_) } -> start, cs + | _ -> anomaly (str "Cluster not ending with Qed") in + VCS.branch ~root:master_id ~pos:id + VCS.edit_branch (`Edit (mode, qed_id, master_id)); + VCS.delete_cluster_of id; + cancel_switch := true; + 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,start), Some mode -> + let tip = VCS.cur_tip () in + if has_failed qed_id && not !Flags.async_proofs_never_reopen_branch + then reopen_branch start 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, info) = Errors.push e in + match Stateid.get info with + | None -> + VCS.print (); + anomaly (str ("edit_at "^Stateid.to_string id^": ") ++ + Errors.print_no_report e) + | Some (_, id) -> + prerr_endline ("Failed at state " ^ Stateid.to_string id); + VCS.restore vcs; + VCS.print (); + iraise (e, info) + +(*********************** TTY API (PG, coqtop, coqc) ***************************) +(******************************************************************************) + +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 + let print_goals = + verb && match clas with + | VtQuery _, _ -> false + | (VtProofStep _ | VtStm (VtBack _, _)), _ -> true + | _ -> not !Flags.coqtop_ui || !Flags.print_emacs in + try finish ~print_goals () + with e -> + let e = Errors.push e in + handle_failure e vcs true + +let finish () = finish () + +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 {cast = 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 (prlist_with_sep fnl (fun x -> x) indented_cmds)) + with Vcs_aux.Expired -> () + +(* Export hooks *) +let state_computed_hook = Hooks.state_computed_hook +let state_ready_hook = Hooks.state_ready_hook +let parse_error_hook = Hooks.parse_error_hook +let execution_error_hook = Hooks.execution_error_hook +let forward_feedback_hook = Hooks.forward_feedback_hook +let process_error_hook = Hooks.process_error_hook +let interp_hook = Hooks.interp_hook +let with_fail_hook = Hooks.with_fail_hook +let unreachable_state_hook = Hooks.unreachable_state_hook + +(* vim:set foldmethod=marker: *) diff --git a/stm/stm.mli b/stm/stm.mli new file mode 100644 index 00000000..1d926e99 --- /dev/null +++ b/stm/stm.mli @@ -0,0 +1,132 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* ?newtip:Stateid.t -> ?check:(located_vernac_expr -> unit) -> + bool -> edit_id -> string -> + Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] + +(* parses and executes a command at a given state, throws away its side effects + but for the printings. Feedback is sent with report_with (defaults to dummy + state id) *) +val query : + at:Stateid.t -> ?report_with:(Stateid.t * Feedback.route_id) -> 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 observe : Stateid.t -> unit + +val stop_worker : string -> unit + +(* Joins the entire document. Implies finish, but also checks proofs *) +val join : unit -> unit + +(* Saves on the dist a .vio corresponding to the current status: + - if the worker prool is empty, all tasks are saved + - if the worker proof is not empty, then it waits until all workers + are done with their current jobs and then dumps (or fails if one + of the completed tasks is a failuere) *) +val snapshot_vio : DirPath.t -> string -> unit + +(* Empties the task queue, can be used only if the worker pool is empty (E.g. + * after having built a .vio in batch mode *) +val reset_task_queue : unit -> unit + +(* A .vio contains tasks to be completed *) +type 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 print_ast : Stateid.t -> Xml_datatype.xml + +(* 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 + +(** workers **************************************************************** **) + +module ProofTask : AsyncTaskQueue.Task +module TacTask : AsyncTaskQueue.Task +module QueryTask : AsyncTaskQueue.Task + +(** customization ********************************************************** **) + +(* From the master (or worker, but beware that to install the hook + * into a worker one has to build the worker toploop to do so and + * the alternative toploop for the worker can be selected by changing + * the name of the Task(s) above) *) + +val state_computed_hook : (Stateid.t -> in_cache:bool -> unit) Hook.t +val parse_error_hook : + (Feedback.edit_or_state_id -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t +val execution_error_hook : (Stateid.t -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t +val unreachable_state_hook : (Stateid.t -> unit) Hook.t +(* ready means that master has it at hand *) +val state_ready_hook : (Stateid.t -> unit) Hook.t + +(* Messages from the workers to the master *) +val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t + +type state = { + system : States.state; + proof : Proof_global.state; + shallow : bool +} +val state_of_id : Stateid.t -> [ `Valid of state option | `Expired ] + +(** 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 : Future.fix_exn Hook.t +val interp_hook : (?verbosely:bool -> ?proof:Proof_global.closed_proof -> + Loc.t * Vernacexpr.vernac_expr -> unit) Hook.t +val with_fail_hook : (bool -> (unit -> unit) -> unit) Hook.t diff --git a/stm/stm.mllib b/stm/stm.mllib new file mode 100644 index 00000000..92b3a869 --- /dev/null +++ b/stm/stm.mllib @@ -0,0 +1,12 @@ +Spawned +Dag +Vcs +TQueue +WorkerPool +Vernac_classifier +Lemmas +CoqworkmgrApi +AsyncTaskQueue +Texmacspp +Stm +Vio_checking diff --git a/stm/tQueue.ml b/stm/tQueue.ml new file mode 100644 index 00000000..8a62fe79 --- /dev/null +++ b/stm/tQueue.ml @@ -0,0 +1,133 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'a t + val set_rel : ('a -> 'a -> int) -> 'a t -> unit + val is_empty : 'a t -> bool + val exists : ('a -> bool) -> 'a t -> bool + val pop : ?picky:('a -> bool) -> 'a t -> 'a + val push : 'a t -> 'a -> unit + val clear : 'a t -> unit +end = struct + type 'a item = int * 'a + type 'a rel = 'a item -> 'a item -> int + type 'a t = ('a item list * 'a rel) ref + let sort_timestamp (i,_) (j,_) = i - j + let age = ref 0 + let create () = ref ([],sort_timestamp) + let is_empty t = fst !t = [] + let exists p t = List.exists (fun (_,x) -> p x) (fst !t) + let pop ?(picky=(fun _ -> true)) ({ contents = (l, rel) } as t) = + let rec aux acc = function + | [] -> raise Queue.Empty + | (_,x) :: xs when picky x -> t := (List.rev acc @ xs, rel); x + | (_,x) as hd :: xs -> aux (hd :: acc) xs in + aux [] l + let push ({ contents = (xs, rel) } as t) x = + incr age; + (* re-roting the whole list is not the most efficient way... *) + t := (List.sort rel (xs @ [!age,x]), rel) + let clear ({ contents = (l, rel) } as t) = t := ([], rel) + let set_rel rel ({ contents = (xs, _) } as t) = + let rel (_,x) (_,y) = rel x y in + t := (List.sort rel xs, rel) +end + +type 'a t = { + queue: 'a PriorityQueue.t; + lock : Mutex.t; + cond : Condition.t; + mutable nwaiting : int; + cond_waiting : Condition.t; + mutable release : bool; +} + +exception BeingDestroyed + +let create () = { + queue = PriorityQueue.create (); + lock = Mutex.create (); + cond = Condition.create (); + nwaiting = 0; + cond_waiting = Condition.create (); + release = false; +} + +let pop ?(picky=(fun _ -> true)) ?(destroy=ref false) + ({ queue = q; lock = m; cond = c; cond_waiting = cn } as tq) += + Mutex.lock m; + if tq.release then (Mutex.unlock m; raise BeingDestroyed); + while not (PriorityQueue.exists picky q || !destroy) do + tq.nwaiting <- tq.nwaiting + 1; + Condition.broadcast cn; + Condition.wait c m; + tq.nwaiting <- tq.nwaiting - 1; + if tq.release || !destroy then (Mutex.unlock m; raise BeingDestroyed) + done; + if !destroy then (Mutex.unlock m; raise BeingDestroyed); + let x = PriorityQueue.pop ~picky q in + Condition.signal c; + Condition.signal cn; + Mutex.unlock m; + x + +let signal_destruction { lock = m; cond = c } = + Mutex.lock m; + Condition.broadcast c; + Mutex.unlock m + +let push { queue = q; lock = m; cond = c; release } x = + if release then Errors.anomaly(Pp.str + "TQueue.push while being destroyed! Only 1 producer/destroyer allowed"); + Mutex.lock m; + PriorityQueue.push q x; + Condition.broadcast c; + Mutex.unlock m + +let clear { queue = q; lock = m; cond = c } = + Mutex.lock m; + PriorityQueue.clear q; + Mutex.unlock m + +let is_empty { queue = q } = PriorityQueue.is_empty q + +let destroy tq = + tq.release <- true; + while tq.nwaiting > 0 do + Mutex.lock tq.lock; + Condition.broadcast tq.cond; + Mutex.unlock tq.lock; + done; + tq.release <- false + +let wait_until_n_are_waiting_and_queue_empty j tq = + Mutex.lock tq.lock; + while not (PriorityQueue.is_empty tq.queue) || tq.nwaiting < j do + Condition.wait tq.cond_waiting tq.lock + done; + Mutex.unlock tq.lock + +let wait_until_n_are_waiting_then_snapshot j tq = + let l = ref [] in + Mutex.lock tq.lock; + while not (PriorityQueue.is_empty tq.queue) do + l := PriorityQueue.pop tq.queue :: !l + done; + while tq.nwaiting < j do Condition.wait tq.cond_waiting tq.lock done; + List.iter (PriorityQueue.push tq.queue) (List.rev !l); + if !l <> [] then Condition.broadcast tq.cond; + Mutex.unlock tq.lock; + List.rev !l + +let set_order tq rel = + Mutex.lock tq.lock; + PriorityQueue.set_rel rel tq.queue; + Mutex.unlock tq.lock diff --git a/stm/tQueue.mli b/stm/tQueue.mli new file mode 100644 index 00000000..bc3922b3 --- /dev/null +++ b/stm/tQueue.mli @@ -0,0 +1,28 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'a t +val pop : ?picky:('a -> bool) -> ?destroy:bool ref -> 'a t -> 'a +val push : 'a t -> 'a -> unit +val set_order : 'a t -> ('a -> 'a -> int) -> unit +val wait_until_n_are_waiting_and_queue_empty : int -> 'a t -> unit +val signal_destruction : 'a t -> unit + +(* Non destructive *) +val wait_until_n_are_waiting_then_snapshot : int -> 'a t -> 'a list + +val clear : 'a t -> unit +val is_empty : 'a t -> bool + +exception BeingDestroyed +(* Threads blocked in pop can get this exception if the queue is being + * destroyed *) +val destroy : 'a t -> unit diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml new file mode 100644 index 00000000..c1a37fed --- /dev/null +++ b/stm/tacworkertop.ml @@ -0,0 +1,18 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + Flags.make_silent true; + W.init_stdout (); + CoqworkmgrApi.init !Flags.async_proofs_worker_priority; + args) + +let () = Coqtop.toploop_run := W.main_loop + diff --git a/stm/tacworkertop.mllib b/stm/tacworkertop.mllib new file mode 100644 index 00000000..db38fde2 --- /dev/null +++ b/stm/tacworkertop.mllib @@ -0,0 +1 @@ +Tacworkertop diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml new file mode 100644 index 00000000..d71c169d --- /dev/null +++ b/stm/texmacspp.ml @@ -0,0 +1,763 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (List.filter (fun (a,_) -> a = attr) attrs) + | _ -> []) + xml_list in + match List.flatten attrs_list with + | [] -> (attr, "") + | l -> (List.hd l) + +let backstep_loc xmllist = + let start_att = get_fst_attr_in_xml_list "begin" xmllist in + let stop_att = get_fst_attr_in_xml_list "end" (List.rev xmllist) in + [start_att ; stop_att] + +let compare_begin_att xml1 xml2 = + let att1 = get_fst_attr_in_xml_list "begin" [xml1] in + let att2 = get_fst_attr_in_xml_list "begin" [xml2] in + match att1, att2 with + | (_, s1), (_, s2) when s1 == "" || s2 == "" -> 0 + | (_, s1), (_, s2) when int_of_string s1 > int_of_string s2 -> 1 + | (_, s1), (_, s2) when int_of_string s1 < int_of_string s2 -> -1 + | _ -> 0 + +let xmlBeginSection loc name = xmlWithLoc loc "beginsection" ["name", name] [] + +let xmlEndSegment loc name = xmlWithLoc loc "endsegment" ["name", name] [] + +let xmlThm typ name loc xml = + xmlWithLoc loc "theorem" ["type", typ; "name", name] xml + +let xmlDef typ name loc xml = + xmlWithLoc loc "definition" ["type", typ; "name", name] xml + +let xmlNotation attr name loc xml = + xmlWithLoc loc "notation" (("name", name) :: attr) xml + +let xmlReservedNotation attr name loc = + xmlWithLoc loc "reservednotation" (("name", name) :: attr) [] + +let xmlCst name ?(attr=[]) loc = + xmlWithLoc loc "constant" (("name", name) :: attr) [] + +let xmlOperator name ?(attr=[]) ?(pprules=[]) loc = + xmlWithLoc loc "operator" + (("name", name) :: List.map (fun (a,b) -> "format"^a,b) pprules @ attr) [] + +let xmlApply loc ?(attr=[]) xml = xmlWithLoc loc "apply" attr xml + +let xmlToken loc ?(attr=[]) xml = xmlWithLoc loc "token" attr xml + +let xmlTyped xml = Element("typed", (backstep_loc xml), xml) + +let xmlReturn ?(attr=[]) xml = Element("return", attr, xml) + +let xmlCase xml = Element("case", [], xml) + +let xmlScrutinee ?(attr=[]) xml = Element("scrutinee", attr, xml) + +let xmlWith xml = Element("with", [], xml) + +let xmlAssign id xml = Element("assign", ["target",string_of_id id], [xml]) + +let xmlInductive kind loc xml = xmlWithLoc loc "inductive" ["kind",kind] xml + +let xmlCoFixpoint xml = Element("cofixpoint", [], xml) + +let xmlFixpoint xml = Element("fixpoint", [], xml) + +let xmlCheck loc xml = xmlWithLoc loc "check" [] xml + +let xmlAssumption kind loc xml = xmlWithLoc loc "assumption" ["kind",kind] xml + +let xmlComment loc xml = xmlWithLoc loc "comment" [] xml + +let xmlCanonicalStructure attr loc = xmlWithLoc loc "canonicalstructure" attr [] + +let xmlQed ?(attr=[]) loc = xmlWithLoc loc "qed" attr [] + +let xmlPatvar id loc = xmlWithLoc loc "patvar" ["id", id] [] + +let xmlReference ref = + let name = Libnames.string_of_reference ref in + let i, j = Loc.unloc (Libnames.loc_of_reference ref) in + let b, e = string_of_int i, string_of_int j in + Element("reference",["name", name; "begin", b; "end", e] ,[]) + +let xmlRequire loc ?(attr=[]) xml = xmlWithLoc loc "require" attr xml +let xmlImport loc ?(attr=[]) xml = xmlWithLoc loc "import" attr xml + +let xmlAddLoaPath loc ?(attr=[]) xml = xmlWithLoc loc "addloadpath" attr xml +let xmlRemoveLoaPath loc ?(attr=[]) = xmlWithLoc loc "removeloadpath" attr +let xmlAddMLPath loc ?(attr=[]) = xmlWithLoc loc "addmlpath" attr + +let xmlExtend loc xml = xmlWithLoc loc "extend" [] xml + +let xmlScope loc action ?(attr=[]) name xml = + xmlWithLoc loc "scope" (["name",name;"action",action] @ attr) xml + +let xmlProofMode loc name = xmlWithLoc loc "proofmode" ["name",name] [] + +let xmlProof loc xml = xmlWithLoc loc "proof" [] xml + +let xmlRawTactic name rtac = + Element("rawtactic", ["name",name], + [PCData (Pp.string_of_ppcmds (Pptactic.pr_raw_tactic rtac))]) + +let xmlSectionSubsetDescr name ssd = + Element("sectionsubsetdescr",["name",name], + [PCData (Proof_using.to_string ssd)]) + +let xmlDeclareMLModule loc s = + xmlWithLoc loc "declarexmlmodule" [] + (List.map (fun x -> Element("path",["value",x],[])) s) + +(* tactics *) +let xmlLtac loc xml = xmlWithLoc loc "ltac" [] xml + +(* toplevel commands *) +let xmlGallina loc xml = xmlWithLoc loc "gallina" [] xml + +let xmlTODO loc x = + xmlWithLoc loc "todo" [] [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))] + +let string_of_name n = + match n with + | Anonymous -> "_" + | Name id -> Id.to_string id + +let string_of_glob_sort s = + match s with + | GProp -> "Prop" + | GSet -> "Set" + | GType _ -> "Type" + +let string_of_cast_sort c = + match c with + | CastConv _ -> "CastConv" + | CastVM _ -> "CastVM" + | CastNative _ -> "CastNative" + | CastCoerce -> "CastCoerce" + +let string_of_case_style s = + match s with + | LetStyle -> "Let" + | IfStyle -> "If" + | LetPatternStyle -> "LetPattern" + | MatchStyle -> "Match" + | RegularStyle -> "Regular" + +let attribute_of_syntax_modifier sm = +match sm with + | SetItemLevel (sl, NumLevel n) -> + List.map (fun s -> ("itemlevel", s)) sl @ ["level", string_of_int n] + | SetItemLevel (sl, NextLevel) -> + List.map (fun s -> ("itemlevel", s)) sl @ ["level", "next"] + | SetLevel i -> ["level", string_of_int i] + | SetAssoc a -> + begin match a with + | NonA -> ["",""] + | RightA -> ["associativity", "right"] + | LeftA -> ["associativity", "left"] + end + | SetEntryType (s, _) -> ["entrytype", s] + | SetOnlyParsing v -> ["compat", Flags.pr_version v] + | SetFormat (system, (loc, s)) -> + let start, stop = unlock loc in + ["format-"^system, s; "begin", start; "end", stop] + +let string_of_assumption_kind l a many = + match l, a, many with + | (Discharge, Logical, true) -> "Hypotheses" + | (Discharge, Logical, false) -> "Hypothesis" + | (Discharge, Definitional, true) -> "Variables" + | (Discharge, Definitional, false) -> "Variable" + | (Global, Logical, true) -> "Axioms" + | (Global, Logical, false) -> "Axiom" + | (Global, Definitional, true) -> "Parameters" + | (Global, Definitional, false) -> "Parameter" + | (Local, Logical, true) -> "Local Axioms" + | (Local, Logical, false) -> "Local Axiom" + | (Local, Definitional, true) -> "Local Parameters" + | (Local, Definitional, false) -> "Local Parameter" + | (Global, Conjectural, _) -> "Conjecture" + | ((Discharge | Local), Conjectural, _) -> assert false + +let rec pp_bindlist bl = + let tlist = + List.flatten + (List.map + (fun (loc_names, _, e) -> + let names = + (List.map + (fun (loc, name) -> + xmlCst (string_of_name name) loc) loc_names) in + match e with + | CHole _ -> names + | _ -> names @ [pp_expr e]) + bl) in + match tlist with + | [e] -> e + | l -> xmlTyped l +and pp_decl_notation ((_, s), ce, sc) = (* don't know what it is for now *) + Element ("decl_notation", ["name", s], [pp_expr ce]) +and pp_local_binder lb = (* don't know what it is for now *) + match lb with + | LocalRawDef ((_, nam), ce) -> + let attrs = ["name", string_of_name nam] in + pp_expr ~attr:attrs ce + | LocalRawAssum (namll, _, ce) -> + let ppl = + List.map (fun (loc, nam) -> (xmlCst (string_of_name nam) loc)) namll in + xmlTyped (ppl @ [pp_expr ce]) +and pp_local_decl_expr lde = (* don't know what it is for now *) + match lde with + | AssumExpr (_, ce) -> pp_expr ce + | DefExpr (_, ce, _) -> pp_expr ce +and pp_inductive_expr ((_, (l, id)), lbl, ceo, _, cl_or_rdexpr) = + (* inductive_expr *) + let b,e = Loc.unloc l in + let location = ["begin", string_of_int b; "end", string_of_int e] in + [Element ("lident", ["name", Id.to_string id] @ location, [])] @ (* inductive name *) + begin match cl_or_rdexpr with + | Constructors coel -> List.map (fun (_, (_, ce)) -> pp_expr ce) coel + | RecordDecl (_, ldewwwl) -> + List.map (fun (((_, x), _), _) -> pp_local_decl_expr x) ldewwwl + end @ + begin match ceo with (* don't know what it is for now *) + | Some ce -> [pp_expr ce] + | None -> [] + end @ + (List.map pp_local_binder lbl) +and pp_recursion_order_expr optid roe = (* don't know what it is for now *) + let attrs = + match optid with + | None -> [] + | Some (loc, id) -> + let start, stop = unlock loc in + ["begin", start; "end", stop ; "name", Id.to_string id] in + let kind, expr = + match roe with + | CStructRec -> "struct", [] + | CWfRec e -> "rec", [pp_expr e] + | CMeasureRec (e, None) -> "mesrec", [pp_expr e] + | CMeasureRec (e, Some rel) -> "mesrec", [pp_expr e] @ [pp_expr rel] in + Element ("recursion_order", ["kind", kind] @ attrs, expr) +and pp_fixpoint_expr ((loc, id), (optid, roe), lbl, ce, ceo) = + (* fixpoint_expr *) + let start, stop = unlock loc in + let id = Id.to_string id in + [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @ + (* fixpoint name *) + [pp_recursion_order_expr optid roe] @ + (List.map pp_local_binder lbl) @ + [pp_expr ce] @ + begin match ceo with (* don't know what it is for now *) + | Some ce -> [pp_expr ce] + | None -> [] + end +and pp_cofixpoint_expr ((loc, id), lbl, ce, ceo) = (* cofixpoint_expr *) + (* Nota: it is like fixpoint_expr without (optid, roe) + * so could be merged if there is no more differences *) + let start, stop = unlock loc in + let id = Id.to_string id in + [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @ + (* cofixpoint name *) + (List.map pp_local_binder lbl) @ + [pp_expr ce] @ + begin match ceo with (* don't know what it is for now *) + | Some ce -> [pp_expr ce] + | None -> [] + end +and pp_lident (loc, id) = xmlCst (Id.to_string id) loc +and pp_simple_binder (idl, ce) = List.map pp_lident idl @ [pp_expr ce] +and pp_cases_pattern_expr cpe = + match cpe with + | CPatAlias (loc, cpe, id) -> + xmlApply loc + (xmlOperator "alias" ~attr:["name", string_of_id id] loc :: + [pp_cases_pattern_expr cpe]) + | CPatCstr (loc, ref, cpel1, cpel2) -> + xmlApply loc + (xmlOperator "reference" + ~attr:["name", Libnames.string_of_reference ref] loc :: + [Element ("impargs", [], (List.map pp_cases_pattern_expr cpel1)); + Element ("args", [], (List.map pp_cases_pattern_expr cpel2))]) + | CPatAtom (loc, optr) -> + let attrs = match optr with + | None -> [] + | Some r -> ["name", Libnames.string_of_reference r] in + xmlApply loc (xmlOperator "atom" ~attr:attrs loc :: []) + | CPatOr (loc, cpel) -> + xmlApply loc (xmlOperator "or" loc :: List.map pp_cases_pattern_expr cpel) + | CPatNotation (loc, n, (subst_constr, subst_rec), cpel) -> + xmlApply loc + (xmlOperator "notation" loc :: + [xmlOperator n loc; + Element ("subst", [], + [Element ("subterms", [], + List.map pp_cases_pattern_expr subst_constr); + Element ("recsubterms", [], + List.map + (fun (cpel) -> + Element ("recsubterm", [], + List.map pp_cases_pattern_expr cpel)) + subst_rec)]); + Element ("args", [], (List.map pp_cases_pattern_expr cpel))]) + | CPatPrim (loc, tok) -> pp_token loc tok + | CPatRecord (loc, rcl) -> + xmlApply loc + (xmlOperator "record" loc :: + List.map (fun (r, cpe) -> + Element ("field", + ["reference", Libnames.string_of_reference r], + [pp_cases_pattern_expr cpe])) + rcl) + | CPatDelimiters (loc, delim, cpe) -> + xmlApply loc + (xmlOperator "delimiter" ~attr:["name", delim] loc :: + [pp_cases_pattern_expr cpe]) +and pp_case_expr (e, (name, pat)) = + match name, pat with + | None, None -> xmlScrutinee [pp_expr e] + | Some (loc, name), None -> + let start, stop= unlock loc in + xmlScrutinee ~attr:["name", string_of_name name; + "begin", start; "end", stop] [pp_expr e] + | Some (loc, name), Some p -> + let start, stop= unlock loc in + xmlScrutinee ~attr:["name", string_of_name name; + "begin", start; "end", stop] + [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e] + | None, Some p -> + xmlScrutinee [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e] +and pp_branch_expr_list bel = + xmlWith + (List.map + (fun (_, cpel, e) -> + let ppcepl = + List.map pp_cases_pattern_expr (List.flatten (List.map snd cpel)) in + let ppe = [pp_expr e] in + xmlCase (ppcepl @ ppe)) + bel) +and pp_token loc tok = + let tokstr = + match tok with + | String s -> PCData s + | Numeral n -> PCData (to_string n) in + xmlToken loc [tokstr] +and pp_local_binder_list lbl = + let l = (List.map pp_local_binder lbl) in + Element ("recurse", (backstep_loc l), l) +and pp_const_expr_list cel = + let l = List.map pp_expr cel in + Element ("recurse", (backstep_loc l), l) +and pp_expr ?(attr=[]) e = + match e with + | CRef (r, _) -> + xmlCst ~attr + (Libnames.string_of_reference r) (Libnames.loc_of_reference r) + | CProdN (loc, bl, e) -> + xmlApply loc + (xmlOperator "forall" loc :: [pp_bindlist bl] @ [pp_expr e]) + | CApp (loc, (_, hd), args) -> + xmlApply ~attr loc (pp_expr hd :: List.map (fun (e,_) -> pp_expr e) args) + | CAppExpl (loc, (_, r, _), args) -> + xmlApply ~attr loc + (xmlCst (Libnames.string_of_reference r) + (Libnames.loc_of_reference r) :: List.map pp_expr args) + | CNotation (loc, notation, ([],[],[])) -> + xmlOperator notation loc + | CNotation (loc, notation, (args, cell, lbll)) -> + let fmts = Notation.find_notation_extra_printing_rules notation in + let oper = xmlOperator notation loc ~pprules:fmts in + let cels = List.map pp_const_expr_list cell in + let lbls = List.map pp_local_binder_list lbll in + let args = List.map pp_expr args in + xmlApply loc (oper :: (List.sort compare_begin_att (args @ cels @ lbls))) + | CSort(loc, s) -> + xmlOperator (string_of_glob_sort s) loc + | CDelimiters (loc, scope, ce) -> + xmlApply loc (xmlOperator "delimiter" ~attr:["name", scope] loc :: + [pp_expr ce]) + | CPrim (loc, tok) -> pp_token loc tok + | CGeneralization (loc, kind, _, e) -> + let kind= match kind with + | Explicit -> "explicit" + | Implicit -> "implicit" in + xmlApply loc + (xmlOperator "generalization" ~attr:["kind", kind] loc :: [pp_expr e]) + | CCast (loc, e, tc) -> + begin match tc with + | CastConv t | CastVM t |CastNative t -> + xmlApply loc + (xmlOperator ":" loc ~attr:["kind", (string_of_cast_sort tc)] :: + [pp_expr e; pp_expr t]) + | CastCoerce -> + xmlApply loc + (xmlOperator ":" loc ~attr:["kind", "CastCoerce"] :: + [pp_expr e]) + end + | CEvar (loc, ek, cel) -> + let ppcel = List.map (fun (id,e) -> xmlAssign id (pp_expr e)) cel in + xmlApply loc + (xmlOperator "evar" loc ~attr:["id", string_of_id ek] :: + ppcel) + | CPatVar (loc, id) -> xmlPatvar (string_of_id id) loc + | CHole (loc, _, _, _) -> xmlCst ~attr "_" loc + | CIf (loc, test, (_, ret), th, el) -> + let return = match ret with + | None -> [] + | Some r -> [xmlReturn [pp_expr r]] in + xmlApply loc + (xmlOperator "if" loc :: + return @ [pp_expr th] @ [pp_expr el]) + | CLetTuple (loc, names, (_, ret), value, body) -> + let return = match ret with + | None -> [] + | Some r -> [xmlReturn [pp_expr r]] in + xmlApply loc + (xmlOperator "lettuple" loc :: + return @ + (List.map (fun (loc, var) -> xmlCst (string_of_name var) loc) names) @ + [pp_expr value; pp_expr body]) + | CCases (loc, sty, ret, cel, bel) -> + let return = match ret with + | None -> [] + | Some r -> [xmlReturn [pp_expr r]] in + xmlApply loc + (xmlOperator "match" loc ~attr:["style", (string_of_case_style sty)] :: + (return @ + [Element ("scrutinees", [], List.map pp_case_expr cel)] @ + [pp_branch_expr_list bel])) + | CRecord (_, _, _) -> assert false + | CLetIn (loc, (varloc, var), value, body) -> + xmlApply loc + (xmlOperator "let" loc :: + [xmlCst (string_of_name var) varloc; pp_expr value; pp_expr body]) + | CLambdaN (loc, bl, e) -> + xmlApply loc + (xmlOperator "lambda" loc :: [pp_bindlist bl] @ [pp_expr e]) + | CCoFix (_, _, _) -> assert false + | CFix (loc, lid, fel) -> + xmlApply loc + (xmlOperator "fix" loc :: + List.flatten (List.map + (fun (a,b,cl,c,d) -> pp_fixpoint_expr (a,b,cl,c,Some d)) + fel)) + +let pp_comment (c) = + match c with + | CommentConstr e -> [pp_expr e] + | CommentString s -> [Element ("string", [], [PCData s])] + | CommentInt i -> [PCData (string_of_int i)] + +let rec tmpp v loc = + match v with + (* Control *) + | VernacLoad (verbose,f) -> + xmlWithLoc loc "load" ["verbose",string_of_bool verbose;"file",f] [] + | VernacTime l -> + xmlApply loc (Element("time",[],[]) :: + List.map (fun(loc,e) ->tmpp e loc) l) + | VernacTimeout (s,e) -> + xmlApply loc (Element("timeout",["val",string_of_int s],[]) :: + [tmpp e loc]) + | VernacFail e -> xmlApply loc (Element("fail",[],[]) :: [tmpp e loc]) + | VernacError _ -> xmlWithLoc loc "error" [] [] + + (* Syntax *) + | VernacTacticNotation _ as x -> + xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))] + + | VernacSyntaxExtension (_, ((_, name), sml)) -> + let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in + xmlReservedNotation attrs name loc + + | VernacOpenCloseScope (_,(true,name)) -> xmlScope loc "open" name [] + | VernacOpenCloseScope (_,(false,name)) -> xmlScope loc "close" name [] + | VernacDelimiters (name,tag) -> + xmlScope loc "delimit" name ~attr:["delimiter",tag] [] + | VernacBindScope (name,l) -> + xmlScope loc "bind" name + (List.map (function + | ByNotation(loc,name,None) -> xmlNotation [] name loc [] + | ByNotation(loc,name,Some d) -> + xmlNotation ["delimiter",d] name loc [] + | AN ref -> xmlReference ref) l) + | VernacInfix (_,((_,name),sml),ce,sn) -> + let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in + let sc_attr = + match sn with + | Some scope -> ["scope", scope] + | None -> [] in + xmlNotation (sc_attr @ attrs) name loc [pp_expr ce] + | VernacNotation (_, ce, (lstr, sml), sn) -> + let name = snd lstr in + let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in + let sc_attr = + match sn with + | Some scope -> ["scope", scope] + | None -> [] in + xmlNotation (sc_attr @ attrs) name loc [pp_expr ce] + | VernacNotationAddFormat _ as x -> xmlTODO loc x + | VernacUniverse _ + | VernacConstraint _ + | VernacPolymorphic (_, _) as x -> xmlTODO loc x + (* Gallina *) + | VernacDefinition (ldk, (_,id), de) -> + let l, dk = + match ldk with + | Some l, dk -> (l, dk) + | None, dk -> (Global, dk) in (* Like in ppvernac.ml, l 585 *) + let e = + match de with + | ProveBody (_, ce) -> ce + | DefineBody (_, Some _, ce, None) -> ce + | DefineBody (_, None , ce, None) -> ce + | DefineBody (_, Some _, ce, Some _) -> ce + | DefineBody (_, None , ce, Some _) -> ce in + let str_dk = Kindops.string_of_definition_kind (l, false, dk) in + let str_id = Id.to_string id in + (xmlDef str_dk str_id loc [pp_expr e]) + | VernacStartTheoremProof (tk, [ Some (_,id), ([], statement, None) ], b) -> + let str_tk = Kindops.string_of_theorem_kind tk in + let str_id = Id.to_string id in + (xmlThm str_tk str_id loc [pp_expr statement]) + | VernacStartTheoremProof _ as x -> xmlTODO loc x + | VernacEndProof pe -> + begin + match pe with + | Admitted -> xmlQed loc + | Proved (_, Some ((_, id), Some tk)) -> + let nam = Id.to_string id in + let typ = Kindops.string_of_theorem_kind tk in + xmlQed ~attr:["name", nam; "type", typ] loc + | Proved (_, Some ((_, id), None)) -> + let nam = Id.to_string id in + xmlQed ~attr:["name", nam] loc + | Proved _ -> xmlQed loc + end + | VernacExactProof _ as x -> xmlTODO loc x + | VernacAssumption ((l, a), _, sbwcl) -> + let many = + List.length (List.flatten (List.map fst (List.map snd sbwcl))) > 1 in + let exprs = + List.flatten (List.map pp_simple_binder (List.map snd sbwcl)) in + let l = match l with Some x -> x | None -> Decl_kinds.Global in + let kind = string_of_assumption_kind l a many in + xmlAssumption kind loc exprs + | VernacInductive (_, _, iednll) -> + let kind = + let (_, _, _, k, _),_ = List.hd iednll in + begin + match k with + | Record -> "Record" + | Structure -> "Structure" + | Inductive_kw -> "Inductive" + | CoInductive -> "CoInductive" + | Class _ -> "Class" + | Variant -> "Variant" + end in + let exprs = + List.flatten (* should probably not be flattened *) + (List.map + (fun (ie, dnl) -> (pp_inductive_expr ie) @ + (List.map pp_decl_notation dnl)) iednll) in + xmlInductive kind loc exprs + | VernacFixpoint (_, fednll) -> + let exprs = + List.flatten (* should probably not be flattened *) + (List.map + (fun (fe, dnl) -> (pp_fixpoint_expr fe) @ + (List.map pp_decl_notation dnl)) fednll) in + xmlFixpoint exprs + | VernacCoFixpoint (_, cfednll) -> + (* Nota: it is like VernacFixpoint without so could be merged *) + let exprs = + List.flatten (* should probably not be flattened *) + (List.map + (fun (cfe, dnl) -> (pp_cofixpoint_expr cfe) @ + (List.map pp_decl_notation dnl)) cfednll) in + xmlCoFixpoint exprs + | VernacScheme _ as x -> xmlTODO loc x + | VernacCombinedScheme _ as x -> xmlTODO loc x + + (* Gallina extensions *) + | VernacBeginSection (_, id) -> xmlBeginSection loc (Id.to_string id) + | VernacEndSegment (_, id) -> xmlEndSegment loc (Id.to_string id) + | VernacNameSectionHypSet _ as x -> xmlTODO loc x + | VernacRequire (None,l) -> + xmlRequire loc (List.map (fun ref -> + xmlReference ref) l) + | VernacRequire (Some true,l) -> + xmlRequire loc ~attr:["export","true"] (List.map (fun ref -> + xmlReference ref) l) + | VernacRequire (Some false,l) -> + xmlRequire loc ~attr:["import","true"] (List.map (fun ref -> + xmlReference ref) l) + | VernacImport (true,l) -> + xmlImport loc ~attr:["export","true"] (List.map (fun ref -> + xmlReference ref) l) + | VernacImport (false,l) -> + xmlImport loc (List.map (fun ref -> + xmlReference ref) l) + | VernacCanonical r -> + let attr = + match r with + | AN (Qualid (_, q)) -> ["qualid", string_of_qualid q] + | AN (Ident (_, id)) -> ["id", Id.to_string id] + | ByNotation (_, s, _) -> ["notation", s] in + xmlCanonicalStructure attr loc + | VernacCoercion _ as x -> xmlTODO loc x + | VernacIdentityCoercion _ as x -> xmlTODO loc x + + (* Type classes *) + | VernacInstance _ as x -> xmlTODO loc x + + | VernacContext _ as x -> xmlTODO loc x + + | VernacDeclareInstances _ as x -> xmlTODO loc x + + | VernacDeclareClass _ as x -> xmlTODO loc x + + (* Modules and Module Types *) + | VernacDeclareModule _ as x -> xmlTODO loc x + | VernacDefineModule _ as x -> xmlTODO loc x + | VernacDeclareModuleType _ as x -> xmlTODO loc x + | VernacInclude _ as x -> xmlTODO loc x + + (* Solving *) + + | (VernacSolve _ | VernacSolveExistential _) as x -> + xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))] + + (* Auxiliary file and library management *) + | VernacAddLoadPath (recf,name,None) -> + xmlAddLoaPath loc ~attr:["rec",string_of_bool recf;"path",name] [] + | VernacAddLoadPath (recf,name,Some dp) -> + xmlAddLoaPath loc ~attr:["rec",string_of_bool recf;"path",name] + [PCData (Names.DirPath.to_string dp)] + + | VernacRemoveLoadPath name -> xmlRemoveLoaPath loc ~attr:["path",name] [] + | VernacAddMLPath (recf,name) -> + xmlAddMLPath loc ~attr:["rec",string_of_bool recf;"path",name] [] + | VernacDeclareMLModule sl -> xmlDeclareMLModule loc sl + | VernacChdir _ as x -> xmlTODO loc x + + (* State management *) + | VernacWriteState _ as x -> xmlTODO loc x + | VernacRestoreState _ as x -> xmlTODO loc x + + (* Resetting *) + | VernacResetName _ as x -> xmlTODO loc x + | VernacResetInitial as x -> xmlTODO loc x + | VernacBack _ as x -> xmlTODO loc x + | VernacBackTo _ -> PCData "VernacBackTo" + + (* Commands *) + | VernacDeclareTacticDefinition _ as x -> xmlTODO loc x + | VernacCreateHintDb _ as x -> xmlTODO loc x + | VernacRemoveHints _ as x -> xmlTODO loc x + | VernacHints _ as x -> xmlTODO loc x + | VernacSyntacticDefinition ((_, name), (idl, ce), _, _) -> + let name = Id.to_string name in + let attrs = List.map (fun id -> ("id", Id.to_string id)) idl in + xmlNotation attrs name loc [pp_expr ce] + | VernacDeclareImplicits _ as x -> xmlTODO loc x + | VernacArguments _ as x -> xmlTODO loc x + | VernacArgumentsScope _ as x -> xmlTODO loc x + | VernacReserve _ as x -> xmlTODO loc x + | VernacGeneralizable _ as x -> xmlTODO loc x + | VernacSetOpacity _ as x -> xmlTODO loc x + | VernacSetStrategy _ as x -> xmlTODO loc x + | VernacUnsetOption _ as x -> xmlTODO loc x + | VernacSetOption _ as x -> xmlTODO loc x + | VernacAddOption _ as x -> xmlTODO loc x + | VernacRemoveOption _ as x -> xmlTODO loc x + | VernacMemOption _ as x -> xmlTODO loc x + | VernacPrintOption _ as x -> xmlTODO loc x + | VernacCheckMayEval (_,_,e) -> xmlCheck loc [pp_expr e] + | VernacGlobalCheck _ as x -> xmlTODO loc x + | VernacDeclareReduction _ as x -> xmlTODO loc x + | VernacPrint _ as x -> xmlTODO loc x + | VernacSearch _ as x -> xmlTODO loc x + | VernacLocate _ as x -> xmlTODO loc x + | VernacRegister _ as x -> xmlTODO loc x + | VernacComments (cl) -> + xmlComment loc (List.flatten (List.map pp_comment cl)) + | VernacNop as x -> xmlTODO loc x + + (* Stm backdoor *) + | VernacStm _ as x -> xmlTODO loc x + + (* Proof management *) + | VernacGoal _ as x -> xmlTODO loc x + | VernacAbort _ as x -> xmlTODO loc x + | VernacAbortAll -> PCData "VernacAbortAll" + | VernacRestart as x -> xmlTODO loc x + | VernacUndo _ as x -> xmlTODO loc x + | VernacUndoTo _ as x -> xmlTODO loc x + | VernacBacktrack _ as x -> xmlTODO loc x + | VernacFocus _ as x -> xmlTODO loc x + | VernacUnfocus as x -> xmlTODO loc x + | VernacUnfocused as x -> xmlTODO loc x + | VernacBullet _ as x -> xmlTODO loc x + | VernacSubproof _ as x -> xmlTODO loc x + | VernacEndSubproof as x -> xmlTODO loc x + | VernacShow _ as x -> xmlTODO loc x + | VernacCheckGuard as x -> xmlTODO loc x + | VernacProof (tac,using) -> + let tac = Option.map (xmlRawTactic "closingtactic") tac in + let using = Option.map (xmlSectionSubsetDescr "using") using in + xmlProof loc (Option.List.(cons tac (cons using []))) + | VernacProofMode name -> xmlProofMode loc name + + (* Toplevel control *) + | VernacToplevelControl _ as x -> xmlTODO loc x + + (* For extension *) + | VernacExtend _ as x -> + xmlExtend loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))] + + (* Flags *) + | VernacProgram e -> xmlApply loc (Element("program",[],[]) :: [tmpp e loc]) + | VernacLocal (b,e) -> + xmlApply loc (Element("local",["flag",string_of_bool b],[]) :: + [tmpp e loc]) + +let tmpp v loc = + match tmpp v loc with + | Element("ltac",_,_) as x -> x + | xml -> xmlGallina loc [xml] diff --git a/stm/texmacspp.mli b/stm/texmacspp.mli new file mode 100644 index 00000000..58dec8fd --- /dev/null +++ b/stm/texmacspp.mli @@ -0,0 +1,12 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Loc.t -> xml diff --git a/stm/vcs.ml b/stm/vcs.ml new file mode 100644 index 00000000..dfcbc19a --- /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*id) Dag.t + + val create_cluster : ('k,'e,'i) t -> id list -> (id * id) -> ('k,'e,'i) t + val cluster_of : ('k,'e,'i) t -> id -> (id * id) Dag.Cluster.t option + val delete_cluster : ('k,'e,'i) t -> (id * 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*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 00000000..fb79d02c --- /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 * id) Dag.t + + val create_cluster : ('k,'e,'i) t -> id list -> (id * id) -> ('k,'e,'i) t + val cluster_of : ('k,'e,'i) t -> id -> (id * id) Dag.Cluster.t option + val delete_cluster : ('k,'e,'i) t -> (id * 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 00000000..e9302bb7 --- /dev/null +++ b/stm/vernac_classifier.ml @@ -0,0 +1,227 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* "Unknown" + | VtStartProof _ -> "StartProof" + | VtSideff _ -> "Sideff" + | VtQed VtKeep -> "Qed(keep)" + | VtQed VtKeepAsAxiom -> "Qed(admitted)" + | VtQed VtDrop -> "Qed(drop)" + | VtProofStep false -> "ProofStep" + | VtProofStep true -> "ProofStep (parallel)" + | VtProofMode s -> "ProofMode " ^ s + | VtQuery (b,(id,route)) -> + "Query " ^ string_of_in_script b ^ " report " ^ Stateid.to_string id ^ + " route " ^ string_of_int route + | 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 : Vernacexpr.extend_name) + (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 (_,id) -> VtQuery (false,id), VtNow + | VtStm (x, _) -> VtStm (x, false), VtNow + | x -> x, VtNow + +let make_polymorphic (a, b as x) = + match a with + | VtStartProof (x, _, ids) -> + VtStartProof (x, Doesn'tGuaranteeOpacity, ids), b + | _ -> x + +let undo_classifier = ref (fun _ -> assert false) +let set_undo_classifier f = undo_classifier := f + +let rec classify_vernac e = + let rec 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 + | VernacPolymorphic (b, e) -> + if b || Flags.is_universe_polymorphism () (* Ok or not? *) then + make_polymorphic (classify_vernac e) + else classify_vernac e + | VernacTimeout (_,e) -> classify_vernac e + | VernacTime e -> classify_vernac_list 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 false, VtNow + | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow) + (* Qed *) + | VernacAbort _ -> VtQed VtDrop, VtLater + | VernacEndProof Admitted -> VtQed VtKeepAsAxiom, VtLater + | VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater + (* Query *) + | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _ + | VernacCheckMayEval _ -> + VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater + (* ProofStep *) + | VernacSolve (SelectAllParallel,_,_,_) -> VtProofStep true, VtLater + | VernacProof _ + | VernacBullet _ + | VernacFocus _ | VernacUnfocus + | VernacSubproof _ | VernacEndSubproof + | VernacSolve _ + | VernacCheckGuard + | VernacUnfocused + | VernacSolveExistential _ -> VtProofStep false, VtLater + (* Options changing parser *) + | VernacUnsetOption (["Default";"Proof";"Using"]) + | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow + (* StartProof *) + | VernacDefinition ( + (Some Decl_kinds.Discharge,Decl_kinds.Definition),(_,i),ProveBody _) -> + VtStartProof("Classic",Doesn'tGuaranteeOpacity,[i]), VtLater + | 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 + | VernacUniverse _ | VernacConstraint _ + | 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 _ + | VernacDeclareTacticDefinition _ + | VernacNameSectionHypSet _ + | VernacComments _ -> VtSideff [], VtLater + (* Who knows *) + | 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 _ | VernacNotationAddFormat _ + | VernacSyntaxExtension _ + | VernacSyntacticDefinition _ + | 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 + | VernacError _ -> assert false + (* Plugins should classify their commands *) + | VernacExtend (s,l) -> + try List.assoc s !classifiers l () + with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)) + and classify_vernac_list = function + (* spiwack: It would be better to define a monoid on classifiers. + So that the classifier of the list would be the composition of + the classifier of the individual commands. Currently: special + case for singleton lists.*) + | [_,c] -> static_classifier c + | l -> VtUnknown,VtNow + in + let res = static_classifier e in + if Flags.is_universe_polymorphism () then + make_polymorphic res + else res + +let classify_as_query = + VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater +let classify_as_sideeff = VtSideff [], VtLater +let classify_as_proofstep = VtProofStep false, VtLater diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli new file mode 100644 index 00000000..0680fe84 --- /dev/null +++ b/stm/vernac_classifier.mli @@ -0,0 +1,28 @@ +(************************************************************************) +(* 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 : + Vernacexpr.extend_name -> (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 +val classify_as_proofstep : vernac_classification + diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml new file mode 100644 index 00000000..84df3ecd --- /dev/null +++ b/stm/vio_checking.ml @@ -0,0 +1,144 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Stm.check_task f tasks ids && acc) true ts + +module Worker = Spawn.Sync(struct end) + +module IntOT = struct + type t = int + let compare = compare +end + +module Pool = Map.Make(IntOT) + +let schedule_vio_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 ".vio" 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-vio-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-vio-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_vio_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 ".vio" 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-vio2vo" :: 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; + [ "-vio2vo"; 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/vio_checking.mli b/stm/vio_checking.mli new file mode 100644 index 00000000..e2da5026 --- /dev/null +++ b/stm/vio_checking.mli @@ -0,0 +1,13 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* bool +val schedule_vio_checking : int -> string list -> unit + +val schedule_vio_compilation : int -> string list -> unit diff --git a/stm/workerPool.ml b/stm/workerPool.ml new file mode 100644 index 00000000..db3bb5ad --- /dev/null +++ b/stm/workerPool.ml @@ -0,0 +1,128 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit; (* called by manager to exit instead of Thread.exit *) + cancelled : unit -> bool; (* manager checks for a request of termination *) + extra : 'a; (* extra stuff to pass to the manager *) +} + +module type PoolModel = sig + (* this shall come from a Spawn.* model *) + type process + val spawn : int -> worker_id * process * CThread.thread_ic * out_channel + + (* this defines the main loop of the manager *) + type extra + val manager : + extra cpanel -> worker_id * process * CThread.thread_ic * out_channel -> unit +end + +module Make(Model : PoolModel) = struct + +type worker = { + name : worker_id; + cancel : bool ref; + manager : Thread.t; + process : Model.process; +} + +type pre_pool = { + workers : worker list ref; + count : int ref; + extra_arg : Model.extra; +} + +type pool = { lock : Mutex.t; pool : pre_pool } + +let magic_no = 17 + +let master_handshake worker_id ic oc = + try + Marshal.to_channel oc magic_no []; flush oc; + let n = (CThread.thread_friendly_input_value ic : int) in + if n <> magic_no then begin + Printf.eprintf "Handshake with %s failed: protocol mismatch\n" worker_id; + exit 1; + end + with e when Errors.noncritical e -> + Printf.eprintf "Handshake with %s failed: %s\n" + worker_id (Printexc.to_string e); + exit 1 + +let worker_handshake slave_ic slave_oc = + try + let v = (CThread.thread_friendly_input_value 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 + +let locking { lock; pool = p } f = + try + Mutex.lock lock; + let x = f p in + Mutex.unlock lock; + x + with e -> Mutex.unlock lock; raise e + +let rec create_worker extra pool id = + let cancel = ref false in + let name, process, ic, oc as worker = Model.spawn id in + master_handshake name ic oc; + let exit () = cancel := true; cleanup pool; Thread.exit () in + let cancelled () = !cancel in + let cpanel = { exit; cancelled; extra } in + let manager = Thread.create (Model.manager cpanel) worker in + { name; cancel; manager; process } + +and cleanup x = locking x begin fun { workers; count; extra_arg } -> + workers := List.map (function + | { cancel } as w when !cancel = false -> w + | _ -> let n = !count in incr count; create_worker extra_arg x n) + !workers +end + +let n_workers x = locking x begin fun { workers } -> + List.length !workers +end + +let is_empty x = locking x begin fun { workers } -> !workers = [] end + +let create extra_arg ~size = let x = { + lock = Mutex.create (); + pool = { + extra_arg; + workers = ref []; + count = ref size; + }} in + locking x begin fun { workers } -> + workers := CList.init size (create_worker extra_arg x) + end; + x + +let cancel n x = locking x begin fun { workers } -> + List.iter (fun { name; cancel } -> if n = name then cancel := true) !workers +end + +let cancel_all x = locking x begin fun { workers } -> + List.iter (fun { cancel } -> cancel := true) !workers +end + +let destroy x = locking x begin fun { workers } -> + List.iter (fun { cancel } -> cancel := true) !workers; + workers := [] +end + +end diff --git a/stm/workerPool.mli b/stm/workerPool.mli new file mode 100644 index 00000000..f46303b5 --- /dev/null +++ b/stm/workerPool.mli @@ -0,0 +1,46 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit; (* called by manager to exit instead of Thread.exit *) + cancelled : unit -> bool; (* manager checks for a request of termination *) + extra : 'a; (* extra stuff to pass to the manager *) +} + +module type PoolModel = sig + (* this shall come from a Spawn.* model *) + type process + val spawn : int -> worker_id * process * CThread.thread_ic * out_channel + + (* this defines the main loop of the manager *) + type extra + val manager : + extra cpanel -> worker_id * process * CThread.thread_ic * out_channel -> unit +end + +module Make(Model : PoolModel) : sig + + type pool + + val create : Model.extra -> size:int -> pool + + val is_empty : pool -> bool + val n_workers : pool -> int + + (* cancel signal *) + val cancel : worker_id -> pool -> unit + val cancel_all : pool -> unit + (* camcel signal + true removal, the pool is empty afterward *) + val destroy : pool -> unit + + (* The worker should call this function *) + val worker_handshake : CThread.thread_ic -> out_channel -> unit + +end -- cgit v1.2.3