aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-rw-r--r--stm/asyncTaskQueue.ml382
-rw-r--r--stm/asyncTaskQueue.mli222
-rw-r--r--stm/coqworkmgrApi.ml149
-rw-r--r--stm/coqworkmgrApi.mli53
-rw-r--r--stm/dag.ml150
-rw-r--r--stm/dag.mli58
-rw-r--r--stm/dune6
-rw-r--r--stm/proofBlockDelimiter.ml190
-rw-r--r--stm/proofBlockDelimiter.mli43
-rw-r--r--stm/spawned.ml81
-rw-r--r--stm/spawned.mli26
-rw-r--r--stm/stm.ml3376
-rw-r--r--stm/stm.mli299
-rw-r--r--stm/stm.mllib11
-rw-r--r--stm/tQueue.ml155
-rw-r--r--stm/tQueue.mli35
-rw-r--r--stm/vcs.ml190
-rw-r--r--stm/vcs.mli98
-rw-r--r--stm/vernac_classifier.ml219
-rw-r--r--stm/vernac_classifier.mli19
-rw-r--r--stm/vio_checking.ml153
-rw-r--r--stm/vio_checking.mli15
-rw-r--r--stm/workerPool.ml130
-rw-r--r--stm/workerPool.mli48
24 files changed, 6108 insertions, 0 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
new file mode 100644
index 0000000000..2493b1fac4
--- /dev/null
+++ b/stm/asyncTaskQueue.ml
@@ -0,0 +1,382 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open CErrors
+open Pp
+open Util
+
+let stm_pr_err pp = Format.eprintf "%s] @[%a@]\n%!" (Spawned.process_id ()) Pp.pp_with pp
+let stm_prerr_endline s = if !Flags.debug then begin stm_pr_err (str s) end else ()
+
+type cancel_switch = bool ref
+let async_proofs_flags_for_workers = ref []
+
+module type Task = sig
+
+ type task
+ type competence
+
+ type worker_status = Fresh | Old of competence
+
+ (* Marshallable *)
+ type request
+ type response
+
+ val name : string ref (* UID of the task kind, for -toploop *)
+ val extra_env : unit -> string array
+
+ (* run by the master, on a thread *)
+ val request_of_task : worker_status -> task -> request option
+ val task_match : worker_status -> task -> bool
+ val use_response : 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
+
+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 UnivGen.univ_unique_id list
+
+ 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 =
+ let open Feedback in
+ feedback ~id:Stateid.initial (WorkerStatus(id, s))
+
+ module Worker = Spawn.Sync ()
+
+ module Model = struct
+
+ type process = Worker.process
+ type extra = (T.task * cancel_switch) TQueue.t
+
+ let spawn id =
+ let name = Printf.sprintf "%s:%d" !T.name id in
+ let proc, ic, oc =
+ (* Filter arguments for slaves. *)
+ let rec set_slave_opt = function
+ | [] -> !async_proofs_flags_for_workers @
+ ["-worker-id"; name;
+ "-async-proofs-worker-priority";
+ CoqworkmgrApi.(string_of_priority !async_proofs_worker_priority)]
+ (* Options to discard: 0 arguments *)
+ | ("-emacs"|"-emacs-U"|"-batch")::tl ->
+ set_slave_opt tl
+ (* Options to discard: 1 argument *)
+ | ( "-async-proofs" | "-vio2vo" | "-o"
+ | "-load-vernac-source" | "-l" | "-load-vernac-source-verbose" | "-lv"
+ | "-compile" | "-compile-verbose"
+ | "-async-proofs-cache" | "-async-proofs-j" | "-async-proofs-tac-j"
+ | "-async-proofs-private-flags" | "-async-proofs-tactic-error-resilience"
+ | "-async-proofs-command-error-resilience" | "-async-proofs-delegation-threshold"
+ | "-async-proofs-worker-priority" | "-worker-id") :: _ :: tl ->
+ set_slave_opt tl
+ (* We need to pass some options with one argument *)
+ | ( "-I" | "-include" | "-top" | "-topfile" | "-coqlib" | "-exclude-dir" | "-compat"
+ | "-load-ml-object" | "-load-ml-source" | "-require" | "-w" | "-color" | "-init-file"
+ | "-profile-ltac-cutoff" | "-main-channel" | "-control-channel" | "-mangle-names" | "-set" | "-unset"
+ | "-diffs" | "-mangle-name" | "-dump-glob" | "-bytecode-compiler" | "-native-compiler" as x) :: a :: tl ->
+ x :: a :: set_slave_opt tl
+ (* We need to pass some options with two arguments *)
+ | ( "-R" | "-Q" as x) :: a1 :: a2 :: tl ->
+ x :: a1 :: a2 :: set_slave_opt tl
+ (* Finally we pass all options starting in '-'; check this is safe w.r.t the weird vio* option set *)
+ | x :: tl when x.[0] = '-' ->
+ x :: set_slave_opt tl
+ (* We assume this is a file, filter out *)
+ | _ :: tl ->
+ 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
+ let worker_name = System.get_toplevel_path ("coq" ^ !T.name) in
+ Worker.spawn ~env worker_name 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 T.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 () =
+ stm_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;
+ stm_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;
+ stm_prerr_endline ("got execution token") in
+ let kill proc =
+ Worker.kill proc;
+ stm_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 n (fun _ -> UnivGen.new_univ_id ()) 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.broadcast queue in
+ Worker.kill proc
+ else
+ let () = Unix.sleep 1 in
+ kill_if ()
+ in
+ let kill_if () =
+ try kill_if ()
+ with Sys.Break ->
+ let () = stop_waiting := true in
+ let () = TQueue.broadcast queue in
+ Worker.kill proc
+ in
+ let _ = CThread.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 -> stm_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 := T.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 ->
+ stm_pr_err Pp.(seq [str "Uncaught exception in worker manager: "; print e]);
+ flush_all (); raise Die
+ done with
+ | (Die | TQueue.BeingDestroyed) ->
+ giveback_exec_token (); kill proc; exit ()
+ | Sys_error _ | Invalid_argument _ | End_of_file ->
+ T.on_task_cancellation_or_expiration_or_slave_death !last_task;
+ giveback_exec_token (); kill proc; exit ()
+ end
+
+ module Pool = WorkerPool.Make(Model)
+
+ type queue = {
+ active : Pool.pool;
+ queue : (T.task * cancel_switch) TQueue.t;
+ cleaner : Thread.t option;
+ }
+
+ 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 = if size > 0 then Some (CThread.create cleaner queue) else None;
+ }
+
+ let destroy { active; queue } =
+ Pool.destroy active;
+ TQueue.destroy queue
+
+ let broadcast { queue } = TQueue.broadcast queue
+
+ let enqueue_task { queue; active } t ~cancel_switch =
+ stm_prerr_endline ("Enqueue task "^T.name_of_task t);
+ TQueue.push queue (t, cancel_switch)
+
+ 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 pp_pid pp = Pp.(str (Spawned.process_id () ^ " ") ++ pp)
+
+ let debug_with_pid = Feedback.(function
+ | { contents = Message(Debug, loc, pp) } as fb ->
+ { fb with contents = Message(Debug,loc, pp_pid pp) }
+ | x -> x)
+
+ let main_loop () =
+ (* We pass feedback to master *)
+ let slave_feeder oc fb =
+ Control.protect_sigalrm (fun () ->
+ Marshal.to_channel oc (RespFeedback (debug_with_pid fb)) []; flush oc) ()
+ in
+ ignore (Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x));
+ (* We ask master to allocate universe identifiers *)
+ UnivGen.set_remote_new_univ_id (bufferize @@ Control.protect_sigalrm (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;
+ CEphemeron.clean ()
+ with
+ | MarshalError s ->
+ stm_pr_err Pp.(prlist str ["Fatal marshal error: "; s]); flush_all (); exit 2
+ | End_of_file ->
+ stm_prerr_endline "connection lost"; flush_all (); exit 2
+ | e ->
+ stm_pr_err Pp.(seq [str "Slave: critical exception: "; 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 = CErrors.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 0000000000..067ea5df0c
--- /dev/null
+++ b/stm/asyncTaskQueue.mli
@@ -0,0 +1,222 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* Default flags for workers *)
+val async_proofs_flags_for_workers : string list ref
+
+(** This file provides an API for defining and managing a queue of
+ tasks to be done by external workers.
+
+ A queue of items of type [task] is maintained, then for each task,
+ a request is generated, then sent to a worker using marshalling.
+
+ The workers will then eventually return a result, using marshalling
+ again:
+ ____ ____ ____ ________
+ | T1 | T2 | T3 | => [request ] => | Worker |
+ |____|____|____| <= [response] <= |________|
+ | Master Proc. |
+ \--------------/
+
+ Thus [request] and [response] must be safely marshallable.
+
+ Operations for managing the task queue are provide, see below
+ for more details.
+
+ *)
+
+(** The [Task] module type defines an abstract message-processing
+ queue. *)
+module type Task = sig
+
+ (** Main description of a task. Elements are stored in the "master"
+ process, and then converted into a request.
+ *)
+ type task
+
+ (** [competence] stores the information about what kind of work a
+ worker has completed / has available. *)
+ type competence
+
+ (** A worker_status is:
+
+ - [`Fresh] when a worker is born.
+
+ - [`Old of competence]: When a worker ends a job it can either die
+ (and be replaced by a fresh new worker) or hang there as an [`Old]
+ worker. In such case some data can be carried by the [`Old]
+ constructor, typically used to implement [request_of_task].
+
+ This allows to implement both one-shot workers and "persistent"
+ ones. E.g. par: is implement using workers that don't
+ "reboot". Proof workers do reboot mainly because the vm has some
+ C state that cannot be cleared, so you have a real memory leak if
+ you don't reboot the worker. *)
+ type worker_status = Fresh | Old of competence
+
+ (** Type of input and output data for workers.
+
+ The data must be marshallable as it send through the network
+ using [Marshal] . *)
+ type request
+ type response
+
+ (** UID of the task kind, for -toploop *)
+ val name : string ref
+
+ (** Extra arguments of the task kind, for -toploop *)
+ val extra_env : unit -> string array
+
+ (** {5 Master API, it is run by the master, on a thread} *)
+
+ (** [request_of_task status t] takes the [status] of the worker
+ and a task [t] and creates the corresponding [Some request] to be
+ sent to the worker or it is not valid anymore [None]. *)
+ val request_of_task : worker_status -> task -> request option
+
+ (** [task_match status tid] Allows to discard tasks based on the
+ worker status. *)
+ val task_match : worker_status -> task -> bool
+
+ (** [use_response status t out]
+
+ For a response [out] to a task [t] with [status] we can choose
+ to end the worker of to keep it alive with some data and
+ immediately inject extra tasks in the queue.
+
+ For example, the proof worker runs a proof and finds an error,
+ the response signals that, e.g.
+
+ [ReponseError {state = 34; msg = "oops"}]
+
+ When the manager uses such a response he can tell the worker to
+ stay there and inject into the queue an extra task requesting
+ state 33 (to implement efficient proof repair). *)
+ val use_response : worker_status -> task -> response ->
+ [ `Stay of competence * task list | `End ]
+
+ (** [on_marshal_error err_msg tid] notifies of marshaling failure. *)
+ val on_marshal_error : string -> task -> unit
+
+ (** [on_task_cancellation_or_expiration_or_slave_death tid]
+
+ These functions are meant to parametrize the worker manager on
+ the actions to be taken when things go wrong or are cancelled
+ (you can kill a worker in CoqIDE, or using kill -9...)
+
+ E.g. master can decide to inhabit the (delegate) Future.t with a
+ closure (to be run in master), i.e. make the document still
+ checkable. This is what I do for marshaling errors. *)
+ val on_task_cancellation_or_expiration_or_slave_death : task option -> unit
+
+ (** [forward_feedback fb] sends fb to all the workers. *)
+ val forward_feedback : Feedback.feedback -> unit
+
+ (** {5 Worker API, it is run by worker, on a different fresh
+ process} *)
+
+ (** [perform in] synchronously processes a request [in] *)
+ val perform : request -> response
+
+ (** debugging *)
+ val name_of_task : task -> string
+ val name_of_request : request -> string
+
+end
+
+(** [cancel_switch] to be flipped to true by anyone to signal the task
+ is not relevant anymore. When the STM performs an undo/edit-at, it
+ crawls the document and flips these flags (the Qed node carries a
+ pointer to the flag IIRC).
+*)
+type cancel_switch = bool ref
+
+(** Client-side functor. [MakeQueue T] creates a task queue for task [T] *)
+module MakeQueue(T : Task) () : sig
+
+ (** [queue] is the abstract queue type. *)
+ type queue
+
+ (** [create n] will initialize the queue with [n] workers. If [n] is
+ 0, the queue won't spawn any process, working in a lazy local
+ manner. [not imposed by the this API] *)
+ val create : int -> queue
+
+ (** [destroy q] Deallocates [q], cancelling all pending tasks. *)
+ val destroy : queue -> unit
+
+ (** [n_workers q] returns the number of workers of [q] *)
+ val n_workers : queue -> int
+
+ (** [enqueue_task q t ~cancel_switch] schedules [t] for execution in
+ [q]. [cancel_switch] can be flipped to true to cancel the task. *)
+ val enqueue_task : queue -> T.task -> cancel_switch:cancel_switch -> unit
+
+ (** [join q] blocks until the task queue is empty *)
+ val join : queue -> unit
+
+ (** [cancel_all q] Cancels all tasks *)
+ val cancel_all : queue -> unit
+
+ (** [cancel_worker q wid] cancels a particular worker [wid] *)
+ val cancel_worker : queue -> WorkerPool.worker_id -> unit
+
+ (** [set_order q cmp] reorders [q] using ordering [cmp] *)
+ val set_order : queue -> (T.task -> T.task -> int) -> unit
+
+ (** [broadcast q]
+
+ This is nasty. Workers can be picky, e.g. pick tasks only when
+ they are "on screen". Of course the screen is scrolled, and that
+ changes the potential choice of workers to pick up a task or
+ not.
+
+ This function wakes up the workers (the managers) that give a
+ look (again) to the tasks in the queue.
+
+ The STM calls it when the perspective (as in PIDE) changes.
+
+ A problem here is that why task_match has access to the
+ competence data in order to decide if the task is palatable to
+ the worker or not... such data is local to the worker (manager).
+ The perspective is global, so it does not quite fit this
+ picture. This API to make all managers reconsider the tasks in
+ the queue is the best I could came up with.
+
+ This API is crucial to Coqoon (or any other UI that invokes
+ Stm.finish eagerly but wants the workers to "focus" on the visible
+ part of the document).
+ *)
+ val broadcast : queue -> unit
+
+ (** [snapshot q] Takes a snapshot (non destructive but waits until
+ all workers are enqueued) *)
+ val snapshot : queue -> T.task list
+
+ (** [clear q] Clears [q], only if the worker prool is empty *)
+ val clear : queue -> unit
+
+ (** [with_n_workers n f] create a queue, run the function, destroy
+ the queue. The user should call join *)
+ val with_n_workers : int -> (queue -> 'a) -> 'a
+
+end
+
+(** Server-side functor. [MakeWorker T] creates the server task
+ dispatcher. *)
+module MakeWorker(T : Task) () : sig
+
+ (** [init_stdout ()] is called at [Coqtop.toploop_init] time. *)
+ val init_stdout : unit -> unit
+
+ (** [main_loop ()] is called at [Coqtop.toploop_run] time. *)
+ val main_loop : unit -> unit
+
+end
diff --git a/stm/coqworkmgrApi.ml b/stm/coqworkmgrApi.ml
new file mode 100644
index 0000000000..841cc08c07
--- /dev/null
+++ b/stm/coqworkmgrApi.ml
@@ -0,0 +1,149 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+let debug = false
+
+type priority = Low | High
+
+(* Default priority *)
+let async_proofs_worker_priority = ref Low
+
+let string_of_priority = function Low -> "low" | High -> "high"
+let priority_of_string = function
+ | "low" -> Low
+ | "high" -> High
+ | _ -> raise (Invalid_argument "priority_of_string")
+
+type request =
+ | Hello of priority
+ | Get of int
+ | TryGet of int
+ | GiveBack of int
+ | Ping
+
+type response =
+ | Tokens of int
+ | Noluck
+ | Pong of int * int * int
+
+exception ParseError
+
+(* make it work with telnet: strip trailing \r *)
+let strip_r s =
+ let len = String.length s in
+ if s.[len - 1] <> '\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 Low
+ | [ "HELLO"; "HIGH" ] -> Hello 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 Low -> "HELLO LOW\n"
+ | Hello 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 () -> n)
+ (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 n)
+ (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 0000000000..be5b291776
--- /dev/null
+++ b/stm/coqworkmgrApi.mli
@@ -0,0 +1,53 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* High level api for clients of the service (like coqtop) *)
+
+type priority = Low | High
+val string_of_priority : priority -> string
+val priority_of_string : string -> priority
+
+(* Default priority *)
+val async_proofs_worker_priority : priority ref
+
+(* Connects to a work manager if any. If no worker manager, then
+ -async-proofs-j and -async-proofs-tac-j are used *)
+val init : priority -> unit
+
+(* blocking *)
+val get : int -> int
+
+(* not blocking *)
+val tryget : int -> int option
+val giveback : int -> unit
+
+(* Low level *)
+type request =
+ | Hello of 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 0000000000..eb5063bf0c
--- /dev/null
+++ b/stm/dag.ml
@@ -0,0 +1,150 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+module type S = sig
+
+ 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 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
+
+ module Property :
+ sig
+ type 'd t
+ val equal : 'd t -> 'd t -> bool
+ val compare : 'd t -> 'd t -> int
+ val to_string : 'd t -> string
+ val data : 'd t -> 'd
+ val having_it : 'd t -> NodeSet.t
+ end
+
+ val create_property : ('e,'i,'d) t -> node list -> 'd -> ('e,'i,'d) t
+ val property_of : ('e,'i,'d) t -> node -> 'd Property.t list
+ val del_property : ('e,'i,'d) t -> 'd Property.t -> ('e,'i,'d) t
+
+ val iter : ('e,'i,'d) t ->
+ (node -> 'd Property.t list -> 'i option ->
+ (node * 'e) list -> unit) -> unit
+
+end
+
+module Make(OT : Map.OrderedType) = struct
+
+module NodeSet = Set.Make(OT)
+
+module Property =
+struct
+ type 'd t = { data : 'd; uid : int; having_it : NodeSet.t }
+ let equal { uid = i1 } { uid = i2 } = Int.equal i1 i2
+ let compare { uid = i1 } { uid = i2 } = Int.compare i1 i2
+ let to_string { uid = i } = string_of_int i
+ let data { data = d } = d
+ let having_it { having_it } = having_it
+end
+
+type node = OT.t
+
+module NodeMap = CMap.Make(OT)
+
+type ('edge,'info,'data) t = {
+ graph : (node * 'edge) list NodeMap.t;
+ properties : 'data Property.t list NodeMap.t;
+ infos : 'info NodeMap.t;
+}
+
+let empty = {
+ graph = NodeMap.empty;
+ properties = 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;
+ properties = NodeMap.filter (fun n _ -> not(NodeSet.mem n s)) dag.properties;
+ 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 map_add_list k v m =
+ try
+ let l = NodeMap.find k m in
+ NodeMap.add k (v::l) m
+ with Not_found -> NodeMap.add k [v] m
+
+let clid = ref 1
+let create_property dag l data =
+ incr clid;
+ let having_it = List.fold_right NodeSet.add l NodeSet.empty in
+ let property = { Property.data; uid = !clid; having_it } in
+ { dag with properties =
+ List.fold_right (fun x ps -> map_add_list x property ps) l dag.properties }
+
+let property_of dag id =
+ try NodeMap.find id dag.properties
+ with Not_found -> []
+
+let del_property dag c =
+ { dag with properties =
+ NodeMap.filter (fun _ cl -> cl <> [])
+ (NodeMap.map (fun cl ->
+ List.filter (fun c' ->
+ not (Property.equal c' c)) cl)
+ dag.properties) }
+
+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 (property_of dag k) (get_info dag k) v) dag.graph
+
+let all_nodes dag = NodeMap.domain dag.graph
+
+end
+
diff --git a/stm/dag.mli b/stm/dag.mli
new file mode 100644
index 0000000000..cae4fccc73
--- /dev/null
+++ b/stm/dag.mli
@@ -0,0 +1,58 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+module type S = sig
+
+ 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 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
+
+ (* A property applies to a set of nodes and holds some data.
+ Stm uses this feature to group nodes contributing to the same proofs and
+ to structure proofs in boxes limiting the scope of errors *)
+ module Property :
+ sig
+ type 'd t
+ val equal : 'd t -> 'd t -> bool
+ val compare : 'd t -> 'd t -> int
+ val to_string : 'd t -> string
+ val data : 'd t -> 'd
+ val having_it : 'd t -> NodeSet.t
+ end
+
+ val create_property : ('e,'i,'d) t -> node list -> 'd -> ('e,'i,'d) t
+ val property_of : ('e,'i,'d) t -> node -> 'd Property.t list
+ val del_property : ('e,'i,'d) t -> 'd Property.t -> ('e,'i,'d) t
+
+ val iter : ('e,'i,'d) t ->
+ (node -> 'd Property.t list -> 'i option ->
+ (node * 'e) list -> unit) -> unit
+
+ end
+
+module Make(OT : Map.OrderedType) : S
+with type node = OT.t
+and type NodeSet.t = Set.Make(OT).t
+and type NodeSet.elt = OT.t
+
diff --git a/stm/dune b/stm/dune
new file mode 100644
index 0000000000..c369bd00fb
--- /dev/null
+++ b/stm/dune
@@ -0,0 +1,6 @@
+(library
+ (name stm)
+ (synopsis "Coq's Document Manager and Proof Checking Scheduler")
+ (public_name coq.stm)
+ (wrapped false)
+ (libraries vernac))
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
new file mode 100644
index 0000000000..d13763cdec
--- /dev/null
+++ b/stm/proofBlockDelimiter.ml
@@ -0,0 +1,190 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Stm
+
+module Util : sig
+
+val simple_goal : Evd.evar_map -> Goal.goal -> Goal.goal list -> bool
+val is_focused_goal_simple : doc:Stm.doc -> Stateid.t -> [ `Simple of Goal.goal list | `Not ]
+
+type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ]
+
+val crawl :
+ document_view -> ?init:document_node option ->
+ ('a -> document_node -> 'a until) -> 'a ->
+ static_block_declaration option
+
+val unit_val : Stm.DynBlockData.t
+val of_bullet_val : Proof_bullet.t -> Stm.DynBlockData.t
+val to_bullet_val : Stm.DynBlockData.t -> Proof_bullet.t
+val of_vernac_control_val : Vernacexpr.vernac_control -> Stm.DynBlockData.t
+val to_vernac_control_val : Stm.DynBlockData.t -> Vernacexpr.vernac_control
+
+end = struct
+
+let unit_tag = DynBlockData.create "unit"
+let unit_val = DynBlockData.Easy.inj () unit_tag
+
+let of_bullet_val, to_bullet_val = DynBlockData.Easy.make_dyn "bullet"
+let of_vernac_control_val, to_vernac_control_val = DynBlockData.Easy.make_dyn "vernac_control"
+
+let simple_goal sigma g gs =
+ let open Evar in
+ let open Evd in
+ let open Evarutil in
+ let evi = Evd.find sigma g in
+ Set.is_empty (evars_of_term (EConstr.Unsafe.to_constr evi.evar_concl)) &&
+ Set.is_empty (evars_of_filtered_evar_info (nf_evar_info sigma evi)) &&
+ not (List.exists (Proofview.depends_on sigma g) gs)
+
+let is_focused_goal_simple ~doc id =
+ match state_of_id ~doc id with
+ | `Expired | `Error _ | `Valid None -> `Not
+ | `Valid (Some { Vernacstate.proof }) ->
+ Option.cata (fun proof ->
+ let proof = Proof_global.give_me_the_proof proof in
+ let Proof.{ goals=focused; stack=r1; shelf=r2; given_up=r3; sigma } = Proof.data proof in
+ let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in
+ if List.for_all (fun x -> simple_goal sigma x rest) focused
+ then `Simple focused
+ else `Not) `Not proof
+
+type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ]
+
+let crawl { entry_point; prev_node } ?(init=Some entry_point) f acc =
+ let rec crawl node acc =
+ match node with
+ | None -> None
+ | Some node ->
+ match f acc node with
+ | `Stop -> None
+ | `Found x -> Some x
+ | `Cont acc -> crawl (prev_node node) acc in
+ crawl init acc
+
+end
+
+include Util
+
+(* ****************** - foo - bar - baz *********************************** *)
+
+let static_bullet ({ entry_point; prev_node } as view) =
+ assert (not (Vernacprop.has_Fail entry_point.ast));
+ match Vernacprop.under_control entry_point.ast with
+ | Vernacexpr.VernacBullet b ->
+ let base = entry_point.indentation in
+ let last_tac = prev_node entry_point in
+ crawl view ~init:last_tac (fun prev node ->
+ if node.indentation < base then `Stop else
+ if node.indentation > base then `Cont node else
+ if Vernacprop.has_Fail node.ast then `Stop
+ else match Vernacprop.under_control node.ast with
+ | Vernacexpr.VernacBullet b' when b = b' ->
+ `Found { block_stop = entry_point.id; block_start = prev.id;
+ dynamic_switch = node.id; carry_on_data = of_bullet_val b }
+ | _ -> `Stop) entry_point
+ | _ -> assert false
+
+let dynamic_bullet doc { dynamic_switch = id; carry_on_data = b } =
+ match is_focused_goal_simple ~doc id with
+ | `Simple focused ->
+ `ValidBlock {
+ base_state = id;
+ goals_to_admit = focused;
+ recovery_command = Some (Vernacexpr.VernacExpr([], Vernacexpr.VernacBullet (to_bullet_val b)))
+ }
+ | `Not -> `Leaks
+
+let () = register_proof_block_delimiter
+ "bullet" static_bullet dynamic_bullet
+
+(* ******************** { block } ***************************************** *)
+
+let static_curly_brace ({ entry_point; prev_node } as view) =
+ assert(Vernacprop.under_control entry_point.ast = Vernacexpr.VernacEndSubproof);
+ crawl view (fun (nesting,prev) node ->
+ if Vernacprop.has_Fail node.ast then `Cont (nesting,node)
+ else match Vernacprop.under_control node.ast with
+ | Vernacexpr.VernacSubproof _ when nesting = 0 ->
+ `Found { block_stop = entry_point.id; block_start = prev.id;
+ dynamic_switch = node.id; carry_on_data = unit_val }
+ | Vernacexpr.VernacSubproof _ ->
+ `Cont (nesting - 1,node)
+ | Vernacexpr.VernacEndSubproof ->
+ `Cont (nesting + 1,node)
+ | _ -> `Cont (nesting,node)) (-1, entry_point)
+
+let dynamic_curly_brace doc { dynamic_switch = id } =
+ match is_focused_goal_simple ~doc id with
+ | `Simple focused ->
+ `ValidBlock {
+ base_state = id;
+ goals_to_admit = focused;
+ recovery_command = Some (Vernacexpr.VernacExpr ([], Vernacexpr.VernacEndSubproof))
+ }
+ | `Not -> `Leaks
+
+let () = register_proof_block_delimiter
+ "curly" static_curly_brace dynamic_curly_brace
+
+(* ***************** par: ************************************************* *)
+
+let static_par { entry_point; prev_node } =
+ match prev_node entry_point with
+ | None -> None
+ | Some { id = pid } ->
+ Some { block_stop = entry_point.id; block_start = pid;
+ dynamic_switch = pid; carry_on_data = unit_val }
+
+let dynamic_par doc { dynamic_switch = id } =
+ match is_focused_goal_simple ~doc id with
+ | `Simple focused ->
+ `ValidBlock {
+ base_state = id;
+ goals_to_admit = focused;
+ recovery_command = None;
+ }
+ | `Not -> `Leaks
+
+let () = register_proof_block_delimiter "par" static_par dynamic_par
+
+(* ***************** simple indentation *********************************** *)
+
+let static_indent ({ entry_point; prev_node } as view) =
+ Printf.eprintf "@%d\n" (Stateid.to_int entry_point.id);
+ match prev_node entry_point with
+ | None -> None
+ | Some last_tac ->
+ if last_tac.indentation <= entry_point.indentation then None
+ else
+ crawl view ~init:(Some last_tac) (fun prev node ->
+ if node.indentation >= last_tac.indentation then `Cont node
+ else
+ `Found { block_stop = entry_point.id; block_start = node.id;
+ dynamic_switch = node.id;
+ carry_on_data = of_vernac_control_val entry_point.ast }
+ ) last_tac
+
+let dynamic_indent doc { dynamic_switch = id; carry_on_data = e } =
+ Printf.eprintf "%s\n" (Stateid.to_string id);
+ match is_focused_goal_simple ~doc id with
+ | `Simple [] -> `Leaks
+ | `Simple focused ->
+ let but_last = List.tl (List.rev focused) in
+ `ValidBlock {
+ base_state = id;
+ goals_to_admit = but_last;
+ recovery_command = Some (to_vernac_control_val e);
+ }
+ | `Not -> `Leaks
+
+let () = register_proof_block_delimiter "indent" static_indent dynamic_indent
+
diff --git a/stm/proofBlockDelimiter.mli b/stm/proofBlockDelimiter.mli
new file mode 100644
index 0000000000..eacd3687ae
--- /dev/null
+++ b/stm/proofBlockDelimiter.mli
@@ -0,0 +1,43 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* This file implements proof block detection for:
+ - blocks delimited by { and }
+ - bullets with indentation
+ - par: terminator
+
+ It exports utility functions to ease the development of other proof block
+ detection code.
+*)
+
+(** A goal is simple if it nor depends on nor impacts on any other goal.
+ This function is used to detect, dynamically, if a proof block leaks,
+ i.e. if skipping it could impact other goals (like not instantiating their
+ type). `Simple carries the list of focused goals.
+*)
+val simple_goal : Evd.evar_map -> Goal.goal -> Goal.goal list -> bool
+val is_focused_goal_simple : doc:Stm.doc -> Stateid.t -> [ `Simple of Goal.goal list | `Not ]
+
+type 'a until = [ `Stop | `Found of Stm.static_block_declaration | `Cont of 'a ]
+
+(* Simpler function to crawl the document backward to detect the block.
+ * ?init is the entry point of the document view if not given *)
+val crawl :
+ Stm.document_view -> ?init:Stm.document_node option ->
+ ('a -> Stm.document_node -> 'a until) -> 'a ->
+ Stm.static_block_declaration option
+
+(* Dummy value for static_block_declaration when no real value is needed *)
+val unit_val : Stm.DynBlockData.t
+
+(* Bullets *)
+val of_bullet_val : Proof_bullet.t -> Stm.DynBlockData.t
+val to_bullet_val : Stm.DynBlockData.t -> Proof_bullet.t
+
diff --git a/stm/spawned.ml b/stm/spawned.ml
new file mode 100644
index 0000000000..bd772d825d
--- /dev/null
+++ b/stm/spawned.ml
@@ -0,0 +1,81 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Spawn
+
+let pr_err s = Printf.eprintf "(Spawned,%d) %s\n%!" (Unix.getpid ()) s
+let prerr_endline s = if !Flags.debug then begin pr_err s end else ()
+
+type chandescr = AnonPipe | Socket of string * int * int
+
+let open_bin_connection h pr pw =
+ let open Unix in
+ let _, cout = open_connection (ADDR_INET (inet_addr_of_string h,pr)) in
+ let cin, _ = open_connection (ADDR_INET (inet_addr_of_string h,pw)) 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 pr pw =
+ prerr_endline "starting controller thread";
+ let main () =
+ let ic, oc = open_bin_connection h pr pw in
+ let 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
+ with
+ | e ->
+ prerr_endline ("control channel broken: " ^ Printexc.to_string e);
+ exit 1 in
+ loop () in
+ ignore(CThread.create main ())
+
+let main_channel = ref None
+let control_channel = ref None
+
+let channels = ref None
+
+let init_channels () =
+ if !channels <> None then CErrors.anomaly(Pp.str "init_channels called twice.");
+ let () = match !main_channel with
+ | None -> ()
+ | Some (Socket(mh,mpr,mpw)) ->
+ channels := Some (open_bin_connection mh mpr mpw);
+ | 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, cpr, cpw)) ->
+ controller ch cpr cpw
+ | Some AnonPipe ->
+ CErrors.anomaly (Pp.str "control channel cannot be a pipe.")
+
+let get_channels () =
+ match !channels with
+ | None ->
+ Printf.eprintf "Fatal error: ideslave communication channels not set.\n";
+ exit 1
+ | Some(ic, oc) -> ic, oc
+
+let process_id () =
+ Printf.sprintf "%d:%s:%d" (Unix.getpid ())
+ (if Flags.async_proofs_is_worker () then !Flags.async_proofs_worker_id
+ else "master")
+ (Thread.id (Thread.self ()))
diff --git a/stm/spawned.mli b/stm/spawned.mli
new file mode 100644
index 0000000000..df4e725953
--- /dev/null
+++ b/stm/spawned.mli
@@ -0,0 +1,26 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* To link this file, threads are needed *)
+
+type chandescr = AnonPipe | Socket of string * int * int
+
+(* Argument parsing should set these *)
+val main_channel : chandescr option ref
+val control_channel : chandescr option ref
+
+(* Immediately after argument parsing one *must* call this *)
+val init_channels : unit -> unit
+
+(* Once initialized, these are the channels to talk with our master *)
+val get_channels : unit -> CThread.thread_ic * out_channel
+
+(** {6 Name of current process.} *)
+val process_id : unit -> string
diff --git a/stm/stm.ml b/stm/stm.ml
new file mode 100644
index 0000000000..e1ab45163a
--- /dev/null
+++ b/stm/stm.ml
@@ -0,0 +1,3376 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* enable in case of stm problems *)
+(* let stm_debug () = !Flags.debug *)
+let stm_debug = ref false
+
+let stm_pr_err s = Format.eprintf "%s] %s\n%!" (Spawned.process_id ()) s
+let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n%!" (Spawned.process_id ()) Pp.pp_with pp
+
+let stm_prerr_endline s = if !stm_debug then begin stm_pr_err (s ()) end else ()
+let stm_pperr_endline s = if !stm_debug then begin stm_pp_err (s ()) end else ()
+
+let stm_prerr_debug s = if !Flags.debug then begin stm_pr_err (s ()) end else ()
+
+open Pp
+open CErrors
+open Names
+open Feedback
+open Vernacexpr
+open Vernacextend
+
+let is_vtkeep = function VtKeep _ -> true | _ -> false
+let get_vtkeep = function VtKeep x -> x | _ -> assert false
+
+module AsyncOpts = struct
+
+ type cache = Force
+ type async_proofs = APoff | APonLazy | APon
+ type tac_error_filter = [ `None | `Only of string list | `All ]
+
+ type stm_opt = {
+ async_proofs_n_workers : int;
+ async_proofs_n_tacworkers : int;
+
+ async_proofs_cache : cache option;
+ async_proofs_mode : async_proofs;
+
+ async_proofs_private_flags : string option;
+ async_proofs_never_reopen_branch : bool;
+
+ async_proofs_tac_error_resilience : tac_error_filter;
+ async_proofs_cmd_error_resilience : bool;
+ async_proofs_delegation_threshold : float;
+ }
+
+ let default_opts = {
+ async_proofs_n_workers = 1;
+ async_proofs_n_tacworkers = 2;
+
+ async_proofs_cache = None;
+
+ async_proofs_mode = APoff;
+
+ async_proofs_private_flags = None;
+ async_proofs_never_reopen_branch = false;
+
+ async_proofs_tac_error_resilience = `Only [ "curly" ];
+ async_proofs_cmd_error_resilience = true;
+ async_proofs_delegation_threshold = 0.03;
+ }
+
+ let cur_opt = ref default_opts
+end
+
+open AsyncOpts
+
+let async_proofs_is_master opt =
+ opt.async_proofs_mode = APon &&
+ !Flags.async_proofs_worker_id = "master"
+
+let execution_error ?loc state_id msg =
+ feedback ~id:state_id (Message (Error, loc, msg))
+
+module Hooks = struct
+
+let state_computed, state_computed_hook = Hook.make
+ ~default:(fun ~doc:_ state_id ~in_cache ->
+ feedback ~id:state_id Processed) ()
+
+let state_ready, state_ready_hook = Hook.make
+ ~default:(fun ~doc:_ state_id -> ()) ()
+
+let forward_feedback, forward_feedback_hook =
+ let m = Mutex.create () in
+ Hook.make ~default:(function
+ | { doc_id = did; span_id = id; route; contents } ->
+ try Mutex.lock m; feedback ~did ~id ~route contents; Mutex.unlock m
+ with e -> Mutex.unlock m; raise e) ()
+
+let unreachable_state, unreachable_state_hook = Hook.make
+ ~default:(fun ~doc:_ _ _ -> ()) ()
+
+include Hook
+
+(* enables: Hooks.(call foo args) *)
+let call = get
+
+let call_process_error_once =
+ let processed : unit Exninfo.t = Exninfo.make () in
+ fun (_, info as ei) ->
+ match Exninfo.get info processed with
+ | Some _ -> ei
+ | None ->
+ let e, info = ExplainErr.process_vernac_interp_error ei in
+ let info = Exninfo.add info processed () in
+ e, info
+
+end
+
+let async_proofs_workers_extra_env = ref [||]
+
+type aast = {
+ verbose : bool;
+ loc : Loc.t option;
+ indentation : int;
+ strlen : int;
+ mutable expr : vernac_control; (* mutable: Proof using hinted by aux file *)
+}
+let pr_ast { expr; indentation } = Pp.(int indentation ++ str " " ++ Ppvernac.pr_vernac expr)
+
+(* Commands piercing opaque *)
+let may_pierce_opaque = function
+ | VernacPrint _
+ | VernacExtend (("Extraction",_), _)
+ | VernacExtend (("SeparateExtraction",_), _)
+ | VernacExtend (("ExtractionLibrary",_), _)
+ | VernacExtend (("RecursiveExtractionLibrary",_), _)
+ | VernacExtend (("ExtractionConstant",_), _)
+ | VernacExtend (("ExtractionInlinedConstant",_), _)
+ | VernacExtend (("ExtractionInductive",_), _) -> true
+ | _ -> false
+
+let update_global_env () =
+ if Vernacstate.Proof_global.there_are_pending_proofs () then
+ Vernacstate.Proof_global.update_global_env ()
+
+module Vcs_ = Vcs.Make(Stateid.Self)
+type future_proof = Proof_global.closed_proof_output Future.computation
+
+type depth = int
+type branch_type =
+ [ `Master
+ | `Proof of depth
+ | `Edit of
+ Stateid.t * Stateid.t * Vernacextend.vernac_qed_type * Vcs_.Branch.t ]
+(* TODO 8.7 : split commands and tactics, since this type is too messy now *)
+type cmd_t = {
+ ctac : bool; (* is a tactic *)
+ ceff : bool; (* is a side-effecting command in the middle of a proof *)
+ cast : aast;
+ cids : Names.Id.t list;
+ cblock : proof_block_name option;
+ cqueue : [ `MainQueue
+ | `TacQueue of solving_tac * anon_abstracting_tac * AsyncTaskQueue.cancel_switch
+ | `QueryQueue of AsyncTaskQueue.cancel_switch
+ | `SkipQueue ] }
+type fork_t = aast * Vcs_.Branch.t * opacity_guarantee * Names.Id.t list
+type qed_t = {
+ qast : aast;
+ keep : vernac_qed_type;
+ mutable fproof : (future_proof * AsyncTaskQueue.cancel_switch) option;
+ brname : Vcs_.Branch.t;
+ brinfo : branch_type Vcs_.branch_info
+}
+type seff_t = ReplayCommand of aast | CherryPickEnv
+type alias_t = Stateid.t * aast
+
+type transaction =
+ | Cmd of cmd_t
+ | Fork of fork_t
+ | Qed of qed_t
+ | Sideff of seff_t
+ | Alias of alias_t
+ | Noop
+type step =
+ [ `Cmd of cmd_t
+ | `Fork of fork_t * Stateid.t option
+ | `Qed of qed_t * Stateid.t
+ | `Sideff of seff_t * Stateid.t
+ | `Alias of alias_t ]
+
+type visit = { step : step; next : Stateid.t }
+
+let mkTransTac cast cblock cqueue =
+ Cmd { ctac = true; cast; cblock; cqueue; cids = []; ceff = false }
+
+let mkTransCmd cast cids ceff cqueue =
+ Cmd { ctac = false; cast; cblock = None; cqueue; cids; ceff }
+
+(* Parts of the system state that are morally part of the proof state *)
+let summary_pstate = Evarutil.meta_counter_summary_tag,
+ Evd.evar_counter_summary_tag,
+ Obligations.program_tcc_summary_tag
+
+type cached_state =
+ | EmptyState
+ | ParsingState of Vernacstate.Parser.state
+ | FullState of Vernacstate.t
+ | ErrorState of Vernacstate.Parser.state option * Exninfo.iexn
+type branch = Vcs_.Branch.t * branch_type Vcs_.branch_info
+type backup = { mine : branch; others : branch list }
+
+type 'vcs state_info = { (* TODO: Make this record private to VCS *)
+ mutable n_reached : int; (* debug cache: how many times was computed *)
+ mutable n_goals : int; (* open goals: indentation *)
+ mutable state : cached_state; (* state value *)
+ mutable proof_mode : Pvernac.proof_mode option;
+ mutable vcs_backup : 'vcs option * backup option;
+}
+let default_info proof_mode =
+ {
+ n_reached = 0; n_goals = 0;
+ state = EmptyState;
+ proof_mode;
+ vcs_backup = (None,None);
+ }
+
+module DynBlockData : Dyn.S = Dyn.Make ()
+
+(* Clusters of nodes implemented as Dag properties. While Dag and Vcs impose
+ * no constraint on properties, here we impose boxes to be non overlapping.
+ * Such invariant makes sense for the current kinds of boxes (proof blocks and
+ * entire proofs) but may make no sense and dropped/refined in the future.
+ * Such invariant is useful to detect broken proof block detection code *)
+type box =
+ | ProofTask of pt
+ | ProofBlock of static_block_declaration * proof_block_name
+and pt = { (* TODO: inline records in OCaml 4.03 *)
+ lemma : Stateid.t;
+ qed : Stateid.t;
+}
+and static_block_declaration = {
+ block_start : Stateid.t;
+ block_stop : Stateid.t;
+ dynamic_switch : Stateid.t;
+ carry_on_data : DynBlockData.t;
+}
+
+(* Functions that work on a Vcs with a specific branch type *)
+module Vcs_aux : sig
+
+ val proof_nesting : (branch_type, 't,'i,'c) Vcs_.t -> int
+ val find_proof_at_depth :
+ (branch_type, 't, 'i,'c) Vcs_.t -> int ->
+ Vcs_.Branch.t * branch_type Vcs_.branch_info
+ exception Expired
+ val visit : (branch_type, transaction,'i,'c) Vcs_.t -> Vcs_.Dag.node -> visit
+
+end = struct (* {{{ *)
+
+ let proof_nesting vcs =
+ List.fold_left max 0
+ (CList.map_filter
+ (function
+ | { Vcs_.kind = `Proof n } -> Some n
+ | { Vcs_.kind = `Edit _ } -> Some 1
+ | _ -> None)
+ (List.map (Vcs_.get_branch vcs) (Vcs_.branches vcs)))
+
+ let find_proof_at_depth vcs pl =
+ try List.find (function
+ | _, { Vcs_.kind = `Proof n } -> Int.equal n pl
+ | _, { Vcs_.kind = `Edit _ } -> anomaly(Pp.str "find_proof_at_depth")
+ | _ -> false)
+ (List.map (fun h -> h, Vcs_.get_branch vcs h) (Vcs_.branches vcs))
+ with Not_found -> failwith "find_proof_at_depth"
+
+ exception Expired
+ let visit vcs id =
+ if Stateid.equal id Stateid.initial then
+ anomaly(Pp.str "Visiting the initial state id.")
+ else if Stateid.equal id Stateid.dummy then
+ anomaly(Pp.str "Visiting the dummy state id.")
+ else
+ try
+ match Vcs_.Dag.from_node (Vcs_.dag vcs) id with
+ | [n, Cmd x] -> { step = `Cmd x; next = n }
+ | [n, Alias x] -> { step = `Alias x; next = n }
+ | [n, Fork x] -> { step = `Fork (x,None); next = n }
+ | [n, Fork x; p, Noop] -> { step = `Fork (x,Some p); next = n }
+ | [p, Noop; n, Fork x] -> { step = `Fork (x,Some p); next = n }
+ | [n, Qed x; p, Noop]
+ | [p, Noop; n, Qed x] -> { step = `Qed (x,p); next = n }
+ | [n, Sideff CherryPickEnv; p, Noop]
+ | [p, Noop; n, Sideff CherryPickEnv]-> { step = `Sideff (CherryPickEnv, p); next = n }
+ | [n, Sideff (ReplayCommand x); p, Noop]
+ | [p, Noop; n, Sideff (ReplayCommand x)]-> { step = `Sideff(ReplayCommand x,p); next = n }
+ | [n, Sideff (ReplayCommand x)]-> {step = `Sideff(ReplayCommand x, Stateid.dummy); next=n}
+ | _ -> anomaly (Pp.str ("Malformed VCS at node "^Stateid.to_string id^"."))
+ with Not_found -> raise Expired
+
+end (* }}} *)
+
+(*************************** THE DOCUMENT *************************************)
+(******************************************************************************)
+
+type interactive_top = TopLogical of DirPath.t | TopPhysical of string
+
+(* The main document type associated to a VCS *)
+type stm_doc_type =
+ | VoDoc of string
+ | VioDoc of string
+ | Interactive of interactive_top
+
+(* Dummy until we land the functional interp patch + fixed start_library *)
+type doc = int
+let dummy_doc : doc = 0
+
+(* Imperative wrap around VCS to obtain _the_ VCS that is the
+ * representation of the document Coq is currently processing *)
+module VCS : sig
+
+ exception Expired
+
+ module Branch : (module type of Vcs_.Branch with type t = Vcs_.Branch.t)
+ type id = Stateid.t
+ type 'branch_type branch_info = 'branch_type Vcs_.branch_info = {
+ kind : [> `Master] as 'branch_type;
+ root : id;
+ pos : id;
+ }
+
+ type vcs = (branch_type, transaction, vcs state_info, box) Vcs_.t
+
+ val init : stm_doc_type -> id -> Vernacstate.Parser.state -> doc
+ (* val get_type : unit -> stm_doc_type *)
+ val set_ldir : Names.DirPath.t -> unit
+ val get_ldir : unit -> Names.DirPath.t
+
+ val is_interactive : unit -> bool
+ val is_vio_doc : unit -> bool
+
+ val current_branch : unit -> Branch.t
+ val checkout : Branch.t -> unit
+ val branches : unit -> Branch.t list
+ val get_branch : Branch.t -> branch_type branch_info
+ val get_branch_pos : Branch.t -> id
+ val new_node : ?id:Stateid.t -> Pvernac.proof_mode option -> unit -> id
+ val merge : id -> ours:transaction -> ?into:Branch.t -> Branch.t -> unit
+ val rewrite_merge : id -> ours:transaction -> at:id -> Branch.t -> unit
+ val delete_branch : Branch.t -> unit
+ val commit : id -> transaction -> unit
+ val mk_branch_name : aast -> Branch.t
+ val edit_branch : Branch.t
+ val branch : ?root:id -> ?pos:id -> Branch.t -> branch_type -> unit
+ val reset_branch : Branch.t -> id -> unit
+ val reachable : id -> Stateid.Set.t
+ val cur_tip : unit -> id
+
+ val get_info : id -> vcs state_info
+ val reached : id -> unit
+ val goals : id -> int -> unit
+ val set_state : id -> cached_state -> unit
+ val get_state : id -> cached_state
+ val set_parsing_state : id -> Vernacstate.Parser.state -> unit
+ val get_parsing_state : id -> Vernacstate.Parser.state option
+ val get_proof_mode : id -> Pvernac.proof_mode option
+ val set_proof_mode : id -> Pvernac.proof_mode option -> unit
+
+ (* cuts from start -> stop, raising Expired if some nodes are not there *)
+ val slice : block_start:id -> block_stop:id -> vcs
+ val nodes_in_slice : block_start:id -> block_stop:id -> Stateid.t list
+
+ val create_proof_task_box : id list -> qed:id -> block_start:id -> unit
+ val create_proof_block : static_block_declaration -> string -> unit
+ val box_of : id -> box list
+ val delete_boxes_of : id -> unit
+ val proof_task_box_of : id -> pt option
+
+ val proof_nesting : unit -> int
+ val checkout_shallowest_proof_branch : unit -> unit
+ val propagate_sideff : action:seff_t -> Stateid.t list
+ val propagate_qed : unit -> unit
+
+ val gc : unit -> unit
+
+ val visit : id -> visit
+
+ val print : ?now:bool -> unit -> unit
+
+ val backup : unit -> vcs
+ val restore : vcs -> unit
+
+end = struct (* {{{ *)
+
+ include Vcs_
+ exception Expired = Vcs_aux.Expired
+
+ open Printf
+
+ let print_dag vcs () =
+
+ (* Due to threading, be wary that this will be called from the
+ toplevel with we_are_parsing set to true, as indeed, the
+ toplevel is waiting for input . What a race! XD
+
+ In case you are hitting the race enable stm_debug.
+ *)
+ if !stm_debug then Flags.we_are_parsing := false;
+
+ let fname =
+ "stm_" ^ Str.global_replace (Str.regexp " ") "_" (Spawned.process_id ()) in
+ let string_of_transaction = function
+ | Cmd { cast = t } | Fork (t, _,_,_) ->
+ (try Pp.string_of_ppcmds (pr_ast t) with _ -> "ERR")
+ | Sideff (ReplayCommand t) ->
+ sprintf "Sideff(%s)"
+ (try Pp.string_of_ppcmds (pr_ast t) with _ -> "ERR")
+ | Sideff CherryPickEnv -> "EnvChange"
+ | Noop -> " "
+ | Alias (id,_) -> sprintf "Alias(%s)" (Stateid.to_string id)
+ | Qed { qast } -> Pp.string_of_ppcmds (pr_ast qast) in
+ let is_green id =
+ match get_info vcs id with
+ | Some { state = FullState _ } -> true
+ | _ -> false in
+ let is_red id =
+ match get_info vcs id with
+ | Some { state = ErrorState _ } -> true
+ | _ -> false in
+ let head = current_branch vcs in
+ let heads =
+ List.map (fun x -> x, (get_branch vcs x).pos) (branches vcs) in
+ let graph = dag vcs in
+ let quote s =
+ Str.global_replace (Str.regexp "\n") "<BR/>"
+ (Str.global_replace (Str.regexp "<") "&lt;"
+ (Str.global_replace (Str.regexp ">") "&gt;"
+ (Str.global_replace (Str.regexp "\"") "&quot;"
+ (Str.global_replace (Str.regexp "&") "&amp;"
+ (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 "<<FONT POINT-SIZE=\"12\" FACE=\"sans\">%s</FONT>>"
+ (quote (string_of_transaction tr)) in
+ let node_info id =
+ match get_info vcs id with
+ | None -> ""
+ | Some info ->
+ sprintf "<<FONT POINT-SIZE=\"12\">%s</FONT>" (Stateid.to_string id) ^
+ sprintf " <FONT POINT-SIZE=\"11\">r:%d g:%d</FONT>>"
+ info.n_reached info.n_goals in
+ let color id =
+ if is_red id then "red" else if is_green id then "green" else "white" in
+ let nodefmt oc id =
+ fprintf oc "%s [label=%s,style=filled,fillcolor=%s];\n"
+ (node id) (node_info id) (color id) in
+
+ let ids = ref Stateid.Set.empty in
+ let boxes = ref [] in
+ (* Fill in *)
+ Dag.iter graph (fun from _ _ l ->
+ ids := Stateid.Set.add from !ids;
+ List.iter (fun box -> boxes := box :: !boxes)
+ (Dag.property_of graph from);
+ List.iter (fun (dest, _) ->
+ ids := Stateid.Set.add dest !ids;
+ List.iter (fun box -> boxes := box :: !boxes)
+ (Dag.property_of graph dest))
+ l);
+ boxes := CList.sort_uniquize Dag.Property.compare !boxes;
+
+ let oc = open_out fname_dot in
+ output_string oc "digraph states {\n";
+ Dag.iter graph (fun from cf _ l ->
+ List.iter (fun (dest, trans) ->
+ fprintf oc "%s -> %s [xlabel=%s,labelfloat=true];\n"
+ (node from) (node dest) (edge trans)) l
+ );
+
+ let contains b1 b2 =
+ Stateid.Set.subset
+ (Dag.Property.having_it b2) (Dag.Property.having_it b1) in
+ let same_box = Dag.Property.equal in
+ let outerboxes boxes =
+ List.filter (fun b ->
+ not (List.exists (fun b1 ->
+ not (same_box b1 b) && contains b1 b) boxes)
+ ) boxes in
+ let rec rec_print b =
+ boxes := CList.remove same_box b !boxes;
+ let sub_boxes = List.filter (contains b) (outerboxes !boxes) in
+ fprintf oc "subgraph cluster_%s {\n" (Dag.Property.to_string b);
+ List.iter rec_print sub_boxes;
+ Stateid.Set.iter (fun id ->
+ if Stateid.Set.mem id !ids then begin
+ ids := Stateid.Set.remove id !ids;
+ nodefmt oc id
+ end)
+ (Dag.Property.having_it b);
+ match Dag.Property.data b with
+ | ProofBlock ({ dynamic_switch = id }, lbl) ->
+ fprintf oc "label=\"%s (test:%s)\";\n" lbl (Stateid.to_string id);
+ fprintf oc "color=red; }\n"
+ | ProofTask _ -> fprintf oc "color=blue; }\n"
+ in
+ List.iter rec_print (outerboxes !boxes);
+ Stateid.Set.iter (nodefmt oc) !ids;
+
+ List.iteri (fun i (b,id) ->
+ let shape = if Branch.equal head b then "box3d" else "box" in
+ fprintf oc "b%d -> %s;\n" i (node id);
+ fprintf oc "b%d [shape=%s,label=\"%s\"];\n" i shape
+ (Branch.to_string b);
+ ) heads;
+
+ output_string oc "}\n";
+ close_out oc;
+ ignore(Sys.command
+ ("dot -Tpdf -Gcharset=latin1 " ^ fname_dot ^ " -o" ^ fname_ps))
+
+ type vcs = (branch_type, transaction, vcs state_info, box) t
+ let vcs : vcs ref = ref (empty Stateid.dummy)
+
+ let doc_type = ref (Interactive (TopLogical (Names.DirPath.make [])))
+ let ldir = ref Names.DirPath.empty
+
+ let init dt id ps =
+ doc_type := dt;
+ vcs := empty id;
+ let info = { (default_info None) with state = ParsingState ps } in
+ vcs := set_info !vcs id info;
+ dummy_doc
+
+ let set_ldir ld =
+ ldir := ld
+
+ let get_ldir () = !ldir
+ (* let get_type () = !doc_type *)
+
+ let is_interactive () =
+ match !doc_type with
+ | Interactive _ -> true
+ | _ -> false
+
+ let is_vio_doc () =
+ match !doc_type with
+ | VioDoc _ -> true
+ | _ -> false
+
+ let current_branch () = current_branch !vcs
+
+ let checkout head = vcs := checkout !vcs head
+ let branches () = branches !vcs
+ let get_branch head = get_branch !vcs head
+ let get_branch_pos head = (get_branch head).pos
+ let new_node ?(id=Stateid.fresh ()) proof_mode () =
+ assert(Vcs_.get_info !vcs id = None);
+ vcs := set_info !vcs id (default_info proof_mode);
+ id
+ let merge id ~ours ?into branch =
+ vcs := merge !vcs id ~ours ~theirs:Noop ?into branch
+ let delete_branch branch = vcs := delete_branch !vcs branch
+ let reset_branch branch id = vcs := reset_branch !vcs branch id
+ let commit id t = vcs := commit !vcs id t
+ let rewrite_merge id ~ours ~at branch =
+ vcs := rewrite_merge !vcs id ~ours ~theirs:Noop ~at branch
+ let reachable id = reachable !vcs id
+ let mk_branch_name { expr = x } = Branch.make
+ (match Vernacprop.under_control x with
+ | VernacDefinition (_,({CAst.v=Name i},_),_) -> Id.to_string i
+ | VernacStartTheoremProof (_,[({CAst.v=i},_),_]) -> Id.to_string i
+ | _ -> "branch")
+ let edit_branch = Branch.make "edit"
+ let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind
+ let get_info id =
+ match get_info !vcs id with
+ | Some x -> x
+ | None -> raise Vcs_aux.Expired
+ let set_state id s =
+ let info = get_info id in
+ info.state <- s;
+ let is_full_state_valid = match s with
+ | FullState _ -> true
+ | EmptyState | ErrorState _ | ParsingState _ -> false
+ in
+ if async_proofs_is_master !cur_opt && is_full_state_valid then
+ Hooks.(call state_ready ~doc:dummy_doc (* XXX should be taken in input *) id)
+
+ let get_state id = (get_info id).state
+
+ let get_parsing_state id =
+ stm_pperr_endline (fun () -> str "retrieve parsing state state " ++ str (Stateid.to_string id) ++ str " }}}");
+ match (get_info id).state with
+ | FullState s -> Some s.Vernacstate.parsing
+ | ParsingState s -> Some s
+ | ErrorState (s,_) -> s
+ | EmptyState -> None
+
+ let set_parsing_state id ps =
+ let info = get_info id in
+ let new_state =
+ match info.state with
+ | FullState s -> assert false
+ | ParsingState s -> assert false
+ | ErrorState _ -> assert false
+ | EmptyState -> ParsingState ps
+ in
+ info.state <- new_state
+
+ let get_proof_mode id = (get_info id).proof_mode
+ let set_proof_mode id pm = (get_info id).proof_mode <- pm
+
+ let reached id =
+ let info = get_info id in
+ info.n_reached <- info.n_reached + 1
+ let goals id n = (get_info id).n_goals <- n
+ let cur_tip () = get_branch_pos (current_branch ())
+
+ let proof_nesting () = Vcs_aux.proof_nesting !vcs
+
+ let checkout_shallowest_proof_branch () =
+ if List.mem edit_branch (Vcs_.branches !vcs) then begin
+ checkout edit_branch
+ end else
+ let pl = proof_nesting () in
+ try
+ let branch = fst @@ Vcs_aux.find_proof_at_depth !vcs pl in
+ checkout branch
+ with Failure _ ->
+ checkout Branch.master
+
+ (* copies the transaction on every open branch *)
+ let propagate_sideff ~action =
+ List.map (fun b ->
+ checkout b;
+ let proof_mode = get_proof_mode @@ get_branch_pos b in
+ let id = new_node proof_mode () in
+ merge id ~ours:(Sideff action) ~into:b Branch.master;
+ id)
+ (List.filter (fun b -> not (Branch.equal b Branch.master)) (branches ()))
+
+ let propagate_qed () =
+ List.iter (fun b ->
+ checkout b;
+ let proof_mode = get_proof_mode @@ get_branch_pos b in
+ let id = new_node proof_mode () in
+ let parsing = Option.get @@ get_parsing_state (get_branch_pos b) in
+ merge id ~ours:(Sideff CherryPickEnv) ~into:b Branch.master;
+ set_parsing_state id parsing)
+ (List.filter (fun b -> not (Branch.equal b Branch.master)) (branches ()))
+
+ let visit id = Vcs_aux.visit !vcs id
+
+ let nodes_in_slice ~block_start ~block_stop =
+ let rec aux id =
+ if Stateid.equal id block_start then [] else
+ match visit id with
+ | { next = n; step = `Cmd x } -> (id,Cmd x) :: aux n
+ | { next = n; step = `Alias x } -> (id,Alias x) :: aux n
+ | { next = n; step = `Sideff (ReplayCommand x,_) } ->
+ (id,Sideff (ReplayCommand x)) :: aux n
+ | _ -> anomaly Pp.(str("Cannot slice from "^ Stateid.to_string block_start ^
+ " to "^Stateid.to_string block_stop^"."))
+ in aux block_stop
+
+ (* [slice] copies a slice of the DAG, keeping only the last known valid state.
+ When it copies a state, it drops the libobjects and keeps only the structure. *)
+ let slice ~block_start ~block_stop =
+ let l = nodes_in_slice ~block_start ~block_stop in
+ let copy_info v id =
+ let info = get_info id in
+ Vcs_.set_info v id
+ { info with state = EmptyState;
+ vcs_backup = None,None } in
+ let make_shallow = function
+ | FullState st -> FullState (Vernacstate.make_shallow st)
+ | x -> x
+ in
+ let copy_info_w_state v id =
+ let info = get_info id in
+ Vcs_.set_info v id { info with state = make_shallow info.state; vcs_backup = None,None } in
+ let copy_proof_blockes v =
+ let nodes = Vcs_.Dag.all_nodes (Vcs_.dag v) in
+ let props =
+ Stateid.Set.fold (fun n pl -> Vcs_.property_of !vcs n @ pl) nodes [] in
+ let props = CList.sort_uniquize Vcs_.Dag.Property.compare props in
+ List.fold_left (fun v p ->
+ Vcs_.create_property v
+ (Stateid.Set.elements (Vcs_.Dag.Property.having_it p))
+ (Vcs_.Dag.Property.data p)) v props
+ in
+ let v = Vcs_.empty block_start in
+ let v = copy_info v block_start in
+ let v = List.fold_right (fun (id,tr) v ->
+ let v = Vcs_.commit v id tr in
+ let v = copy_info v id in
+ v) l v in
+ (* Stm should have reached the beginning of proof *)
+ assert (match get_state block_start
+ with FullState _ -> true | _ -> false);
+ (* We put in the new dag the most recent state known to master *)
+ let rec fill id =
+ match get_state id with
+ | EmptyState | ErrorState _ | ParsingState _ -> fill (Vcs_aux.visit v id).next
+ | FullState _ -> copy_info_w_state v id
+ in
+ let v = fill block_stop in
+ (* We put in the new dag the first state (since Qed shall run on it,
+ * see check_task_aux) *)
+ let v = copy_info_w_state v block_start in
+ copy_proof_blockes v
+
+ let nodes_in_slice ~block_start ~block_stop =
+ List.rev (List.map fst (nodes_in_slice ~block_start ~block_stop))
+
+ let topo_invariant l =
+ let all = List.fold_right Stateid.Set.add l Stateid.Set.empty in
+ List.for_all
+ (fun x ->
+ let props = property_of !vcs x in
+ let sets = List.map Dag.Property.having_it props in
+ List.for_all (fun s -> Stateid.Set.(subset s all || subset all s)) sets)
+ l
+
+ let create_proof_task_box l ~qed ~block_start:lemma =
+ if not (topo_invariant l) then anomaly Pp.(str "overlapping boxes.");
+ vcs := create_property !vcs l (ProofTask { qed; lemma })
+ let create_proof_block ({ block_start; block_stop} as decl) name =
+ let l = nodes_in_slice ~block_start ~block_stop in
+ if not (topo_invariant l) then anomaly Pp.(str "overlapping boxes.");
+ vcs := create_property !vcs l (ProofBlock (decl, name))
+ let box_of id = List.map Dag.Property.data (property_of !vcs id)
+ let delete_boxes_of id =
+ List.iter (fun x -> vcs := delete_property !vcs x) (property_of !vcs id)
+ let proof_task_box_of id =
+ match
+ CList.map_filter (function ProofTask x -> Some x | _ -> None) (box_of id)
+ with
+ | [] -> None
+ | [x] -> Some x
+ | _ -> anomaly Pp.(str "node with more than 1 proof task box.")
+
+ let gc () =
+ let old_vcs = !vcs in
+ let new_vcs, erased_nodes = gc old_vcs in
+ Stateid.Set.iter (fun id ->
+ match (Vcs_aux.visit old_vcs id).step with
+ | `Qed ({ fproof = Some (_, cancel_switch) }, _)
+ | `Cmd { cqueue = `TacQueue (_,_,cancel_switch) }
+ | `Cmd { cqueue = `QueryQueue cancel_switch } ->
+ cancel_switch := true
+ | _ -> ())
+ erased_nodes;
+ vcs := new_vcs
+
+ module NB : sig (* Non blocking Sys.command *)
+
+ val command : now:bool -> (unit -> unit) -> unit
+
+ end = struct
+
+ let m = Mutex.create ()
+ let c = Condition.create ()
+ let job = ref None
+ let worker = ref None
+
+ let set_last_job j =
+ Mutex.lock m;
+ job := Some j;
+ Condition.signal c;
+ Mutex.unlock m
+
+ let get_last_job () =
+ Mutex.lock m;
+ while Option.is_empty !job do Condition.wait c m; done;
+ match !job with
+ | None -> assert false
+ | Some x -> job := None; Mutex.unlock m; x
+
+ let run_command () =
+ try while true do get_last_job () () done
+ with e -> () (* No failure *)
+
+ let command ~now job =
+ if now then job ()
+ else begin
+ set_last_job job;
+ if Option.is_empty !worker then
+ worker := Some (CThread.create run_command ())
+ end
+
+ end
+
+ let print ?(now=false) () =
+ if !Flags.debug then NB.command ~now (print_dag !vcs)
+
+ let backup () = !vcs
+ let restore v = vcs := v
+
+end (* }}} *)
+
+let state_of_id ~doc id =
+ try match VCS.get_state id with
+ | FullState s -> `Valid (Some s)
+ | ErrorState (_,(e,_)) -> `Error e
+ | EmptyState | ParsingState _ -> `Valid None
+ with VCS.Expired -> `Expired
+
+(****** A cache: fills in the nodes of the VCS document with their value ******)
+module State : sig
+
+ type t
+
+ val freeze : unit -> t
+ val unfreeze : t -> unit
+
+ (** The function is from unit, so it uses the current state to define
+ a new one. I.e. one may been to install the right state before
+ defining a new one.
+ Warning: an optimization in installed_cached requires that state
+ modifying functions are always executed using this wrapper. *)
+ val define :
+ doc:doc ->
+ ?safe_id:Stateid.t ->
+ ?redefine:bool -> ?cache:bool ->
+ ?feedback_processed:bool -> (unit -> unit) -> Stateid.t -> unit
+
+ val fix_exn_ref : (Exninfo.iexn -> Exninfo.iexn) ref
+
+ val install_cached : Stateid.t -> unit
+ (* val install_parsing_state : Stateid.t -> unit *)
+ val is_cached : ?cache:bool -> Stateid.t -> bool
+ val is_cached_and_valid : ?cache:bool -> Stateid.t -> bool
+
+ val exn_on : Stateid.t -> valid:Stateid.t -> Exninfo.iexn -> Exninfo.iexn
+
+ (* to send states across worker/master *)
+ val get_cached : Stateid.t -> Vernacstate.t
+ val same_env : Vernacstate.t -> Vernacstate.t -> bool
+
+ type proof_part
+
+ type partial_state =
+ [ `Full of Vernacstate.t
+ | `ProofOnly of Stateid.t * proof_part ]
+
+ val proof_part_of_frozen : Vernacstate.t -> proof_part
+ val assign : Stateid.t -> partial_state -> unit
+
+ (* Handlers for initial state, prior to document creation. *)
+ val register_root_state : unit -> unit
+ val restore_root_state : unit -> unit
+
+ val purify : ('a -> 'b) -> 'a -> 'b
+
+end = struct (* {{{ *)
+
+ type t = { id : Stateid.t; vernac_state : Vernacstate.t }
+
+ (* cur_id holds Stateid.dummy in case the last attempt to define a state
+ * failed, so the global state may contain garbage *)
+ let cur_id = ref Stateid.dummy
+ let fix_exn_ref = ref (fun x -> x)
+
+ let freeze () = { id = !cur_id; vernac_state = Vernacstate.freeze_interp_state ~marshallable:false }
+ let unfreeze st =
+ Vernacstate.unfreeze_interp_state st.vernac_state;
+ cur_id := st.id
+
+ let invalidate_cur_state () = cur_id := Stateid.dummy
+
+ type proof_part =
+ Proof_global.t option *
+ int * (* Evarutil.meta_counter_summary_tag *)
+ int * (* Evd.evar_counter_summary_tag *)
+ Obligations.program_info Names.Id.Map.t (* Obligations.program_tcc_summary_tag *)
+
+ type partial_state =
+ [ `Full of Vernacstate.t
+ | `ProofOnly of Stateid.t * proof_part ]
+
+ let proof_part_of_frozen { Vernacstate.proof; system } =
+ let st = States.summary_of_state system in
+ proof,
+ Summary.project_from_summary st Util.(pi1 summary_pstate),
+ Summary.project_from_summary st Util.(pi2 summary_pstate),
+ Summary.project_from_summary st Util.(pi3 summary_pstate)
+
+ let cache_state ~marshallable id =
+ VCS.set_state id (FullState (Vernacstate.freeze_interp_state ~marshallable))
+
+ let freeze_invalid id iexn =
+ let ps = VCS.get_parsing_state id in
+ VCS.set_state id (ErrorState (ps,iexn))
+
+ let is_cached ?(cache=false) id only_valid =
+ if Stateid.equal id !cur_id then
+ try match VCS.get_info id with
+ | ({ state = EmptyState } | { state = ParsingState _ }) when cache -> cache_state ~marshallable:false id; true
+ | _ -> true
+ with VCS.Expired -> false
+ else
+ try match VCS.get_state id with
+ | EmptyState | ParsingState _ -> false
+ | FullState _ -> true
+ | ErrorState _ -> not only_valid
+ with VCS.Expired -> false
+
+ let is_cached_and_valid ?cache id = is_cached ?cache id true
+ let is_cached ?cache id = is_cached ?cache id false
+
+ let install_cached id =
+ match VCS.get_state id with
+ | FullState s ->
+ Vernacstate.unfreeze_interp_state s;
+ cur_id := id
+
+ | ErrorState (_,ie) ->
+ Exninfo.iraise ie
+
+ | EmptyState | ParsingState _ ->
+ (* coqc has a 1 slot cache and only for valid states *)
+ if (VCS.is_interactive ()) || not (Stateid.equal id !cur_id) then
+ anomaly Pp.(str "installing a non cached state.")
+
+ (*
+ let install_parsing_state id =
+ if not (Stateid.equal id !cur_id) then begin
+ Vernacstate.Parser.install @@ VCS.get_parsing_state id
+ end
+ *)
+
+ let get_cached id =
+ try match VCS.get_state id with
+ | FullState s -> s
+ | _ -> anomaly Pp.(str "not a cached state.")
+ with VCS.Expired -> anomaly Pp.(str "not a cached state (expired).")
+
+ let assign id what =
+ let open Vernacstate in
+ if VCS.get_state id <> EmptyState then () else
+ try match what with
+ | `Full s ->
+ let s =
+ try
+ let prev = (VCS.visit id).next in
+ if is_cached_and_valid prev
+ then { s with proof =
+ Vernacstate.Proof_global.copy_terminators
+ ~src:((get_cached prev).proof) ~tgt:s.proof }
+ else s
+ with VCS.Expired -> s in
+ VCS.set_state id (FullState s)
+ | `ProofOnly(ontop,(pstate,c1,c2,c3)) ->
+ if is_cached_and_valid ontop then
+ let s = get_cached ontop in
+ let s = { s with proof =
+ Vernacstate.Proof_global.copy_terminators ~src:s.proof ~tgt:pstate } in
+ let s = { s with system =
+ States.replace_summary s.system
+ begin
+ let st = States.summary_of_state s.system in
+ let st = Summary.modify_summary st Util.(pi1 summary_pstate) c1 in
+ let st = Summary.modify_summary st Util.(pi2 summary_pstate) c2 in
+ let st = Summary.modify_summary st Util.(pi3 summary_pstate) c3 in
+ st
+ end
+ } in
+ VCS.set_state id (FullState s)
+ with VCS.Expired -> ()
+
+ let exn_on id ~valid (e, info) =
+ match Stateid.get info with
+ | Some _ -> (e, info)
+ | None ->
+ let loc = Loc.get_loc info in
+ let (e, info) = Hooks.(call_process_error_once (e, info)) in
+ execution_error ?loc id (iprint (e, info));
+ (e, Stateid.add info ~valid id)
+
+ let same_env { Vernacstate.system = s1 } { Vernacstate.system = s2 } =
+ let s1 = States.summary_of_state s1 in
+ let e1 = Summary.project_from_summary s1 Global.global_env_summary_tag in
+ let s2 = States.summary_of_state s2 in
+ let e2 = Summary.project_from_summary s2 Global.global_env_summary_tag in
+ e1 == e2
+
+ (* [define] puts the system in state [id] calling [f ()] *)
+ (* [safe_id] is the last known valid state before execution *)
+ let define ~doc ?safe_id ?(redefine=false) ?(cache=false) ?(feedback_processed=true)
+ f id
+ =
+ feedback ~id:id (ProcessingIn !Flags.async_proofs_worker_id);
+ let str_id = Stateid.to_string id in
+ if is_cached id && not redefine then
+ anomaly Pp.(str"defining state "++str str_id++str" twice.");
+ try
+ stm_prerr_endline (fun () -> "defining "^str_id^" (cache="^
+ if cache then "Y)" else "N)");
+ let good_id = match safe_id with None -> !cur_id | Some id -> id in
+ fix_exn_ref := exn_on id ~valid:good_id;
+ f ();
+ fix_exn_ref := (fun x -> x);
+ if cache then cache_state ~marshallable:false id;
+ stm_prerr_endline (fun () -> "setting cur id to "^str_id);
+ cur_id := id;
+ if feedback_processed then
+ Hooks.(call state_computed ~doc id ~in_cache:false);
+ VCS.reached id;
+ if Vernacstate.Proof_global.there_are_pending_proofs () then
+ VCS.goals id (Vernacstate.Proof_global.get_open_goals ())
+ with e ->
+ let (e, info) = CErrors.push e in
+ let good_id = !cur_id in
+ invalidate_cur_state ();
+ VCS.reached id;
+ let ie =
+ match Stateid.get info, safe_id with
+ | None, None -> (exn_on id ~valid:good_id (e, info))
+ | None, Some good_id -> (exn_on id ~valid:good_id (e, info))
+ | Some _, None -> (e, info)
+ | Some (_,at), Some id -> (e, Stateid.add info ~valid:id at) in
+ if cache then freeze_invalid id ie;
+ Hooks.(call unreachable_state ~doc id ie);
+ Exninfo.iraise ie
+
+ let init_state = ref None
+
+ let register_root_state () =
+ init_state := Some (Vernacstate.freeze_interp_state ~marshallable:false)
+
+ let restore_root_state () =
+ cur_id := Stateid.dummy;
+ Vernacstate.unfreeze_interp_state (Option.get !init_state)
+
+ (* Protect against state changes *)
+ let purify f x =
+ let st = freeze () in
+ try
+ let res = f x in
+ Vernacstate.invalidate_cache ();
+ unfreeze st;
+ res
+ with e ->
+ let e = CErrors.push e in
+ Vernacstate.invalidate_cache ();
+ unfreeze st;
+ Exninfo.iraise e
+
+end (* }}} *)
+
+(* indentation code for Show Script, initially contributed
+ * by D. de Rauglaudre. Should be moved away.
+ *)
+
+module ShowScript = struct
+
+let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) =
+ (* ng1 : number of goals remaining at the current level (before cmd)
+ ngl1 : stack of previous levels with their remaining goals
+ ng : number of goals after the execution of cmd
+ beginend : special indentation stack for { } *)
+ let ngprev = List.fold_left (+) ng1 ngl1 in
+ let new_ngl =
+ if ng > ngprev then
+ (* We've branched *)
+ (ng - ngprev + 1, ng1 - 1 :: ngl1)
+ else if ng < ngprev then
+ (* A subgoal have been solved. Let's compute the new current level
+ by discarding all levels with 0 remaining goals. *)
+ let rec loop = function
+ | (0, ng2::ngl2) -> loop (ng2,ngl2)
+ | p -> p
+ in loop (ng1-1, ngl1)
+ else
+ (* Standard case, same goal number as before *)
+ (ng1, ngl1)
+ in
+ (* When a subgoal have been solved, separate this block by an empty line *)
+ let new_nl = (ng < ngprev)
+ in
+ (* Indentation depth *)
+ let ind = List.length ngl1
+ in
+ (* Some special handling of bullets and { }, to get a nicer display *)
+ let pred n = max 0 (n-1) in
+ let ind, nl, new_beginend = match Vernacprop.under_control cmd with
+ | VernacSubproof _ -> pred ind, nl, (pred ind)::beginend
+ | VernacEndSubproof -> List.hd beginend, false, List.tl beginend
+ | VernacBullet _ -> pred ind, nl, beginend
+ | _ -> ind, nl, beginend
+ in
+ let pp = Pp.(
+ (if nl then fnl () else mt ()) ++
+ (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd)))
+ in
+ (new_ngl, new_nl, new_beginend, pp :: ppl)
+
+let get_script prf =
+ let branch, test =
+ match prf with
+ | None -> VCS.Branch.master, fun _ -> true
+ | Some name -> VCS.current_branch (),fun nl -> nl=[] || List.mem name nl in
+ let rec find acc id =
+ if Stateid.equal id Stateid.initial ||
+ Stateid.equal id Stateid.dummy then acc else
+ let view = VCS.visit id in
+ match view.step with
+ | `Fork((_,_,_,ns), _) when test ns -> acc
+ | `Qed (qed, proof) -> find [qed.qast.expr, (VCS.get_info id).n_goals] proof
+ | `Sideff (ReplayCommand x,_) ->
+ find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next
+ | `Sideff (CherryPickEnv, id) -> find acc id
+ | `Cmd {cast = x; ctac} when ctac -> (* skip non-tactics *)
+ find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next
+ | `Cmd _ -> find acc view.next
+ | `Alias (id,_) -> find acc id
+ | `Fork _ -> find acc view.next
+ in
+ find [] (VCS.get_branch_pos branch)
+
+let warn_show_script_deprecated =
+ CWarnings.create ~name:"deprecated-show-script" ~category:"deprecated"
+ (fun () -> Pp.str "The “Show Script” command is deprecated.")
+
+let show_script ?proof () =
+ warn_show_script_deprecated ();
+ try
+ let prf =
+ try match proof with
+ | None -> Some (Vernacstate.Proof_global.get_current_proof_name ())
+ | Some (p,_) -> Some (p.Proof_global.id)
+ with Vernacstate.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 Pp.(v 0 (prlist_with_sep fnl (fun x -> x) indented_cmds))
+ with Vcs_aux.Expired -> ()
+
+end
+
+(* Wrapper for Vernacentries.interp to set the feedback id *)
+(* It is currently called 19 times, this number should be certainly
+ reduced... *)
+let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t =
+ (* The Stm will gain the capability to interpret commmads affecting
+ the whole document state, such as backtrack, etc... so we start
+ to design the stm command interpreter now *)
+ set_id_for_feedback ?route dummy_doc id;
+ Aux_file.record_in_aux_set_at ?loc ();
+ (* We need to check if a command should be filtered from
+ * vernac_entries, as it cannot handle it. This should go away in
+ * future refactorings.
+ *)
+ let is_filtered_command = function
+ | VernacResetName _ | VernacResetInitial | VernacBack _
+ | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
+ | VernacAbortAll | VernacAbort _ -> true
+ | _ -> false
+ in
+ let aux_interp st expr =
+ (* XXX unsupported attributes *)
+ let cmd = Vernacprop.under_control expr in
+ if is_filtered_command cmd then
+ (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st)
+ else
+ match cmd with
+ | VernacShow ShowScript -> ShowScript.show_script (); st (* XX we are ignoring control here *)
+ | _ ->
+ stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr);
+ try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st (CAst.make ?loc expr)
+ with e ->
+ let e = CErrors.push e in
+ Exninfo.iraise Hooks.(call_process_error_once e)
+ in aux_interp st expr
+
+(****************************** CRUFT *****************************************)
+(******************************************************************************)
+
+(* The backtrack module simulates the classic behavior of a linear document *)
+module Backtrack : sig
+
+ val record : unit -> unit
+
+ (* we could navigate the dag, but this ways easy *)
+ val branches_of : Stateid.t -> backup
+
+ (* Returns the state that the command should backtract to *)
+ val undo_vernac_classifier : vernac_control -> doc:doc -> Stateid.t
+ val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option
+
+end = struct (* {{{ *)
+
+ let record () =
+ List.iter (fun current_branch ->
+ let mine = current_branch, VCS.get_branch current_branch in
+ let info = VCS.get_info (VCS.get_branch_pos current_branch) in
+ let others =
+ CList.map_filter (fun b ->
+ if Vcs_.Branch.equal b current_branch then None
+ else Some(b, VCS.get_branch b)) (VCS.branches ()) in
+ let backup = if fst info.vcs_backup <> None then fst info.vcs_backup
+ else Some (VCS.backup ()) in
+ let branches = if snd info.vcs_backup <> None then snd info.vcs_backup
+ else Some { mine; others } in
+ info.vcs_backup <- backup, branches)
+ [VCS.current_branch (); VCS.Branch.master]
+
+ let branches_of id =
+ let info = VCS.get_info id in
+ match info.vcs_backup with
+ | _, None ->
+ anomaly Pp.(str"Backtrack.branches_of "++str(Stateid.to_string id)++
+ str": a state with no vcs_backup.")
+ | _, Some x -> x
+
+ let rec fold_until f acc id =
+ let next acc =
+ if id = Stateid.initial then raise Not_found
+ else fold_until f acc (VCS.visit id).next in
+ let info = VCS.get_info id in
+ match info.vcs_backup with
+ | None, _ -> next acc
+ | Some vcs, _ ->
+ let ids, tactic, undo =
+ if id = Stateid.initial || id = Stateid.dummy then [],false,0 else
+ match VCS.visit id with
+ | { step = `Fork ((_,_,_,l),_) } -> l, false,0
+ | { step = `Cmd { cids = l; ctac } } -> l, ctac,0
+ | { step = `Alias (_,{ expr }) } when not (Vernacprop.has_Fail expr) ->
+ begin match Vernacprop.under_control expr with
+ | VernacUndo n -> [], false, n
+ | _ -> [],false,0
+ end
+ | _ -> [],false,0 in
+ match f acc (id, vcs, ids, tactic, undo) with
+ | `Stop x -> x
+ | `Cont acc -> next acc
+
+ let undo_costly_in_batch_mode =
+ CWarnings.create ~name:"undo-batch-mode" ~category:"non-interactive" Pp.(fun v ->
+ str "Command " ++ Ppvernac.pr_vernac v ++
+ str (" is not recommended in batch mode. In particular, going back in the document" ^
+ " is not efficient in batch mode due to Coq not caching previous states for memory optimization reasons." ^
+ " If your use is intentional, you may want to disable this warning and pass" ^
+ " the \"-async-proofs-cache force\" option to Coq."))
+
+ let back_tactic n (id,_,_,tactic,undo) =
+ let value = (if tactic then 1 else 0) - undo in
+ if Int.equal n 0 then `Stop id else `Cont (n-value)
+
+ let get_proof ~doc id =
+ match state_of_id ~doc id with
+ | `Valid (Some vstate) -> Option.map Proof_global.give_me_the_proof vstate.Vernacstate.proof
+ | _ -> None
+
+ let undo_vernac_classifier v ~doc =
+ if not (VCS.is_interactive ()) && !cur_opt.async_proofs_cache <> Some Force
+ then undo_costly_in_batch_mode v;
+ try
+ match Vernacprop.under_control v with
+ | VernacResetInitial ->
+ Stateid.initial
+ | VernacResetName {CAst.v=name} ->
+ let id = VCS.cur_tip () in
+ (try
+ let oid =
+ fold_until (fun b (id,_,label,_,_) ->
+ if b then `Stop id else `Cont (List.mem name label))
+ false id in
+ oid
+ with Not_found ->
+ id)
+ | VernacBack n ->
+ let id = VCS.cur_tip () in
+ let oid = fold_until (fun n (id,_,_,_,_) ->
+ if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in
+ oid
+ | VernacUndo n ->
+ let id = VCS.cur_tip () in
+ let oid = fold_until back_tactic n id in
+ oid
+ | VernacUndoTo _
+ | VernacRestart as e ->
+ let m = match e with VernacUndoTo m -> m | _ -> 0 in
+ let id = VCS.cur_tip () in
+ let vcs =
+ match (VCS.get_info id).vcs_backup with
+ | None, _ -> anomaly Pp.(str"Backtrack: tip with no vcs_backup.")
+ | Some vcs, _ -> vcs in
+ let cb, _ =
+ try Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs)
+ with Failure _ -> raise Vernacstate.Proof_global.NoCurrentProof in
+ let n = fold_until (fun n (_,vcs,_,_,_) ->
+ if List.mem cb (Vcs_.branches vcs) then `Cont (n+1) else `Stop n)
+ 0 id in
+ let oid = fold_until (fun n (id,_,_,_,_) ->
+ if Int.equal n 0 then `Stop id else `Cont (n-1)) (n-m-1) id in
+ oid
+ | VernacAbortAll ->
+ let id = VCS.cur_tip () in
+ let oid = fold_until (fun () (id,vcs,_,_,_) ->
+ match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ())
+ () id in
+ oid
+ | VernacBackTo id ->
+ Stateid.of_int id
+ | _ -> anomaly Pp.(str "incorrect VtMeta classification")
+ with
+ | Not_found ->
+ CErrors.user_err ~hdr:"undo_vernac_classifier"
+ Pp.(str "Cannot undo")
+
+ let get_prev_proof ~doc id =
+ try
+ let np = get_proof ~doc id in
+ match np with
+ | None -> None
+ | Some cp ->
+ let did = ref id in
+ let rv = ref np in
+ let done_ = ref false in
+ while not !done_ do
+ did := fold_until back_tactic 1 !did;
+ rv := get_proof ~doc !did;
+ done_ := match !rv with
+ | Some rv -> not (Goal.Set.equal (Proof.all_goals rv) (Proof.all_goals cp))
+ | None -> true
+ done;
+ !rv
+ with Not_found | Vernacstate.Proof_global.NoCurrentProof -> None
+
+end (* }}} *)
+
+let get_prev_proof = Backtrack.get_prev_proof
+
+let hints = ref Aux_file.empty_aux_file
+let set_compilation_hints file =
+ hints := Aux_file.load_aux_file_for file
+
+let get_hint_ctx loc =
+ let s = Aux_file.get ?loc !hints "context_used" in
+ let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") s) in
+ let ids = List.map (fun id -> CAst.make id) ids in
+ match ids with
+ | [] -> SsEmpty
+ | x :: xs ->
+ List.fold_left (fun a x -> SsUnion (SsSingl x,a)) (SsSingl x) xs
+
+let get_hint_bp_time proof_name =
+ try float_of_string (Aux_file.get !hints proof_name)
+ with Not_found -> 1.0
+
+let record_pb_time ?loc proof_name time =
+ let proof_build_time = Printf.sprintf "%.3f" time in
+ Aux_file.record_in_aux_at ?loc "proof_build_time" proof_build_time;
+ if proof_name <> "" then begin
+ Aux_file.record_in_aux_at proof_name proof_build_time;
+ hints := Aux_file.set !hints proof_name proof_build_time
+ end
+
+exception RemoteException of Pp.t
+let _ = CErrors.register_handler (function
+ | RemoteException ppcmd -> ppcmd
+ | _ -> raise Unhandled)
+
+(****************** proof structure for error recovery ************************)
+(******************************************************************************)
+
+type document_node = {
+ indentation : int;
+ ast : Vernacexpr.vernac_control;
+ id : Stateid.t;
+}
+
+type document_view = {
+ entry_point : document_node;
+ prev_node : document_node -> document_node option;
+}
+
+type static_block_detection =
+ document_view -> static_block_declaration option
+
+type recovery_action = {
+ base_state : Stateid.t;
+ goals_to_admit : Goal.goal list;
+ recovery_command : Vernacexpr.vernac_control option;
+}
+
+type dynamic_block_error_recovery =
+ doc -> static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ]
+
+let proof_block_delimiters = ref []
+
+let register_proof_block_delimiter name static dynamic =
+ if List.mem_assoc name !proof_block_delimiters then
+ CErrors.user_err ~hdr:"STM" Pp.(str "Duplicate block delimiter " ++ str name);
+ proof_block_delimiters := (name, (static,dynamic)) :: !proof_block_delimiters
+
+let mk_doc_node id = function
+ | { step = `Cmd { ctac; cast = { indentation; expr }}; next } when ctac ->
+ Some { indentation; ast = expr; id }
+ | { step = `Sideff (ReplayCommand { indentation; expr }, _); next } ->
+ Some { indentation; ast = expr; id }
+ | _ -> None
+let prev_node { id } =
+ let id = (VCS.visit id).next in
+ mk_doc_node id (VCS.visit id)
+let cur_node id = mk_doc_node id (VCS.visit id)
+
+let is_block_name_enabled name =
+ match !cur_opt.async_proofs_tac_error_resilience with
+ | `None -> false
+ | `All -> true
+ | `Only l -> List.mem name l
+
+let detect_proof_block id name =
+ let name = match name with None -> "indent" | Some x -> x in
+ if is_block_name_enabled name &&
+ (async_proofs_is_master !cur_opt || Flags.async_proofs_is_worker ())
+ then (
+ match cur_node id with
+ | None -> ()
+ | Some entry_point -> try
+ let static, _ = List.assoc name !proof_block_delimiters in
+ begin match static { prev_node; entry_point } with
+ | None -> ()
+ | Some ({ block_start; block_stop } as decl) ->
+ VCS.create_proof_block decl name
+ end
+ with Not_found ->
+ CErrors.user_err ~hdr:"STM"
+ Pp.(str "Unknown proof block delimiter " ++ str name)
+ )
+(****************************** THE SCHEDULER *********************************)
+(******************************************************************************)
+
+(* Unused module warning doesn't understand [module rec] *)
+[@@@ocaml.warning "-60"]
+module rec ProofTask : sig
+
+ type competence = Stateid.t list
+ type task_build_proof = {
+ t_exn_info : Stateid.t * Stateid.t;
+ t_start : Stateid.t;
+ t_stop : Stateid.t;
+ t_drop : bool;
+ t_states : competence;
+ t_assign : Proof_global.closed_proof_output Future.assignment -> unit;
+ t_loc : Loc.t option;
+ t_uuid : Future.UUID.t;
+ t_name : string }
+
+ type task =
+ | BuildProof of task_build_proof
+ | States of Stateid.t list
+
+ type request =
+ | ReqBuildProof of (Future.UUID.t,VCS.vcs) Stateid.request * bool * competence
+ | ReqStates of Stateid.t list
+
+ include AsyncTaskQueue.Task
+ with type task := task
+ and type competence := competence
+ and type request := request
+
+ val build_proof_here :
+ doc:doc ->
+ ?loc:Loc.t ->
+ drop_pt:bool ->
+ Stateid.t * Stateid.t -> Stateid.t ->
+ Proof_global.closed_proof_output Future.computation
+
+ (* If set, only tasks overlapping with this list are processed *)
+ val set_perspective : Stateid.t list -> unit
+
+end = struct (* {{{ *)
+
+ let forward_feedback msg = Hooks.(call forward_feedback msg)
+
+ type competence = Stateid.t list
+ type task_build_proof = {
+ t_exn_info : Stateid.t * Stateid.t;
+ t_start : Stateid.t;
+ t_stop : Stateid.t;
+ t_drop : bool;
+ t_states : competence;
+ t_assign : Proof_global.closed_proof_output Future.assignment -> unit;
+ t_loc : Loc.t option;
+ t_uuid : Future.UUID.t;
+ t_name : string }
+
+ type task =
+ | BuildProof of task_build_proof
+ | States of Stateid.t list
+
+ type worker_status = Fresh | Old of competence
+
+ type request =
+ | ReqBuildProof of (Future.UUID.t,VCS.vcs) Stateid.request * bool * competence
+ | ReqStates of Stateid.t list
+
+ type error = {
+ e_error_at : Stateid.t;
+ e_safe_id : Stateid.t;
+ e_msg : Pp.t;
+ e_safe_states : Stateid.t list }
+
+ type response =
+ | RespBuiltProof of Proof_global.closed_proof_output * float
+ | RespError of error
+ | RespStates of (Stateid.t * State.partial_state) list
+
+ let name = ref "proofworker"
+ let extra_env () = !async_proofs_workers_extra_env
+
+ let perspective = ref []
+ let set_perspective l = perspective := l
+
+ let is_inside_perspective st = true
+ (* This code is now disabled. If an IDE needs this feature, make it accessible again.
+ List.exists (fun x -> CList.mem_f Stateid.equal x !perspective) st
+ *)
+
+ let task_match age t =
+ match age, t with
+ | Fresh, BuildProof { t_states } -> is_inside_perspective t_states
+ | Old my_states, States l ->
+ List.for_all (fun x -> CList.mem_f Stateid.equal x my_states) l
+ | _ -> false
+
+ let name_of_task = function
+ | BuildProof t -> "proof: " ^ t.t_name
+ | States l -> "states: " ^ String.concat "," (List.map Stateid.to_string l)
+ let name_of_request = function
+ | ReqBuildProof(r,_,_) -> "proof: " ^ r.Stateid.name
+ | ReqStates l -> "states: "^String.concat "," (List.map Stateid.to_string l)
+
+ let request_of_task age = function
+ | States l -> Some (ReqStates l)
+ | BuildProof {
+ t_exn_info;t_start;t_stop;t_loc;t_uuid;t_name;t_states;t_drop
+ } ->
+ assert(age = Fresh);
+ try Some (ReqBuildProof ({
+ Stateid.exn_info = t_exn_info;
+ stop = t_stop;
+ document = VCS.slice ~block_start:t_start ~block_stop:t_stop;
+ loc = t_loc;
+ uuid = t_uuid;
+ name = t_name }, t_drop, t_states))
+ with VCS.Expired -> None
+
+ let use_response (s : worker_status) t r =
+ match s, t, r with
+ | Old c, States _, RespStates l ->
+ List.iter (fun (id,s) -> State.assign id s) l; `End
+ | Fresh, BuildProof { t_assign; t_loc; t_name; t_states; t_drop },
+ RespBuiltProof (pl, time) ->
+ feedback (InProgress ~-1);
+ t_assign (`Val pl);
+ record_pb_time ?loc:t_loc t_name time;
+ if t_drop then `Stay(t_states,[States t_states])
+ else `End
+ | Fresh, BuildProof { t_assign; t_loc; t_name; t_states },
+ RespError { e_error_at; e_safe_id = valid; e_msg; e_safe_states } ->
+ feedback (InProgress ~-1);
+ let info = Stateid.add ~valid Exninfo.null e_error_at in
+ let e = (RemoteException e_msg, info) in
+ t_assign (`Exn e);
+ `Stay(t_states,[States e_safe_states])
+ | _ -> assert false
+
+ let on_task_cancellation_or_expiration_or_slave_death = function
+ | None -> ()
+ | Some (States _) -> ()
+ | Some (BuildProof { t_start = start; t_assign }) ->
+ let s = "Worker dies or task expired" in
+ let info = Stateid.add ~valid:start Exninfo.null start in
+ let e = (RemoteException (Pp.strbrk s), info) in
+ t_assign (`Exn e);
+ execution_error start (Pp.strbrk s);
+ feedback (InProgress ~-1)
+
+ let build_proof_here ~doc ?loc ~drop_pt (id,valid) eop =
+ Future.create (State.exn_on id ~valid) (fun () ->
+ let wall_clock1 = Unix.gettimeofday () in
+ Reach.known_state ~doc ~cache:(VCS.is_interactive ()) eop;
+ let wall_clock2 = Unix.gettimeofday () in
+ Aux_file.record_in_aux_at ?loc "proof_build_time"
+ (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
+ let p = Vernacstate.Proof_global.return_proof ~allow_partial:drop_pt () in
+ if drop_pt then feedback ~id Complete;
+ p)
+
+ let perform_buildp { Stateid.exn_info; stop; document; loc } drop my_states =
+ try
+ VCS.restore document;
+ VCS.print ();
+ let proof, future_proof, time =
+ let wall_clock = Unix.gettimeofday () in
+ let fp = build_proof_here ~doc:dummy_doc (* XXX should be document *) ?loc ~drop_pt:drop exn_info stop in
+ let proof = Future.force fp in
+ proof, fp, Unix.gettimeofday () -. wall_clock in
+ (* We typecheck the proof with the kernel (in the worker) to spot
+ * the few errors tactics don't catch, like the "fix" tactic building
+ * a bad fixpoint *)
+ let fix_exn = Future.fix_exn_of future_proof in
+ (* STATE: We use the current installed imperative state *)
+ let st = State.freeze () in
+ if not drop then begin
+ let checked_proof = Future.chain future_proof (fun p ->
+ let opaque = Proof_global.Opaque in
+
+ (* Unfortunately close_future_proof and friends are not pure so we need
+ to set the state manually here *)
+ State.unfreeze st;
+ let pobject, _ =
+ Vernacstate.Proof_global.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in
+ let terminator = (* The one sent by master is an InvalidKey *)
+ Lemmas.(standard_proof_terminator []) in
+
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
+ stm_vernac_interp stop
+ ~proof:(pobject, terminator) st
+ { verbose = false; loc; indentation = 0; strlen = 0;
+ expr = VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in
+ ignore(Future.join checked_proof);
+ end;
+ (* STATE: Restore the state XXX: handle exn *)
+ State.unfreeze st;
+ RespBuiltProof(proof,time)
+ with
+ | e when CErrors.noncritical e || e = Stack_overflow ->
+ let (e, info) = CErrors.push e in
+ (* This can happen if the proof is broken. The error has also been
+ * signalled as a feedback, hence we can silently recover *)
+ let e_error_at, e_safe_id = match Stateid.get info with
+ | Some (safe, err) -> err, safe
+ | None -> Stateid.dummy, Stateid.dummy in
+ let e_msg = iprint (e, info) in
+ stm_pperr_endline Pp.(fun () -> str "failed with the following exception: " ++ fnl () ++ e_msg);
+ let e_safe_states = List.filter State.is_cached_and_valid my_states in
+ RespError { e_error_at; e_safe_id; e_msg; e_safe_states }
+
+ let perform_states query =
+ if query = [] then [] else
+ let is_tac e = match Vernac_classifier.classify_vernac e with
+ | VtProofStep _, _ -> true
+ | _ -> false
+ in
+ let initial =
+ let rec aux id =
+ try match VCS.visit id with { next } -> aux next
+ with VCS.Expired -> id in
+ aux (List.hd query) in
+ let get_state seen id =
+ let prev =
+ try
+ let { next = prev; step } = VCS.visit id in
+ if State.is_cached_and_valid prev && List.mem prev seen
+ then Some (prev, State.get_cached prev, step)
+ else None
+ with VCS.Expired -> None in
+ let this =
+ if State.is_cached_and_valid id then Some (State.get_cached id) else None in
+ match prev, this with
+ | _, None -> None
+ | Some (prev, o, `Cmd { cast = { expr }}), Some n
+ when is_tac expr && State.same_env o n -> (* A pure tactic *)
+ Some (id, `ProofOnly (prev, State.proof_part_of_frozen n))
+ | Some _, Some s ->
+ if !Flags.debug then msg_debug (Pp.str "STM: sending back a fat state");
+ Some (id, `Full s)
+ | _, Some s -> Some (id, `Full s) in
+ let rec aux seen = function
+ | [] -> []
+ | id :: rest ->
+ match get_state seen id with
+ | None -> aux seen rest
+ | Some stuff -> stuff :: aux (id :: seen) rest in
+ aux [initial] query
+
+ let perform = function
+ | ReqBuildProof (bp,drop,states) -> perform_buildp bp drop states
+ | ReqStates sl -> RespStates (perform_states sl)
+
+ let on_marshal_error s = function
+ | States _ ->
+ msg_warning Pp.(strbrk("Marshalling error: "^s^". "^
+ "The system state could not be sent to the master process."))
+ | BuildProof { t_exn_info; t_stop; t_assign; t_loc; t_drop = drop_pt } ->
+ msg_warning Pp.(strbrk("Marshalling error: "^s^". "^
+ "The system state could not be sent to the worker process. "^
+ "Falling back to local, lazy, evaluation."));
+ t_assign(`Comp(build_proof_here ~doc:dummy_doc (* XXX should be stored in a closure, it is the same doc that was used to generate the task *) ?loc:t_loc ~drop_pt t_exn_info t_stop));
+ feedback (InProgress ~-1)
+
+end (* }}} *)
+
+(* Slave processes (if initialized, otherwise local lazy evaluation) *)
+and Slaves : sig
+
+ (* (eventually) remote calls *)
+ val build_proof :
+ doc:doc ->
+ ?loc:Loc.t -> drop_pt:bool ->
+ exn_info:(Stateid.t * Stateid.t) -> block_start:Stateid.t -> block_stop:Stateid.t ->
+ name:string -> future_proof * AsyncTaskQueue.cancel_switch
+
+ (* blocking function that waits for the task queue to be empty *)
+ val wait_all_done : unit -> unit
+
+ (* initialize the whole machinery (optional) *)
+ val init : unit -> unit
+
+ type 'a tasks = (('a,VCS.vcs) Stateid.request * bool) list
+ val dump_snapshot : unit -> Future.UUID.t tasks
+ val check_task : string -> int tasks -> int -> bool
+ val info_tasks : 'a tasks -> (string * float * int) list
+ val finish_task :
+ string ->
+ Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs ->
+ int tasks -> int -> Library.seg_univ
+
+ val cancel_worker : WorkerPool.worker_id -> unit
+
+ val reset_task_queue : unit -> unit
+
+ val set_perspective : Stateid.t list -> unit
+
+end = struct (* {{{ *)
+
+ module TaskQueue = AsyncTaskQueue.MakeQueue(ProofTask) ()
+
+ let queue = ref None
+ let init () =
+ if async_proofs_is_master !cur_opt then
+ queue := Some (TaskQueue.create !cur_opt.async_proofs_n_workers)
+ else
+ queue := Some (TaskQueue.create 0)
+
+ let check_task_aux extra name l i =
+ let { Stateid.stop; document; loc; name = r_name }, drop = List.nth l i in
+ Flags.if_verbose msg_info
+ Pp.(str(Printf.sprintf "Checking task %d (%s%s) of %s" i r_name extra name));
+ VCS.restore document;
+ let start =
+ let rec aux cur =
+ try aux (VCS.visit cur).next
+ with VCS.Expired -> cur in
+ aux stop in
+ try
+ Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:false stop;
+ if drop then
+ let _proof = Vernacstate.Proof_global.return_proof ~allow_partial:true () in
+ `OK_ADMITTED
+ else begin
+ (* The original terminator, a hook, has not been saved in the .vio*)
+ Vernacstate.Proof_global.set_terminator (Lemmas.standard_proof_terminator []);
+
+ let opaque = Proof_global.Opaque in
+ let proof =
+ Vernacstate.Proof_global.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in
+ (* We jump at the beginning since the kernel handles side effects by also
+ * looking at the ones that happen to be present in the current env *)
+ Reach.known_state ~doc:dummy_doc (* XXX should be document *) ~cache:false start;
+ (* STATE SPEC:
+ * - start: First non-expired state! [This looks very fishy]
+ * - end : start + qed
+ * => takes nothing from the itermediate states.
+ *)
+ (* STATE We use the state resulting from reaching start. *)
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
+ ignore(stm_vernac_interp stop ~proof st
+ { verbose = false; loc; indentation = 0; strlen = 0;
+ expr = VernacExpr ([], VernacEndProof (Proved (opaque,None))) });
+ `OK proof
+ end
+ with e ->
+ let (e, info) = CErrors.push e in
+ (try match Stateid.get info with
+ | None ->
+ msg_warning Pp.(
+ str"File " ++ str name ++ str ": proof of " ++ str r_name ++
+ spc () ++ iprint (e, info))
+ | Some (_, cur) ->
+ match VCS.visit cur with
+ | { step = `Cmd { cast = { loc } } }
+ | { step = `Fork (( { loc }, _, _, _), _) }
+ | { step = `Qed ( { qast = { loc } }, _) }
+ | { step = `Sideff (ReplayCommand { loc }, _) } ->
+ let start, stop = Option.cata Loc.unloc (0,0) loc in
+ msg_warning Pp.(
+ str"File " ++ str name ++ str ": proof of " ++ str r_name ++
+ str ": chars " ++ int start ++ str "-" ++ int stop ++
+ spc () ++ iprint (e, info))
+ | _ ->
+ msg_warning Pp.(
+ str"File " ++ str name ++ str ": proof of " ++ str r_name ++
+ spc () ++ iprint (e, info))
+ with e ->
+ msg_warning Pp.(str"unable to print error message: " ++
+ str (Printexc.to_string e)));
+ if drop then `ERROR_ADMITTED else `ERROR
+
+ let finish_task name (u,cst,_) d p l i =
+ let { Stateid.uuid = bucket }, drop = List.nth l i in
+ let bucket_name =
+ if bucket < 0 then (assert drop; ", no bucket")
+ else Printf.sprintf ", bucket %d" bucket in
+ match check_task_aux bucket_name name l i with
+ | `ERROR -> exit 1
+ | `ERROR_ADMITTED -> u, cst, false
+ | `OK_ADMITTED -> u, cst, false
+ | `OK (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
+ (* We only manipulate monomorphic terms here. *)
+ let map (c, ctx) = assert (Univ.AUContext.is_empty ctx); c in
+ let pr =
+ Future.from_val (map (Option.get (Global.body_of_constant_body c))) in
+ let uc =
+ Future.chain uc Univ.hcons_universe_context_set in
+ let pr = Future.chain pr discharge in
+ let pr = Future.chain 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
+ | `OK _ | `OK_ADMITTED -> true
+ | `ERROR | `ERROR_ADMITTED -> false
+
+ let info_tasks l =
+ CList.map_i (fun i ({ Stateid.loc; name }, _) ->
+ let time1 =
+ try float_of_string (Aux_file.get ?loc !hints "proof_build_time")
+ with Not_found -> 0.0 in
+ let time2 =
+ try float_of_string (Aux_file.get ?loc !hints "proof_check_time")
+ with Not_found -> 0.0 in
+ name, max (time1 +. time2) 0.0001,i) 0 l
+
+ let set_perspective idl =
+ ProofTask.set_perspective idl;
+ TaskQueue.broadcast (Option.get !queue);
+ 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 ~doc ?loc ~drop_pt ~exn_info ~block_start ~block_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 VCS.is_vio_doc () then begin
+ let f,assign =
+ Future.create_delegate ~blocking:true ~name:pname (State.exn_on id ~valid) in
+ let t_uuid = Future.uuid f in
+ let task = ProofTask.(BuildProof {
+ t_exn_info; t_start = block_start; t_stop = block_stop; t_drop = drop_pt;
+ t_assign = assign; t_loc = loc; t_uuid; t_name = pname;
+ t_states = VCS.nodes_in_slice ~block_start ~block_stop }) in
+ TaskQueue.enqueue_task (Option.get !queue) task ~cancel_switch;
+ f, cancel_switch
+ end else
+ ProofTask.build_proof_here ~doc ?loc ~drop_pt t_exn_info block_stop, cancel_switch
+ else
+ let f, t_assign = Future.create_delegate ~name:pname (State.exn_on id ~valid) in
+ let t_uuid = Future.uuid f in
+ feedback (InProgress 1);
+ let task = ProofTask.(BuildProof {
+ t_exn_info; t_start = block_start; t_stop = block_stop; t_assign; t_drop = drop_pt;
+ t_loc = loc; t_uuid; t_name = pname;
+ t_states = VCS.nodes_in_slice ~block_start ~block_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 * bool) 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, b, _)) -> Some(r, b)
+ | _ -> None)
+ tasks in
+ stm_prerr_endline (fun () -> 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 * UState.t) option
+ type task = {
+ t_state : Stateid.t;
+ t_state_fb : Stateid.t;
+ t_assign : output Future.assignment -> unit;
+ t_ast : int * aast;
+ t_goal : Goal.goal;
+ t_kill : unit -> unit;
+ t_name : string }
+
+ include AsyncTaskQueue.Task with type task := task
+
+end = struct (* {{{ *)
+
+ type output = (Constr.constr * UState.t) option
+
+ let forward_feedback msg = Hooks.(call forward_feedback msg)
+
+ type task = {
+ t_state : Stateid.t;
+ t_state_fb : Stateid.t;
+ t_assign : output Future.assignment -> unit;
+ t_ast : int * aast;
+ 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 : int * aast;
+ r_goal : Goal.goal;
+ r_name : string }
+
+ type response =
+ | RespBuiltSubProof of (Constr.constr * UState.t)
+ | RespError of Pp.t
+ | RespNoProgress
+
+ let name = ref "tacticworker"
+ let extra_env () = [||]
+ type competence = unit
+ type worker_status = Fresh | Old of competence
+
+ 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 ~block_start:t_state ~block_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 (Some o)); `Stay ((),[])
+ | RespNoProgress ->
+ t_assign (`Val None);
+ t_kill ();
+ `Stay ((),[])
+ | RespError msg ->
+ let e = (RemoteException msg, Exninfo.null) in
+ t_assign (`Exn e);
+ t_kill ();
+ `Stay ((),[])
+
+ let on_marshal_error err { t_name } =
+ stm_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 command_focus = Proof.new_focus_kind ()
+ let focus_cond = Proof.no_cond command_focus
+
+ let perform { r_state = id; r_state_fb; r_document = vcs; r_ast; r_goal } =
+ Option.iter VCS.restore vcs;
+ try
+ Reach.known_state ~doc:dummy_doc (* XXX should be vcs *) ~cache:false id;
+ State.purify (fun () ->
+ let Proof.{sigma=sigma0} = Proof.data (Vernacstate.Proof_global.give_me_the_proof ()) in
+ let g = Evd.find sigma0 r_goal in
+ let is_ground c = Evarutil.is_ground_term sigma0 c in
+ if not (
+ is_ground Evd.(evar_concl g) &&
+ List.for_all (Context.Named.Declaration.for_all is_ground)
+ Evd.(evar_context g))
+ then
+ CErrors.user_err ~hdr:"STM" Pp.(strbrk("the par: goal selector supports ground "^
+ "goals only"))
+ else begin
+ let (i, ast) = r_ast in
+ Vernacstate.Proof_global.simple_with_current_proof (fun _ p -> Proof.focus focus_cond () i p);
+ (* STATE SPEC:
+ * - start : id
+ * - return: id
+ * => captures state id in a future closure, which will
+ discard execution state but for the proof + univs.
+ *)
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
+ ignore(stm_vernac_interp r_state_fb st ast);
+ let Proof.{sigma} = Proof.data (Vernacstate.Proof_global.give_me_the_proof ()) in
+ match Evd.(evar_body (find sigma r_goal)) with
+ | Evd.Evar_empty -> RespNoProgress
+ | Evd.Evar_defined t ->
+ let t = Evarutil.nf_evar sigma t in
+ if Evarutil.is_ground_term sigma t then
+ let t = EConstr.Unsafe.to_constr t in
+ RespBuiltSubProof (t, Evd.evar_universe_context sigma)
+ else CErrors.user_err ~hdr:"STM" Pp.(str"The solution is not ground")
+ end) ()
+ with e when CErrors.noncritical e -> RespError (CErrors.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 :
+ solve:bool -> abstract:bool -> cancel_switch:AsyncTaskQueue.cancel_switch ->
+ int -> Stateid.t -> Stateid.t -> aast -> unit
+
+end = struct (* {{{ *)
+
+ module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask) ()
+
+ let stm_fail ~st fail f =
+ if fail then
+ Vernacentries.with_fail ~st f
+ else
+ f ()
+
+ let vernac_interp ~solve ~abstract ~cancel_switch nworkers safe_id id
+ { indentation; verbose; loc; expr = e; strlen } : unit
+ =
+ let e, time, batch, fail =
+ let rec find ~time ~batch ~fail = function
+ | VernacTime (batch,{CAst.v=e}) -> find ~time:true ~batch ~fail e
+ | VernacRedirect (_,{CAst.v=e}) -> find ~time ~batch ~fail e
+ | VernacFail {CAst.v=e} -> find ~time ~batch ~fail:true e
+ | e -> e, time, batch, fail in
+ find ~time:false ~batch:false ~fail:false e in
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
+ stm_fail ~st fail (fun () ->
+ (if time then System.with_time ~batch ~header:(Pp.mt ()) else (fun x -> x)) (fun () ->
+ ignore(TaskQueue.with_n_workers nworkers (fun queue ->
+ Vernacstate.Proof_global.with_current_proof (fun _ p ->
+ let Proof.{goals} = Proof.data p in
+ let open TacTask in
+ let res = CList.map_i (fun i g ->
+ let f, assign =
+ Future.create_delegate
+ ~name:(Printf.sprintf "subgoal %d" i)
+ (State.exn_on id ~valid:safe_id) in
+ let t_ast = (i, { indentation; verbose; loc; expr = e; strlen }) 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 () -> if solve then TaskQueue.cancel_all queue) }
+ ~cancel_switch;
+ g,f)
+ 1 goals in
+ TaskQueue.join queue;
+ let assign_tac : unit Proofview.tactic =
+ Proofview.(Goal.enter begin fun g ->
+ let gid = Goal.goal g in
+ let f =
+ try List.assoc gid res
+ with Not_found -> CErrors.anomaly(str"Partac: wrong focus.") in
+ if not (Future.is_over f) then
+ (* One has failed and cancelled the others, but not this one *)
+ if solve then Tacticals.New.tclZEROMSG
+ (str"Interrupted by the failure of another goal")
+ else tclUNIT ()
+ else
+ let open Notations in
+ match Future.join f with
+ | Some (pt, uc) ->
+ let sigma, env = Vernacstate.Proof_global.get_current_context () in
+ stm_pperr_endline (fun () -> hov 0 (
+ str"g=" ++ int (Evar.repr gid) ++ spc () ++
+ str"t=" ++ (Printer.pr_constr_env env sigma pt) ++ spc () ++
+ str"uc=" ++ Termops.pr_evar_universe_context uc));
+ (if abstract then Abstract.tclABSTRACT None else (fun x -> x))
+ (V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*>
+ Tactics.exact_no_check (EConstr.of_constr pt))
+ | None ->
+ if solve then Tacticals.New.tclSOLVE [] else tclUNIT ()
+ end)
+ 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 : aast }
+ include AsyncTaskQueue.Task with type task := task
+
+end = struct (* {{{ *)
+
+ type task =
+ { t_where : Stateid.t; t_for : Stateid.t ; t_what : aast }
+
+ type request =
+ { r_where : Stateid.t ; r_for : Stateid.t ; r_what : aast; r_doc : VCS.vcs }
+ type response = unit
+
+ let name = ref "queryworker"
+ let extra_env _ = [||]
+ type competence = unit
+ type worker_status = Fresh | Old of competence
+
+ 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 ~block_start:t_where ~block_stop:t_where;
+ r_what = t_what }
+ with VCS.Expired -> None
+
+ let use_response _ _ _ = `End
+
+ let on_marshal_error _ _ =
+ stm_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 ~doc:dummy_doc (* XXX should be r_doc *) ~cache:false r_where;
+ (* STATE *)
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
+ try
+ (* STATE SPEC:
+ * - start: r_where
+ * - end : after execution of r_what
+ *)
+ ignore(stm_vernac_interp r_for st { r_what with verbose = true });
+ feedback ~id:r_for Processed
+ with e when CErrors.noncritical e ->
+ let e = CErrors.push e in
+ let msg = iprint e in
+ feedback ~id:r_for (Message (Error, None, 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:AsyncTaskQueue.cancel_switch -> Stateid.t -> Stateid.t -> aast -> unit
+
+end = struct (* {{{ *)
+
+ module TaskQueue = AsyncTaskQueue.MakeQueue(QueryTask) ()
+
+ let queue = ref None
+
+ let vernac_interp ~cancel_switch prev id q =
+ assert(TaskQueue.n_workers (Option.get !queue) > 0);
+ TaskQueue.enqueue_task (Option.get !queue)
+ QueryTask.({ t_where = prev; t_for = id; t_what = q }) ~cancel_switch
+
+ let init () = queue := Some (TaskQueue.create 0)
+
+end (* }}} *)
+
+(* Runs all transactions needed to reach a state *)
+and Reach : sig
+
+ val known_state :
+ doc:doc -> ?redefine_qed:bool -> cache:bool ->
+ Stateid.t -> unit
+
+end = struct (* {{{ *)
+
+let async_policy () =
+ if Attributes.is_universe_polymorphism () then false (* FIXME this makes no sense, it is the default value of the attribute *)
+ else if VCS.is_interactive () then
+ (async_proofs_is_master !cur_opt || !cur_opt.async_proofs_mode = APonLazy)
+ else
+ (VCS.is_vio_doc () || !cur_opt.async_proofs_mode <> APoff)
+
+let delegate name =
+ get_hint_bp_time name >= !cur_opt.async_proofs_delegation_threshold
+ || VCS.is_vio_doc ()
+
+let collect_proof keep cur hd brkind id =
+ stm_prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id);
+ let no_name = "" in
+ let name = function
+ | [] -> no_name
+ | id :: _ -> Names.Id.to_string id in
+ let loc = (snd cur).loc in
+ let is_defined_expr = function
+ | VernacEndProof (Proved (Proof_global.Transparent,_)) -> true
+ | _ -> false in
+ let is_defined = function
+ | _, { expr = e } -> is_defined_expr (Vernacprop.under_control e)
+ && (not (Vernacprop.has_Fail e)) in
+ let proof_using_ast = function
+ | VernacProof(_,Some _) -> true
+ | _ -> false
+ in
+ let proof_using_ast = function
+ | Some (_, v) when proof_using_ast (Vernacprop.under_control v.expr)
+ && (not (Vernacprop.has_Fail v.expr)) -> Some v
+ | _ -> None in
+ let has_proof_using x = proof_using_ast x <> None in
+ let proof_no_using = function
+ | VernacProof(t,None) -> t
+ | _ -> assert false
+ in
+ let proof_no_using = function
+ | Some (_, v) -> proof_no_using (Vernacprop.under_control v.expr), v
+ | _ -> assert false in
+ let has_proof_no_using = function
+ | VernacProof(_,None) -> true
+ | _ -> false
+ in
+ let has_proof_no_using = function
+ | Some (_, v) -> has_proof_no_using (Vernacprop.under_control v.expr)
+ && (not (Vernacprop.has_Fail v.expr))
+ | _ -> false in
+ let too_complex_to_delegate = function
+ | VernacDeclareModule _
+ | VernacDefineModule _
+ | VernacDeclareModuleType _
+ | VernacInclude _
+ | VernacRequire _
+ | VernacImport _ -> true
+ | ast -> may_pierce_opaque ast in
+ let parent = function Some (p, _) -> p | None -> assert false in
+ let is_empty = function `Async(_,[],_,_) | `MaybeASync(_,[],_,_) -> true | _ -> false in
+ let rec collect last accn id =
+ let view = VCS.visit id in
+ match view.step with
+ | (`Sideff (ReplayCommand x,_) | `Cmd { cast = x })
+ when too_complex_to_delegate (Vernacprop.under_control x.expr) ->
+ `Sync(no_name,`Print)
+ | `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next
+ | `Sideff (ReplayCommand x,_) -> collect (Some (id,x)) (id::accn) view.next
+ (* An Alias could jump everywhere... we hope we can ignore it*)
+ | `Alias _ -> `Sync (no_name,`Alias)
+ | `Fork((_,_,_,_::_::_), _) ->
+ `Sync (no_name,`MutualProofs)
+ | `Fork((_,_,Doesn'tGuaranteeOpacity,_), _) ->
+ `Sync (no_name,`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,accn,name,delegate name)
+ | `Fork((_, hd', GuaranteesOpacity, ids), _) when
+ has_proof_no_using last && not (State.is_cached_and_valid (parent last)) &&
+ VCS.is_vio_doc () ->
+ 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 <- VernacExpr([], VernacProof(t, Some hint));
+ `ASync (parent last,accn,name,delegate name)
+ with Not_found ->
+ let name = name ids in
+ `MaybeASync (parent last, accn, name, delegate name))
+ | `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, accn, name, delegate name)
+ | `Sideff (CherryPickEnv,_) ->
+ `Sync (no_name,`NestedProof)
+ | _ -> `Sync (no_name,`Unknown) in
+ let make_sync why = function
+ | `Sync(name,_) -> `Sync (name,why)
+ | `MaybeASync(_,_,name,_) -> `Sync (name,why)
+ | `ASync(_,_,name,_) -> `Sync (name,why) in
+
+ let check_policy rc = if async_policy () then rc else make_sync `Policy rc in
+ let is_vernac_exact = function
+ | VernacExactProof _ -> true
+ | _ -> false
+ in
+ match cur, (VCS.visit id).step, brkind with
+ | (parent, x), `Fork _, _ when is_vernac_exact (Vernacprop.under_control x.expr)
+ && (not (Vernacprop.has_Fail x.expr)) ->
+ `Sync (no_name,`Immediate)
+ | _, _, { VCS.kind = `Edit _ } -> check_policy (collect (Some cur) [] id)
+ | _ ->
+ if is_defined cur then `Sync (no_name,`Transparent)
+ else if keep == VtDrop then `Sync (no_name,`Aborted)
+ else
+ let rc = collect (Some cur) [] id in
+ if is_empty rc then make_sync `AlreadyEvaluated rc
+ else if (is_vtkeep keep) && (not(State.is_cached_and_valid id))
+ then check_policy rc
+ else make_sync `AlreadyEvaluated rc
+
+let string_of_reason = function
+ | `Transparent -> "non opaque"
+ | `AlreadyEvaluated -> "proof already evaluated"
+ | `Policy -> "policy"
+ | `NestedProof -> "contains nested proof"
+ | `Immediate -> "proof term given explicitly"
+ | `Aborted -> "aborted proof"
+ | `Doesn'tGuaranteeOpacity -> "not a simple opaque lemma"
+ | `MutualProofs -> "block of mutually recursive proofs"
+ | `Alias -> "contains Undo-like command"
+ | `Print -> "contains Print-like command"
+ | `NoPU_NoHint_NoES -> "no 'Proof using..', no .aux file, inside a section"
+ | `Unknown -> "unsupported case"
+
+let log_string s = stm_prerr_debug (fun () -> "STM: " ^ s)
+let log_processing_async id name = log_string Printf.(sprintf
+ "%s: proof %s: asynch" (Stateid.to_string id) name
+)
+let log_processing_sync id name reason = log_string Printf.(sprintf
+ "%s: proof %s: synch (cause: %s)"
+ (Stateid.to_string id) name (string_of_reason reason)
+)
+
+let wall_clock_last_fork = ref 0.0
+
+let known_state ~doc ?(redefine_qed=false) ~cache id =
+
+ let error_absorbing_tactic id blockname exn =
+ (* We keep the static/dynamic part of block detection separate, since
+ the static part could be performed earlier. As of today there is
+ no advantage in doing so since no UI can exploit such piece of info *)
+ detect_proof_block id blockname;
+
+ let boxes = VCS.box_of id in
+ let valid_boxes = CList.map_filter (function
+ | ProofBlock ({ block_stop } as decl, name) when Stateid.equal block_stop id ->
+ Some (decl, name)
+ | _ -> None) boxes in
+ assert(List.length valid_boxes < 2);
+ if valid_boxes = [] then Exninfo.iraise exn
+ else
+ let decl, name = List.hd valid_boxes in
+ try
+ let _, dynamic_check = List.assoc name !proof_block_delimiters in
+ match dynamic_check dummy_doc decl with
+ | `Leaks -> Exninfo.iraise exn
+ | `ValidBlock { base_state; goals_to_admit; recovery_command } -> begin
+ let tac =
+ Proofview.Goal.enter begin fun gl ->
+ if CList.mem_f Evar.equal
+ (Proofview.Goal.goal gl) goals_to_admit then
+ Proofview.give_up else Proofview.tclUNIT ()
+ end in
+ match (VCS.get_info base_state).state with
+ | FullState { Vernacstate.proof } ->
+ Option.iter Vernacstate.Proof_global.unfreeze proof;
+ Vernacstate.Proof_global.with_current_proof (fun _ p ->
+ feedback ~id:id Feedback.AddedAxiom;
+ fst (Pfedit.solve Goal_select.SelectAll None tac p), ());
+ (* STATE SPEC:
+ * - start: Modifies the input state adding a proof.
+ * - end : maybe after recovery command.
+ *)
+ (* STATE: We use an updated state with proof *)
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
+ Option.iter (fun expr -> ignore(stm_vernac_interp id st {
+ verbose = true; loc = None; expr; indentation = 0;
+ strlen = 0 } ))
+ recovery_command
+ | _ -> assert false
+ end
+ with Not_found ->
+ CErrors.user_err ~hdr:"STM"
+ (str "Unknown proof block delimiter " ++ str name)
+ in
+
+ (* Absorb tactic errors from f () *)
+ let resilient_tactic id blockname f =
+ if !cur_opt.async_proofs_tac_error_resilience = `None ||
+ (async_proofs_is_master !cur_opt &&
+ !cur_opt.async_proofs_mode = APoff)
+ then f ()
+ else
+ try f ()
+ with e when CErrors.noncritical e ->
+ let ie = CErrors.push e in
+ error_absorbing_tactic id blockname ie in
+ (* Absorb errors from f x *)
+ let resilient_command f x =
+ if not !cur_opt.async_proofs_cmd_error_resilience ||
+ (async_proofs_is_master !cur_opt &&
+ !cur_opt.async_proofs_mode = APoff)
+ then f x
+ else
+ try f x
+ with e when CErrors.noncritical e -> () in
+
+ (* ugly functions to process nested lemmas, i.e. hard to reproduce
+ * side effects *)
+ let cherry_pick_non_pstate () =
+ let st = Summary.freeze_summaries ~marshallable:false in
+ let st = Summary.remove_from_summary st Util.(pi1 summary_pstate) in
+ let st = Summary.remove_from_summary st Util.(pi2 summary_pstate) in
+ let st = Summary.remove_from_summary st Util.(pi3 summary_pstate) in
+ st, Lib.freeze ~marshallable:false in
+
+ let inject_non_pstate (s,l) =
+ Summary.unfreeze_summaries ~partial:true s; Lib.unfreeze l; update_global_env ()
+ in
+ let rec pure_cherry_pick_non_pstate safe_id id =
+ State.purify (fun id ->
+ stm_prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id);
+ reach ~safe_id id;
+ cherry_pick_non_pstate ())
+ id
+
+ (* traverses the dag backward from nodes being already calculated *)
+ and reach ?safe_id ?(redefine_qed=false) ?(cache=cache) id =
+ stm_prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id);
+ if not redefine_qed && State.is_cached ~cache id then begin
+ Hooks.(call state_computed ~doc id ~in_cache:true);
+ stm_prerr_endline (fun () -> "reached (cache)");
+ State.install_cached id
+ 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 = `SkipQueue } -> (fun () ->
+ reach view.next), cache, true
+ | `Cmd { cast = x; cqueue = `TacQueue (solve,abstract,cancel_switch); cblock } ->
+ (fun () ->
+ resilient_tactic id cblock (fun () ->
+ reach ~cache:true view.next;
+ Partac.vernac_interp ~solve ~abstract ~cancel_switch
+ !cur_opt.async_proofs_n_tacworkers view.next id x)
+ ), cache, true
+ | `Cmd { cast = x; cqueue = `QueryQueue cancel_switch }
+ when async_proofs_is_master !cur_opt -> (fun () ->
+ reach view.next;
+ Query.vernac_interp ~cancel_switch view.next id x
+ ), cache, false
+ | `Cmd { cast = x; ceff = eff; ctac = true; cblock } -> (fun () ->
+ resilient_tactic id cblock (fun () ->
+ reach view.next;
+ (* State resulting from reach *)
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
+ ignore(stm_vernac_interp id st x)
+ );
+ if eff then update_global_env ()
+ ), eff || cache, true
+ | `Cmd { cast = x; ceff = eff } -> (fun () ->
+ (match !cur_opt.async_proofs_mode with
+ | APon | APonLazy ->
+ resilient_command reach view.next
+ | APoff -> reach view.next);
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
+ ignore(stm_vernac_interp id st x);
+ if eff then update_global_env ()
+ ), eff || cache, true
+ | `Fork ((x,_,_,_), None) -> (fun () ->
+ resilient_command reach view.next;
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
+ ignore(stm_vernac_interp id st x);
+ wall_clock_last_fork := Unix.gettimeofday ()
+ ), true, true
+ | `Fork ((x,_,_,_), Some prev) -> (fun () -> (* nested proof *)
+ reach ~cache:true prev;
+ reach view.next;
+
+ (try
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
+ ignore(stm_vernac_interp id st x);
+ with e when CErrors.noncritical e ->
+ let (e, info) = CErrors.push e in
+ let info = Stateid.add info ~valid:prev id in
+ Exninfo.iraise (e, info));
+ wall_clock_last_fork := Unix.gettimeofday ()
+ ), true, true
+ | `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) ->
+ let rec aux = function
+ | `ASync (block_start, nodes, name, delegate) -> (fun () ->
+ let keep' = get_vtkeep keep in
+ let drop_pt = keep' == VtKeepAxiom in
+ let block_stop, exn_info, loc = eop, (id, eop), x.loc in
+ log_processing_async id name;
+ VCS.create_proof_task_box nodes ~qed:id ~block_start;
+ begin match brinfo, qed.fproof with
+ | { VCS.kind = `Edit _ }, None -> assert false
+ | { VCS.kind = `Edit (_,_, okeep, _) }, Some (ofp, cancel) ->
+ assert(redefine_qed = true);
+ if okeep <> keep then
+ msg_warning(strbrk("The command closing the proof changed. "
+ ^"The kernel cannot take this into account and will "
+ ^(if not drop_pt then "not check " else "reject ")
+ ^"the "^(if not drop_pt then "new" else "incomplete")
+ ^" proof. Reprocess the command declaring "
+ ^"the proof's statement to avoid that."));
+ let fp, cancel =
+ Slaves.build_proof ~doc
+ ?loc ~drop_pt ~exn_info ~block_start ~block_stop ~name in
+ Future.replace ofp fp;
+ qed.fproof <- Some (fp, cancel);
+ (* We don't generate a new state, but we still need
+ * to install the right one *)
+ State.install_cached id
+ | { VCS.kind = `Proof _ }, Some _ -> assert false
+ | { VCS.kind = `Proof _ }, None ->
+ reach ~cache:true block_start;
+ let fp, cancel =
+ if delegate then
+ Slaves.build_proof ~doc
+ ?loc ~drop_pt ~exn_info ~block_start ~block_stop ~name
+ else
+ ProofTask.build_proof_here ~doc ?loc
+ ~drop_pt exn_info block_stop, ref false
+ in
+ qed.fproof <- Some (fp, cancel);
+ let opaque = match keep' with
+ | VtKeepAxiom | VtKeepOpaque ->
+ Proof_global.Opaque (* Admitted -> Opaque should be OK. *)
+ | VtKeepDefined -> Proof_global.Transparent
+ in
+ let proof =
+ Vernacstate.Proof_global.close_future_proof ~opaque ~feedback_id:id fp in
+ if not delegate then ignore(Future.compute fp);
+ reach view.next;
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
+ ignore(stm_vernac_interp id ~proof st x);
+ feedback ~id:id Incomplete
+ | { VCS.kind = `Master }, _ -> assert false
+ end;
+ Vernacstate.Proof_global.discard_all ()
+ ), not redefine_qed, true
+ | `Sync (name, `Immediate) -> (fun () ->
+ reach eop;
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
+ ignore(stm_vernac_interp id st x);
+ Vernacstate.Proof_global.discard_all ()
+ ), true, true
+ | `Sync (name, reason) -> (fun () ->
+ log_processing_sync id name reason;
+ reach eop;
+ let wall_clock = Unix.gettimeofday () in
+ record_pb_time name ?loc:x.loc (wall_clock -. !wall_clock_last_fork);
+ let proof =
+ match keep with
+ | VtDrop -> None
+ | VtKeep VtKeepAxiom ->
+ let ctx = UState.empty in
+ let fp = Future.from_val ([],ctx) in
+ qed.fproof <- Some (fp, ref false); None
+ | VtKeep opaque ->
+ let opaque = let open Proof_global in match opaque with
+ | VtKeepOpaque -> Opaque | VtKeepDefined -> Transparent
+ | VtKeepAxiom -> assert false
+ in
+ Some(Vernacstate.Proof_global.close_proof ~opaque
+ ~keep_body_ucst_separate:false
+ (State.exn_on id ~valid:eop)) in
+ if keep <> VtKeep VtKeepAxiom then
+ reach view.next;
+ let wall_clock2 = Unix.gettimeofday () in
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
+ ignore(stm_vernac_interp id ?proof st x);
+ let wall_clock3 = Unix.gettimeofday () in
+ Aux_file.record_in_aux_at ?loc:x.loc "proof_check_time"
+ (Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2));
+ Vernacstate.Proof_global.discard_all ()
+ ), true, true
+ | `MaybeASync (start, nodes, name, delegate) -> (fun () ->
+ reach ~cache:true start;
+ (* no sections *)
+ if CList.is_empty (Environ.named_context (Global.env ()))
+ then Util.pi1 (aux (`ASync (start, nodes, name, delegate))) ()
+ else Util.pi1 (aux (`Sync (name, `NoPU_NoHint_NoES))) ()
+ ), not redefine_qed, true
+ in
+ aux (collect_proof keep (view.next, x) brname brinfo eop)
+ | `Sideff (ReplayCommand x,_) -> (fun () ->
+ reach view.next;
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
+ ignore(stm_vernac_interp id st x);
+ update_global_env ()
+ ), cache, true
+ | `Sideff (CherryPickEnv, origin) -> (fun () ->
+ reach view.next;
+ inject_non_pstate (pure_cherry_pick_non_pstate view.next origin);
+ ), cache, true
+ in
+ let cache_step =
+ !cur_opt.async_proofs_cache = Some Force || cache_step
+ in
+ State.define ~doc ?safe_id
+ ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id;
+ stm_prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in
+ reach ~redefine_qed id
+
+end (* }}} *)
+[@@@ocaml.warning "+60"]
+
+(********************************* STM API ************************************)
+(******************************************************************************)
+
+(* Main initalization routine *)
+type stm_init_options = {
+ (* The STM will set some internal flags differently depending on the
+ specified [doc_type]. This distinction should dissappear at some
+ some point. *)
+ doc_type : stm_doc_type;
+
+ (* Initial load path in scope for the document. Usually extracted
+ from -R options / _CoqProject *)
+ iload_path : Mltop.coq_path list;
+
+ (* Require [require_libs] before the initial state is
+ ready. Parameters follow [Library], that is to say,
+ [lib,prefix,import_export] means require library [lib] from
+ optional [prefix] and [import_export] if [Some false/Some true]
+ is used. *)
+ require_libs : (string * string option * bool option) list;
+
+ (* STM options that apply to the current document. *)
+ stm_options : AsyncOpts.stm_opt;
+}
+(* fb_handler : Feedback.feedback -> unit; *)
+
+(*
+let doc_type_module_name (std : stm_doc_type) =
+ match std with
+ | VoDoc mn | VioDoc mn | Vio2Vo mn -> mn
+ | Interactive mn -> Names.DirPath.to_string mn
+*)
+
+let init_core () =
+ if !cur_opt.async_proofs_mode = APon then Control.enable_thread_delay := true;
+ State.register_root_state ()
+
+let dirpath_of_file f =
+ let ldir0 =
+ try
+ let lp = Loadpath.find_load_path (Filename.dirname f) in
+ Loadpath.logical lp
+ with Not_found -> Libnames.default_root_prefix
+ in
+ let file = Filename.chop_extension (Filename.basename f) in
+ let id = Id.of_string file in
+ let ldir = Libnames.add_dirpath_suffix ldir0 id in
+ ldir
+
+let new_doc { doc_type ; iload_path; require_libs; stm_options } =
+
+ let load_objs libs =
+ let rq_file (dir, from, exp) =
+ let mp = Libnames.qualid_of_string dir in
+ let mfrom = Option.map Libnames.qualid_of_string from in
+ Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in
+ List.(iter rq_file (rev libs))
+ in
+
+ (* Set the options from the new documents *)
+ AsyncOpts.cur_opt := stm_options;
+
+ (* We must reset the whole state before creating a document! *)
+ State.restore_root_state ();
+
+ let doc = VCS.init doc_type Stateid.initial (Vernacstate.Parser.init ()) in
+
+ (* Set load path; important, this has to happen before we declare
+ the library below as [Declaremods/Library] will infer the module
+ name by looking at the load path! *)
+ List.iter Mltop.add_coq_path iload_path;
+
+ Safe_typing.allow_delayed_constants := !cur_opt.async_proofs_mode <> APoff;
+
+ begin match doc_type with
+ | Interactive ln ->
+ let dp = match ln with
+ | TopLogical dp -> dp
+ | TopPhysical f -> dirpath_of_file f
+ in
+ Declaremods.start_library dp
+
+ | VoDoc f ->
+ let ldir = dirpath_of_file f in
+ let () = Flags.verbosely Declaremods.start_library ldir in
+ VCS.set_ldir ldir;
+ set_compilation_hints f
+
+ | VioDoc f ->
+ let ldir = dirpath_of_file f in
+ let () = Flags.verbosely Declaremods.start_library ldir in
+ VCS.set_ldir ldir;
+ set_compilation_hints f
+ end;
+
+ (* Import initial libraries. *)
+ load_objs require_libs;
+
+ (* We record the state at this point! *)
+ State.define ~doc ~cache:true ~redefine:true (fun () -> ()) Stateid.initial;
+ Backtrack.record ();
+ Slaves.init ();
+ if async_proofs_is_master !cur_opt then begin
+ stm_prerr_endline (fun () -> "Initializing workers");
+ Query.init ();
+ let opts = match !cur_opt.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;
+ doc, VCS.cur_tip ()
+
+let observe ~doc id =
+ let vcs = VCS.backup () in
+ try
+ Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id;
+ VCS.print ();
+ doc
+ with e ->
+ let e = CErrors.push e in
+ VCS.print ();
+ VCS.restore vcs;
+ Exninfo.iraise e
+
+let finish ~doc =
+ let head = VCS.current_branch () in
+ let doc = observe ~doc (VCS.get_branch_pos head) in
+ VCS.print (); doc
+
+let wait ~doc =
+ let doc = observe ~doc (VCS.get_branch_pos VCS.Branch.master) in
+ Slaves.wait_all_done ();
+ VCS.print ();
+ doc
+
+let rec join_admitted_proofs id =
+ if Stateid.equal id Stateid.initial then () else
+ let view = VCS.visit id in
+ match view.step with
+ | `Qed ({ keep = VtKeep VtKeepAxiom; fproof = Some (fp,_) },_) ->
+ ignore(Future.force fp);
+ join_admitted_proofs view.next
+ | _ -> join_admitted_proofs view.next
+
+(* Error resiliency may have tolerated some broken commands *)
+let rec check_no_err_states ~doc visited id =
+ let open Stateid in
+ if Set.mem id visited then visited else
+ match state_of_id ~doc id with
+ | `Error e -> raise e
+ | _ ->
+ let view = VCS.visit id in
+ match view.step with
+ | `Qed(_,id) ->
+ let visited = check_no_err_states ~doc (Set.add id visited) id in
+ check_no_err_states ~doc visited view.next
+ | _ -> check_no_err_states ~doc (Set.add id visited) view.next
+
+let join ~doc =
+ let doc = wait ~doc in
+ stm_prerr_endline (fun () -> "Joining the environment");
+ Global.join_safe_environment ();
+ stm_prerr_endline (fun () -> "Joining Admitted proofs");
+ join_admitted_proofs (VCS.get_branch_pos VCS.Branch.master);
+ stm_prerr_endline (fun () -> "Checking no error states");
+ ignore(check_no_err_states ~doc (Stateid.Set.singleton Stateid.initial)
+ (VCS.get_branch_pos VCS.Branch.master));
+ VCS.print ();
+ doc
+
+let dump_snapshot () = Slaves.dump_snapshot (), RemoteCounter.snapshot ()
+
+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 = State.purify (Slaves.check_task name tasks) i in
+ VCS.restore vcs;
+ rc
+ with e when CErrors.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 = State.purify (Slaves.finish_task name u d p t) i in
+ 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 = CErrors.push e in
+ msg_warning (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e);
+ exit 1
+
+let merge_proof_branch ~valid ?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 None () in
+ let parsing = Option.get @@ VCS.get_parsing_state (VCS.cur_tip ()) in
+ VCS.merge id ~ours:(Qed (qed None)) brname;
+ VCS.set_parsing_state id parsing;
+ VCS.delete_branch brname;
+ VCS.propagate_qed ();
+ `Ok
+ | { VCS.kind = `Edit (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 ();
+ let _st : unit = Reach.known_state ~doc:dummy_doc (* XXX should be taken in input *) ~redefine_qed:true ~cache:false qed_id in
+ VCS.checkout VCS.Branch.master;
+ `Unfocus qed_id
+ | { VCS.kind = `Master } ->
+ Exninfo.iraise (State.exn_on ~valid Stateid.dummy (Vernacstate.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 =
+ VCS.restore vcs;
+ VCS.print ();
+ Exninfo.iraise (e, info)
+
+let snapshot_vio ~doc ~output_native_objects ldir long_f_dot_vo =
+ let doc = finish ~doc in
+ if List.length (VCS.branches ()) > 1 then
+ CErrors.user_err ~hdr:"stm" (str"Cannot dump a vio with open proofs");
+ Library.save_library_to ~todo:(dump_snapshot ()) ~output_native_objects
+ ldir long_f_dot_vo
+ (Global.opaque_tables ());
+ doc
+
+let reset_task_queue = Slaves.reset_task_queue
+
+(* Document building *)
+
+(* We process a meta command found in the document *)
+let process_back_meta_command ~newtip ~head oid aast =
+ let valid = VCS.get_branch_pos head in
+ let old_parsing = Option.get @@ VCS.get_parsing_state oid in
+
+ (* Merge in and discard all the branches currently open that were not open in `oid` *)
+ 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 ~valid aast VtDrop branch))
+ (VCS.branches ());
+
+ (* We add a node on top of every branch, to represent state aliasing *)
+ VCS.checkout_shallowest_proof_branch ();
+ let head = VCS.current_branch () in
+ List.iter (fun b ->
+ VCS.checkout b;
+ let id = if (VCS.Branch.equal b head) then Some newtip else None in
+ let proof_mode = VCS.get_proof_mode @@ VCS.cur_tip () in
+ let id = VCS.new_node ?id proof_mode () in
+ VCS.commit id (Alias (oid,aast));
+ VCS.set_parsing_state id old_parsing)
+ (VCS.branches ());
+ VCS.checkout_shallowest_proof_branch ();
+ Backtrack.record (); `Ok
+
+let get_allow_nested_proofs =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~name:"Nested Proofs Allowed"
+ ~key:Vernac_classifier.stm_allow_nested_proofs_option_name
+ ~value:false
+
+(** [process_transaction] adds a node in the document *)
+let process_transaction ~doc ?(newtip=Stateid.fresh ())
+ ({ verbose; loc; expr } as x) c =
+ stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x);
+ let vcs = VCS.backup () in
+ try
+ let head = VCS.current_branch () in
+ VCS.checkout head;
+ let head_parsing =
+ Option.get @@ VCS.(get_parsing_state (get_branch_pos head)) in
+ let proof_mode = VCS.(get_proof_mode (get_branch_pos head)) in
+ let rc = begin
+ stm_prerr_endline (fun () ->
+ " classified as: " ^ Vernac_classifier.string_of_vernac_classification c);
+ match c with
+ (* Meta *)
+ | VtMeta, _ ->
+ let id = Backtrack.undo_vernac_classifier expr ~doc in
+ process_back_meta_command ~newtip ~head id x
+
+ (* Query *)
+ | VtQuery, w ->
+ let id = VCS.new_node ~id:newtip proof_mode () in
+ let queue =
+ if VCS.is_vio_doc () &&
+ VCS.((get_branch head).kind = `Master) &&
+ may_pierce_opaque (Vernacprop.under_control x.expr)
+ then `SkipQueue
+ else `MainQueue in
+ VCS.commit id (mkTransCmd x [] false queue);
+ VCS.set_parsing_state id head_parsing;
+ Backtrack.record (); assert (w == VtLater); `Ok
+
+ (* Proof *)
+ | VtStartProof (guarantee, names), w ->
+
+ if not (get_allow_nested_proofs ()) && VCS.proof_nesting () > 0 then
+ "Nested proofs are not allowed unless you turn option Nested Proofs Allowed on."
+ |> Pp.str
+ |> (fun s -> (UserError (None, s), Exninfo.null))
+ |> State.exn_on ~valid:Stateid.dummy newtip
+ |> Exninfo.iraise
+ else
+
+ let proof_mode = Some (Vernacentries.get_default_proof_mode ()) in
+ let id = VCS.new_node ~id:newtip proof_mode () 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 (VCS.proof_nesting () + 1))
+ end else begin
+ VCS.branch bname (`Proof (VCS.proof_nesting () + 1));
+ VCS.merge id ~ours:(Fork (x, bname, guarantee, names)) head
+ end;
+ VCS.set_parsing_state id head_parsing;
+ Backtrack.record (); assert (w == VtLater); `Ok
+
+ | VtProofStep { parallel; proof_block_detection = cblock }, w ->
+ let id = VCS.new_node ~id:newtip proof_mode () in
+ let queue =
+ match parallel with
+ | `Yes(solve,abstract) -> `TacQueue (solve, abstract, ref false)
+ | `No -> `MainQueue in
+ VCS.commit id (mkTransTac x cblock queue);
+ (* Static proof block detection delayed until an error really occurs.
+ If/when and UI will make something useful with this piece of info,
+ detection should occur here.
+ detect_proof_block id cblock; *)
+ VCS.set_parsing_state id head_parsing;
+ Backtrack.record (); assert (w == VtLater); `Ok
+
+ | VtQed keep, w ->
+ let valid = VCS.get_branch_pos head in
+ let rc =
+ merge_proof_branch ~valid ~id:newtip x keep head in
+ VCS.checkout_shallowest_proof_branch ();
+ Backtrack.record (); assert (w == VtLater);
+ rc
+
+ (* Side effect in a (still open) proof is replayed on all branches*)
+ | VtSideff l, w ->
+ let id = VCS.new_node ~id:newtip proof_mode () in
+ let new_ids =
+ match (VCS.get_branch head).VCS.kind with
+ | `Edit _ -> VCS.commit id (mkTransCmd x l true `MainQueue); []
+ | `Master -> VCS.commit id (mkTransCmd x l false `MainQueue); []
+ | `Proof _ ->
+ VCS.checkout VCS.Branch.master;
+ VCS.commit id (mkTransCmd x l true `MainQueue);
+ (* We can't replay a Definition since universes may be differently
+ * inferred. This holds in Coq >= 8.5 *)
+ let action = match Vernacprop.under_control x.expr with
+ | VernacDefinition(_, _, DefineBody _) -> CherryPickEnv
+ | _ -> ReplayCommand x in
+ VCS.propagate_sideff ~action
+ in
+ VCS.checkout_shallowest_proof_branch ();
+ Backtrack.record ();
+ let parsing_state =
+ begin match w with
+ | VtNow ->
+ (* We need to execute to get the new parsing state *)
+ ignore(finish ~doc:dummy_doc);
+ let parsing = Vernacstate.Parser.cur_state () in
+ (* If execution has not been put in cache, we need to save the parsing state *)
+ if (VCS.get_info id).state == EmptyState then VCS.set_parsing_state id parsing;
+ parsing
+ | VtLater -> VCS.set_parsing_state id head_parsing; head_parsing
+ end
+ in
+ (* We save the parsing state on non-master branches *)
+ List.iter (fun id ->
+ if (VCS.get_info id).state == EmptyState then
+ VCS.set_parsing_state id parsing_state) new_ids;
+ `Ok
+
+ (* Unknown: we execute it, check for open goals and propagate sideeff *)
+ | VtUnknown, VtNow ->
+ let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in
+ if not (get_allow_nested_proofs ()) && in_proof then
+ "Commands which may open proofs are not allowed in a proof unless you turn option Nested Proofs Allowed on."
+ |> Pp.str
+ |> (fun s -> (UserError (None, s), Exninfo.null))
+ |> State.exn_on ~valid:Stateid.dummy newtip
+ |> Exninfo.iraise
+ else
+ let id = VCS.new_node ~id:newtip proof_mode () in
+ let head_id = VCS.get_branch_pos head in
+ let _st : unit = Reach.known_state ~doc ~cache:true head_id in (* ensure it is ok *)
+ let step () =
+ VCS.checkout VCS.Branch.master;
+ let mid = VCS.get_branch_pos VCS.Branch.master in
+ let _st' : unit = Reach.known_state ~doc ~cache:(VCS.is_interactive ()) mid in
+ let st = Vernacstate.freeze_interp_state ~marshallable:false in
+ ignore(stm_vernac_interp id st x);
+ (* Vernac x may or may not start a proof *)
+ if not in_proof && Vernacstate.Proof_global.there_are_pending_proofs () then
+ begin
+ let bname = VCS.mk_branch_name x in
+ let opacity_of_produced_term = function
+ (* This AST is ambiguous, hence we check it dynamically *)
+ | VernacInstance (_,_ , None, _) -> GuaranteesOpacity
+ | _ -> Doesn'tGuaranteeOpacity in
+ VCS.commit id (Fork (x,bname,opacity_of_produced_term (Vernacprop.under_control x.expr),[]));
+ VCS.set_proof_mode id (Some (Vernacentries.get_default_proof_mode ()));
+ VCS.branch bname (`Proof (VCS.proof_nesting () + 1));
+ end else begin
+ begin match (VCS.get_branch head).VCS.kind with
+ | `Edit _ -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
+ | `Master -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
+ | `Proof _ ->
+ VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
+ (* We hope it can be replayed, but we can't really know *)
+ ignore(VCS.propagate_sideff ~action:(ReplayCommand x));
+ end;
+ VCS.checkout_shallowest_proof_branch ();
+ end in
+ State.define ~doc ~safe_id:head_id ~cache:true step id;
+ Backtrack.record (); `Ok
+
+ | VtUnknown, VtLater ->
+ anomaly(str"classifier: VtUnknown must imply VtNow.")
+
+ | VtProofMode pm, VtNow ->
+ let proof_mode = Pvernac.lookup_proof_mode pm in
+ let id = VCS.new_node ~id:newtip proof_mode () in
+ VCS.commit id (mkTransCmd x [] false `MainQueue);
+ VCS.set_parsing_state id head_parsing;
+ Backtrack.record (); `Ok
+
+ | VtProofMode _, VtLater ->
+ anomaly(str"classifier: VtProofMode must imply VtNow.")
+
+ end in
+ let pr_rc rc = match rc with
+ | `Ok -> Pp.(seq [str "newtip ("; str (Stateid.to_string (VCS.cur_tip ())); str ")"])
+ | _ -> Pp.(str "unfocus")
+ in
+ stm_pperr_endline (fun () -> str "processed with " ++ pr_rc rc ++ str " }}}");
+ VCS.print ();
+ rc
+ with e ->
+ let e = CErrors.push e in
+ handle_failure e vcs
+
+let get_ast ~doc id =
+ match VCS.visit id with
+ | { step = `Cmd { cast = { loc; expr } } }
+ | { step = `Fork (({ loc; expr }, _, _, _), _) }
+ | { step = `Sideff ((ReplayCommand {loc; expr}) , _) }
+ | { step = `Qed ({ qast = { loc; expr } }, _) } ->
+ Some (Loc.tag ?loc expr)
+ | _ -> None
+
+let stop_worker n = Slaves.cancel_worker n
+
+let parse_sentence ~doc sid ~entry pa =
+ let ps = Option.get @@ VCS.get_parsing_state sid in
+ let proof_mode = VCS.get_proof_mode sid in
+ Vernacstate.Parser.parse ps (entry proof_mode) pa
+
+(* You may need to know the len + indentation of previous command to compute
+ * the indentation of the current one.
+ * Eg. foo. bar.
+ * Here bar is indented of the indentation of foo + its strlen (4) *)
+let ind_len_loc_of_id sid =
+ if Stateid.equal sid Stateid.initial then None
+ else match (VCS.visit sid).step with
+ | `Cmd { ctac = true; cast = { indentation; strlen; loc } } ->
+ Some (indentation, strlen, loc)
+ | _ -> None
+
+(* the indentation logic works like this: if the beginning of the
+ command is different than the start we are in a new line, thus
+ indentation follows from the starting position. Otherwise, we use
+ the previous one plus the offset.
+
+ Note, this could maybe improved by handling more cases in
+ compute_indentation. *)
+
+let compute_indentation ?loc sid = Option.cata (fun loc ->
+ let open Loc in
+ (* The effective lenght is the lenght on the last line *)
+ let len = loc.ep - loc.bp in
+ let prev_indent = match ind_len_loc_of_id sid with
+ | None -> 0
+ | Some (i,l,p) -> i + l
+ in
+ (* Now if the line has not changed, the need to add the previous indent *)
+ let eff_indent = loc.bp - loc.bol_pos in
+ if loc.bol_pos = 0 then
+ eff_indent + prev_indent, len
+ else
+ eff_indent, len
+ ) (0, 0) loc
+
+let add ~doc ~ontop ?newtip verb { CAst.loc; v=ast } =
+ let cur_tip = VCS.cur_tip () in
+ if not (Stateid.equal ontop cur_tip) then
+ user_err ?loc ~hdr:"Stm.add"
+ (str "Stm.add called for a different state (" ++ str (Stateid.to_string ontop) ++
+ str ") than the tip: " ++ str (Stateid.to_string cur_tip) ++ str "." ++ fnl () ++
+ str "This is not supported yet, sorry.");
+ let indentation, strlen = compute_indentation ?loc ontop in
+ (* XXX: Classifiy vernac should be moved inside process transaction *)
+ let clas = Vernac_classifier.classify_vernac ast in
+ let aast = { verbose = verb; indentation; strlen; loc; expr = ast } in
+ match process_transaction ~doc ?newtip aast clas with
+ | `Ok -> doc, VCS.cur_tip (), `NewTip
+ | `Unfocus qed_id -> doc, qed_id, `Unfocus (VCS.cur_tip ())
+
+let set_perspective ~doc id_list = Slaves.set_perspective id_list
+
+type focus = {
+ start : Stateid.t;
+ stop : Stateid.t;
+ tip : Stateid.t
+}
+
+let query ~doc ~at ~route s =
+ State.purify (fun s ->
+ if Stateid.equal at Stateid.dummy then ignore(finish ~doc:dummy_doc)
+ else Reach.known_state ~doc ~cache:true at;
+ let rec loop () =
+ match parse_sentence ~doc at ~entry:Pvernac.main_entry s with
+ | None -> ()
+ | Some {CAst.loc; v=ast} ->
+ let indentation, strlen = compute_indentation ?loc at in
+ let st = State.get_cached at in
+ let aast = {
+ verbose = true; indentation; strlen;
+ loc; expr = ast } in
+ ignore(stm_vernac_interp ~route at st aast);
+ loop ()
+ in
+ loop ()
+ )
+ s
+
+let edit_at ~doc 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 =
+ match VCS.visit cur with
+ | { step = `Fork _ } -> false
+ | { next } -> if id = cur then true else aux next in
+ aux (VCS.get_branch_pos (VCS.current_branch ())) in
+ let rec is_pure_aux id =
+ let view = VCS.visit id in
+ match view.step with
+ | `Cmd _ -> is_pure_aux view.next
+ | `Fork _ -> true
+ | _ -> false in
+ let is_pure id =
+ match (VCS.visit id).step with
+ | `Qed (_,last_step) -> is_pure_aux last_step
+ | _ -> assert false
+ in
+ let is_ancestor_of_cur_branch id =
+ Stateid.Set.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
+ | { step = (`Fork _ | `Qed _) } -> tip
+ | { step = `Sideff (ReplayCommand _,id) } -> id
+ | { step = `Sideff _ } -> tip
+ | { next } -> master_for_br root next in
+ let reopen_branch start at_id qed_id tip old_branch =
+ let master_id, cancel_switch, keep =
+ (* Hum, this should be the real start_id in the cluster and not next *)
+ match VCS.visit qed_id with
+ | { step = `Qed ({ fproof = Some (_,cs); keep },_) } -> start, cs, keep
+ | _ -> anomaly (str "ProofTask not ending with Qed.") in
+ VCS.branch ~root:master_id ~pos:id
+ VCS.edit_branch (`Edit (qed_id, master_id, keep, old_branch));
+ VCS.delete_boxes_of id;
+ cancel_switch := true;
+ Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id;
+ VCS.checkout_shallowest_proof_branch ();
+ `Focus { stop = qed_id; start = master_id; tip } in
+ let no_edit = function
+ | `Edit (_,_,_,_) -> `Proof 1
+ | x -> x in
+ let backto id bn =
+ 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) &&
+ Stateid.Set.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
+ (Option.default brname bn)
+ (no_edit brinfo.VCS.kind);
+ VCS.delete_boxes_of id;
+ VCS.gc ();
+ VCS.print ();
+ Reach.known_state ~doc ~cache:(VCS.is_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 = bn, { VCS.kind = `Proof _ }} -> Some bn
+ | Some{ mine = _, { VCS.kind = `Edit(_,_,_,bn) }} -> Some bn
+ | _ -> None in
+ match focused, VCS.proof_task_box_of id, branch_info with
+ | _, Some _, None -> assert false
+ | false, Some { qed = qed_id ; lemma = start }, Some bn ->
+ let tip = VCS.cur_tip () in
+ if has_failed qed_id && is_pure qed_id && not !cur_opt.async_proofs_never_reopen_branch
+ then reopen_branch start id qed_id tip bn
+ else backto id (Some bn)
+ | true, Some { qed = qed_id }, Some bn ->
+ if on_cur_branch id then begin
+ assert false
+ end else if is_ancestor_of_cur_branch id then begin
+ backto id (Some bn)
+ 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 ~doc ~cache:(VCS.is_interactive ()) id;
+ VCS.checkout_shallowest_proof_branch ();
+ `NewTip
+ end else if is_ancestor_of_cur_branch id then begin
+ backto id None
+ end else begin
+ anomaly(str"Cannot leave an `Edit branch open.")
+ end
+ | false, None, Some bn -> backto id (Some bn)
+ | false, None, None -> backto id None
+ in
+ VCS.print ();
+ doc, rc
+ with e ->
+ let (e, info) = CErrors.push e in
+ match Stateid.get info with
+ | None ->
+ VCS.print ();
+ anomaly (str ("edit_at "^Stateid.to_string id^": ") ++
+ CErrors.print_no_report e ++ str ".")
+ | Some (_, id) ->
+ stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
+ VCS.restore vcs;
+ VCS.print ();
+ Exninfo.iraise (e, info)
+
+let get_current_state ~doc = VCS.cur_tip ()
+let get_ldir ~doc = VCS.get_ldir ()
+
+let get_doc did = dummy_doc
+
+(*********************** TTY API (PG, coqtop, coqc) ***************************)
+(******************************************************************************)
+
+let current_proof_depth ~doc =
+ 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 ~doc =
+ List.map unmangle (CList.map_filter proofname (VCS.branches ()))
+
+(* Export hooks *)
+let state_computed_hook = Hooks.state_computed_hook
+let state_ready_hook = Hooks.state_ready_hook
+let forward_feedback_hook = Hooks.forward_feedback_hook
+let unreachable_state_hook = Hooks.unreachable_state_hook
+let () = Hook.set Obligations.stm_get_fix_exn (fun () -> !State.fix_exn_ref)
+
+type document = VCS.vcs
+let backup () = VCS.backup ()
+let restore d = VCS.restore d
+
+
+(* vim:set foldmethod=marker: *)
diff --git a/stm/stm.mli b/stm/stm.mli
new file mode 100644
index 0000000000..91651e3534
--- /dev/null
+++ b/stm/stm.mli
@@ -0,0 +1,299 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Names
+
+(** state-transaction-machine interface *)
+
+(* Flags *)
+module AsyncOpts : sig
+
+ type cache = Force
+ type async_proofs = APoff
+ | APonLazy (* Delays proof checking, but does it in master *)
+ | APon
+ type tac_error_filter = [ `None | `Only of string list | `All ]
+
+ type stm_opt = {
+ async_proofs_n_workers : int;
+ async_proofs_n_tacworkers : int;
+
+ async_proofs_cache : cache option;
+ async_proofs_mode : async_proofs;
+
+ async_proofs_private_flags : string option;
+ async_proofs_never_reopen_branch : bool;
+
+ async_proofs_tac_error_resilience : tac_error_filter;
+ async_proofs_cmd_error_resilience : bool;
+ async_proofs_delegation_threshold : float;
+ }
+
+ val default_opts : stm_opt
+
+end
+
+type interactive_top = TopLogical of DirPath.t | TopPhysical of string
+
+(** The STM document type [stm_doc_type] determines some properties
+ such as what uncompleted proofs are allowed and what gets recorded
+ to aux files. *)
+type stm_doc_type =
+ | VoDoc of string (* file path *)
+ | VioDoc of string (* file path *)
+ | Interactive of interactive_top (* module path *)
+
+(** Coq initalization options:
+
+ - [doc_type]: Type of document being created.
+
+ - [require_libs]: list of libraries/modules to be pre-loaded at
+ startup. A tuple [(modname,modfrom,import)] is equivalent to [From
+ modfrom Require modname]; [import] works similarly to
+ [Library.require_library_from_dirpath], [Some false] will import
+ the module, [Some true] will additionally export it.
+
+*)
+type stm_init_options = {
+ (* The STM will set some internal flags differently depending on the
+ specified [doc_type]. This distinction should dissappear at some
+ some point. *)
+ doc_type : stm_doc_type;
+
+ (* Initial load path in scope for the document. Usually extracted
+ from -R options / _CoqProject *)
+ iload_path : Mltop.coq_path list;
+
+ (* Require [require_libs] before the initial state is
+ ready. Parameters follow [Library], that is to say,
+ [lib,prefix,import_export] means require library [lib] from
+ optional [prefix] and [import_export] if [Some false/Some true]
+ is used. *)
+ require_libs : (string * string option * bool option) list;
+
+ (* STM options that apply to the current document. *)
+ stm_options : AsyncOpts.stm_opt;
+}
+(* fb_handler : Feedback.feedback -> unit; *)
+
+(** The type of a STM document *)
+type doc
+
+(** [init_core] performs some low-level initalization; should go away
+ in future releases. *)
+val init_core : unit -> unit
+
+(** [new_doc opt] Creates a new document with options [opt] *)
+val new_doc : stm_init_options -> doc * Stateid.t
+
+(** [parse_sentence sid entry pa] Reads a sentence from [pa] with parsing state
+ [sid] and non terminal [entry]. [entry] receives in input the current proof
+ mode. [sid] should be associated with a valid parsing state (which may not
+ be the case if an error was raised at parsing time). *)
+val parse_sentence :
+ doc:doc -> Stateid.t ->
+ entry:(Pvernac.proof_mode option -> 'a Pcoq.Entry.t) -> Pcoq.Parsable.t -> 'a
+
+(* Reminder: A parsable [pa] is constructed using
+ [Pcoq.Parsable.t stream], where [stream : char Stream.t]. *)
+
+(* [add ~ontop ?newtip verbose cmd] adds a new command [cmd] ontop of
+ the state [ontop].
+ The [ontop] parameter just asserts that the GUI is on
+ sync, but it will eventually call edit_at on the fly if needed.
+ If [newtip] is provided, then the returned state id is guaranteed
+ to be [newtip] *)
+val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t ->
+ bool -> Vernacexpr.vernac_control CAst.t ->
+ doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
+
+(* Returns the proof state before the last tactic that was applied at or before
+the specified state AND that has differences in the underlying proof (i.e.,
+ignoring proofview-only changes). Used to compute proof diffs. *)
+val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option
+
+(* [query at ?report_with cmd] Executes [cmd] at a given state [at],
+ throwing away side effects except messages. Feedback will
+ be sent with [report_with], which defaults to the dummy state id *)
+val query : doc:doc ->
+ at:Stateid.t -> route:Feedback.route_id -> Pcoq.Parsable.t -> 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].
+ If Flags.async_proofs_full is set, then [id] is not [observe]d, else it is.
+*)
+type focus = { start : Stateid.t; stop : Stateid.t; tip : Stateid.t }
+val edit_at : doc:doc -> Stateid.t -> doc * [ `NewTip | `Focus of focus ]
+
+(* [observe doc sid]] Check / execute span [sid] *)
+val observe : doc:doc -> Stateid.t -> doc
+
+(* [finish doc] Fully checks a document up to the "current" tip. *)
+val finish : doc:doc -> doc
+
+(* Internal use (fake_ide) only, do not use *)
+val wait : doc:doc -> doc
+
+val stop_worker : string -> unit
+
+(* Joins the entire document. Implies finish, but also checks proofs *)
+val join : doc:doc -> doc
+
+(* Saves on the disk a .vio corresponding to the current status:
+ - if the worker pool 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 failure) *)
+val snapshot_vio : doc:doc -> output_native_objects:bool -> DirPath.t -> string -> doc
+
+(* 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 : doc:doc -> Stateid.t
+val get_ldir : doc:doc -> Names.DirPath.t
+
+(* This returns the node at that position *)
+val get_ast : doc:doc -> Stateid.t -> (Vernacexpr.vernac_control Loc.located) option
+
+(* Filename *)
+val set_compilation_hints : string -> unit
+
+(* Reorders the task queue putting forward what is in the perspective *)
+val set_perspective : doc:doc -> Stateid.t list -> unit
+
+(** workers **************************************************************** **)
+
+module ProofTask : AsyncTaskQueue.Task
+module TacTask : AsyncTaskQueue.Task
+module QueryTask : AsyncTaskQueue.Task
+
+(** document structure customization *************************************** **)
+
+(* A proof block delimiter defines a syntactic delimiter for sub proofs
+ that, when contain an error, do not impact the rest of the proof.
+ While checking a proof, if an error occurs in a (valid) block then
+ processing can skip the entire block and go on to give feedback
+ on the rest of the proof.
+
+ static_block_detection and dynamic_block_validation are run when
+ the closing block marker is parsed/executed respectively.
+
+ static_block_detection is for example called when "}" is parsed and
+ declares a block containing all proof steps between it and the matching
+ "{".
+
+ dynamic_block_validation is called when an error "crosses" the "}" statement.
+ Depending on the nature of the goal focused by "{" the block may absorb the
+ error or not. For example if the focused goal occurs in the type of
+ another goal, then the block is leaky.
+ Note that one can design proof commands that need no dynamic validation.
+
+ Example of document:
+
+ .. { tac1. tac2. } ..
+
+ Corresponding DAG:
+
+ .. (3) <-- { -- (4) <-- tac1 -- (5) <-- tac2 -- (6) <-- } -- (7) ..
+
+ Declaration of block [-------------------------------------------]
+
+ start = 5 the first state_id that could fail in the block
+ stop = 7 the node that may absorb the error
+ dynamic_switch = 4 dynamic check on this node
+ carry_on_data = () no need to carry extra data from static to dynamic
+ checks
+*)
+
+module DynBlockData : Dyn.S
+
+type static_block_declaration = {
+ block_start : Stateid.t;
+ block_stop : Stateid.t;
+ dynamic_switch : Stateid.t;
+ carry_on_data : DynBlockData.t;
+}
+
+type document_node = {
+ indentation : int;
+ ast : Vernacexpr.vernac_control;
+ id : Stateid.t;
+}
+
+type document_view = {
+ entry_point : document_node;
+ prev_node : document_node -> document_node option;
+}
+
+type static_block_detection =
+ document_view -> static_block_declaration option
+
+type recovery_action = {
+ base_state : Stateid.t;
+ goals_to_admit : Goal.goal list;
+ recovery_command : Vernacexpr.vernac_control option;
+}
+
+type dynamic_block_error_recovery =
+ doc -> static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ]
+
+val register_proof_block_delimiter :
+ Vernacextend.proof_block_name ->
+ static_block_detection ->
+ dynamic_block_error_recovery ->
+ unit
+
+(** 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 : (doc:doc -> Stateid.t -> in_cache:bool -> unit) Hook.t
+val unreachable_state_hook :
+ (doc:doc -> Stateid.t -> Exninfo.iexn -> unit) Hook.t
+
+(* ready means that master has it at hand *)
+val state_ready_hook : (doc:doc -> Stateid.t -> unit) Hook.t
+
+(* Messages from the workers to the master *)
+val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t
+
+val get_doc : Feedback.doc_id -> doc
+
+val state_of_id : doc:doc ->
+ Stateid.t -> [ `Valid of Vernacstate.t option | `Expired | `Error of exn ]
+
+(* Queries for backward compatibility *)
+val current_proof_depth : doc:doc -> int
+val get_all_proof_names : doc:doc -> Id.t list
+
+(** Enable STM debugging *)
+val stm_debug : bool ref
+
+type document
+val backup : unit -> document
+val restore : document -> unit
diff --git a/stm/stm.mllib b/stm/stm.mllib
new file mode 100644
index 0000000000..4b254e8113
--- /dev/null
+++ b/stm/stm.mllib
@@ -0,0 +1,11 @@
+Spawned
+Dag
+Vcs
+TQueue
+WorkerPool
+Vernac_classifier
+CoqworkmgrApi
+AsyncTaskQueue
+Stm
+ProofBlockDelimiter
+Vio_checking
diff --git a/stm/tQueue.ml b/stm/tQueue.ml
new file mode 100644
index 0000000000..33744e7323
--- /dev/null
+++ b/stm/tQueue.ml
@@ -0,0 +1,155 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+module PriorityQueue : sig
+ type 'a t
+ val create : unit -> '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
+ val length : 'a t -> int
+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)
+ let length ({ contents = (l, _) }) = List.length l
+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 broadcast { 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 CErrors.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 length { queue = q; lock = m } =
+ Mutex.lock m;
+ let n = PriorityQueue.length q in
+ Mutex.unlock m;
+ n
+
+let clear { queue = q; lock = m; cond = c } =
+ Mutex.lock m;
+ PriorityQueue.clear q;
+ Mutex.unlock m
+
+let clear_saving { queue = q; lock = m; cond = c } f =
+ Mutex.lock m;
+ let saved = ref [] in
+ while not (PriorityQueue.is_empty q) do
+ let elem = PriorityQueue.pop q in
+ match f elem with
+ | Some x -> saved := x :: !saved
+ | None -> ()
+ done;
+ Mutex.unlock m;
+ List.rev !saved
+
+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 0000000000..e098c37f2a
--- /dev/null
+++ b/stm/tQueue.mli
@@ -0,0 +1,35 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* Thread safe queue with some extras *)
+
+type 'a t
+val create : unit -> '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
+
+(* Wake up all waiting threads *)
+val broadcast : 'a t -> unit
+
+(* Non destructive *)
+val wait_until_n_are_waiting_then_snapshot : int -> 'a t -> 'a list
+
+val clear : 'a t -> unit
+val clear_saving : 'a t -> ('a -> 'b option) -> 'b list
+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
+
+val length : 'a t -> int
diff --git a/stm/vcs.ml b/stm/vcs.ml
new file mode 100644
index 0000000000..4bd46286bd
--- /dev/null
+++ b/stm/vcs.ml
@@ -0,0 +1,190 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Pp
+open CErrors
+
+module type S = sig
+
+ module Branch :
+ sig
+ type t
+ val make : string -> 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,'property_data) t constraint 'kind = [> `Master ]
+
+ val empty : id -> ('kind,'diff,'info,'property_data) t
+
+ val current_branch : ('k,'e,'i,'c) t -> Branch.t
+ val branches : ('k,'e,'i,'c) t -> Branch.t list
+
+ val get_branch : ('k,'e,'i,'c) t -> Branch.t -> 'k branch_info
+ val reset_branch : ('k,'e,'i,'c) t -> Branch.t -> id -> ('k,'e,'i,'c) t
+ val branch :
+ ('kind,'e,'i,'c) t -> ?root:id -> ?pos:id ->
+ Branch.t -> 'kind -> ('kind,'e,'i,'c) t
+ val delete_branch : ('k,'e,'i,'c) t -> Branch.t -> ('k,'e,'i,'c) t
+ val merge :
+ ('k,'diff,'i,'c) t -> id -> ours:'diff -> theirs:'diff -> ?into:Branch.t ->
+ Branch.t -> ('k,'diff,'i,'c) t
+ val commit : ('k,'diff,'i,'c) t -> id -> 'diff -> ('k,'diff,'i,'c) t
+ val rewrite_merge :
+ ('k,'diff,'i,'c) t -> id -> ours:'diff -> theirs:'diff -> at:id ->
+ Branch.t -> ('k,'diff,'i,'c) t
+ val checkout : ('k,'e,'i,'c) t -> Branch.t -> ('k,'e,'i,'c) t
+
+ val set_info : ('k,'e,'info,'c) t -> id -> 'info -> ('k,'e,'info,'c) t
+ val get_info : ('k,'e,'info,'c) t -> id -> 'info option
+
+ (* Read only dag *)
+ module Dag : Dag.S with type node = id
+ val dag : ('kind,'diff,'info,'cdata) t -> ('diff,'info,'cdata) Dag.t
+
+ val create_property : ('k,'e,'i,'c) t -> id list -> 'c -> ('k,'e,'i,'c) t
+ val property_of : ('k,'e,'i,'c) t -> id -> 'c Dag.Property.t list
+ val delete_property : ('k,'e,'i,'c) t -> 'c Dag.Property.t -> ('k,'e,'i,'c) t
+
+ (* Removes all unreachable nodes and returns them *)
+ val gc : ('k,'e,'info,'c) t -> ('k,'e,'info,'c) t * Dag.NodeSet.t
+ val reachable : ('k,'e,'info,'c) t -> id -> Dag.NodeSet.t
+
+end
+
+module Make(OT : Map.OrderedType) = struct
+
+module Dag = Dag.Make(OT)
+
+type id = OT.t
+
+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,'property_data) t = {
+ cur_branch : Branch.t;
+ heads : 'kind branch_info BranchMap.t;
+ dag : ('edge,'info,'property_data) 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_property vcs l i = { vcs with dag = Dag.create_property vcs.dag l i }
+let property_of vcs i = Dag.property_of vcs.dag i
+let delete_property vcs c = { vcs with dag = Dag.del_property vcs.dag c }
+
+let branches vcs = BranchMap.fold (fun x _ accu -> x :: accu) vcs.heads []
+let dag vcs = vcs.dag
+
+let rec closure s d n =
+ let l = try Dag.from_node d n with Not_found -> [] in
+ List.fold_left (fun s (n',_) ->
+ if Dag.NodeSet.mem n' s then s
+ else closure s d n')
+ (Dag.NodeSet.add n s) l
+
+let reachable vcs i = closure Dag.NodeSet.empty vcs.dag i
+
+let gc vcs =
+ let alive =
+ BranchMap.fold (fun b { pos } s -> closure s vcs.dag pos)
+ vcs.heads Dag.NodeSet.empty in
+ let dead = Dag.NodeSet.diff (Dag.all_nodes vcs.dag) alive in
+ { vcs with dag = Dag.del_nodes vcs.dag dead }, dead
+
+end
diff --git a/stm/vcs.mli b/stm/vcs.mli
new file mode 100644
index 0000000000..47622ef6f1
--- /dev/null
+++ b/stm/vcs.mli
@@ -0,0 +1,98 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* This module builds a VCS like interface on top of Dag, used to build
+ a Dag instance by the State Transaction Machine.
+
+ This data structure does not hold system states:
+ - Edges are meant to hold a diff.
+ The delta between two states, or equivalent data like a vernac_expr whose
+ execution corresponds to the application of the diff.
+ - Nodes are empty, unless one adds explicit info.
+ The info could be a system state, obtaind by applying all the diffs
+ from the initial state, but is not necessarily there.
+ As a consequence, "checkout" just updates the current branch.
+
+ The type [id] is the type of commits (a node in the dag)
+ The type [Vcs.t] has 4 parameters:
+ ['info] data attached to a node (like a system state)
+ ['diff] data attached to an edge (the commit content, a "patch")
+ ['kind] extra data attached to a branch (like being the master branch)
+ ['cdata] extra data hold by dag properties
+*)
+
+module type S = sig
+
+ module Branch :
+ sig
+ type t
+ val make : string -> 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,'property_data) t constraint 'kind = [> `Master ]
+
+ val empty : id -> ('kind,'diff,'info,'property_data) t
+
+ val current_branch : ('k,'e,'i,'c) t -> Branch.t
+ val branches : ('k,'e,'i,'c) t -> Branch.t list
+
+ val get_branch : ('k,'e,'i,'c) t -> Branch.t -> 'k branch_info
+ val reset_branch : ('k,'e,'i,'c) t -> Branch.t -> id -> ('k,'e,'i,'c) t
+ val branch :
+ ('kind,'e,'i,'c) t -> ?root:id -> ?pos:id ->
+ Branch.t -> 'kind -> ('kind,'e,'i,'c) t
+ val delete_branch : ('k,'e,'i,'c) t -> Branch.t -> ('k,'e,'i,'c) t
+ val merge :
+ ('k,'diff,'i,'c) t -> id -> ours:'diff -> theirs:'diff -> ?into:Branch.t ->
+ Branch.t -> ('k,'diff,'i,'c) t
+ val commit : ('k,'diff,'i,'c) t -> id -> 'diff -> ('k,'diff,'i,'c) t
+ val rewrite_merge :
+ ('k,'diff,'i,'c) t -> id -> ours:'diff -> theirs:'diff -> at:id ->
+ Branch.t -> ('k,'diff,'i,'c) t
+ val checkout : ('k,'e,'i,'c) t -> Branch.t -> ('k,'e,'i,'c) t
+
+ val set_info : ('k,'e,'info,'c) t -> id -> 'info -> ('k,'e,'info,'c) t
+ val get_info : ('k,'e,'info,'c) t -> id -> 'info option
+
+ (* Read only dag *)
+ module Dag : Dag.S with type node = id
+ val dag : ('kind,'diff,'info,'cdata) t -> ('diff,'info,'cdata) Dag.t
+
+ (* Properties are not a concept typical of a VCS, but a useful metadata
+ * of a DAG (or graph). *)
+ val create_property : ('k,'e,'i,'c) t -> id list -> 'c -> ('k,'e,'i,'c) t
+ val property_of : ('k,'e,'i,'c) t -> id -> 'c Dag.Property.t list
+ val delete_property : ('k,'e,'i,'c) t -> 'c Dag.Property.t -> ('k,'e,'i,'c) t
+
+ (* Removes all unreachable nodes and returns them *)
+ val gc : ('k,'e,'info,'c) t -> ('k,'e,'info,'c) t * Dag.NodeSet.t
+ val reachable : ('k,'e,'info,'c) t -> id -> Dag.NodeSet.t
+
+
+end
+
+module Make(OT : Map.OrderedType) : S
+with type id = OT.t
+and type Dag.node = OT.t
+and type Dag.NodeSet.t = Set.Make(OT).t
+and type Dag.NodeSet.elt = OT.t
+
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
new file mode 100644
index 0000000000..243b5c333d
--- /dev/null
+++ b/stm/vernac_classifier.ml
@@ -0,0 +1,219 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open CErrors
+open Util
+open Pp
+open CAst
+open Vernacextend
+open Vernacexpr
+
+let string_of_parallel = function
+ | `Yes (solve,abs) ->
+ "par" ^ if solve then "solve" else "" ^ if abs then "abs" else ""
+ | `No -> ""
+
+let string_of_vernac_type = function
+ | VtUnknown -> "Unknown"
+ | VtStartProof _ -> "StartProof"
+ | VtSideff _ -> "Sideff"
+ | VtQed (VtKeep VtKeepAxiom) -> "Qed(admitted)"
+ | VtQed (VtKeep (VtKeepOpaque | VtKeepDefined)) -> "Qed(keep)"
+ | VtQed VtDrop -> "Qed(drop)"
+ | VtProofStep { parallel; proof_block_detection } ->
+ "ProofStep " ^ string_of_parallel parallel ^
+ Option.default "" proof_block_detection
+ | VtQuery -> "Query"
+ | VtMeta -> "Meta "
+ | VtProofMode _ -> "Proof Mode"
+
+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 vtkeep_of_opaque = let open Proof_global in function
+ | Opaque -> VtKeepOpaque
+ | Transparent -> VtKeepDefined
+
+let idents_of_name : Names.Name.t -> Names.Id.t list =
+ function
+ | Names.Anonymous -> []
+ | Names.Name n -> [n]
+
+let stm_allow_nested_proofs_option_name = ["Nested";"Proofs";"Allowed"]
+
+let options_affecting_stm_scheduling =
+ [ Attributes.universe_polymorphism_option_name;
+ stm_allow_nested_proofs_option_name;
+ Vernacentries.proof_mode_opt_name;
+ Attributes.program_mode_option_name;
+ Proof_using.proof_using_opt_name;
+ ]
+
+let classify_vernac e =
+ let static_classifier ~poly e = match e with
+ (* Univ poly compatibility: we run it now, so that we can just
+ * look at Flags in stm.ml. Would be nicer to have the stm
+ * look at the entire dag to detect this option. *)
+ | VernacSetOption (_, l,_)
+ when CList.exists (CList.equal String.equal l)
+ options_affecting_stm_scheduling ->
+ VtSideff [], VtNow
+ (* Qed *)
+ | VernacAbort _ -> VtQed VtDrop, VtLater
+ | VernacEndProof Admitted -> VtQed (VtKeep VtKeepAxiom), VtLater
+ | VernacEndProof (Proved (opaque,_)) -> VtQed (VtKeep (vtkeep_of_opaque opaque)), VtLater
+ | VernacExactProof _ -> VtQed (VtKeep VtKeepOpaque), VtLater
+ (* Query *)
+ | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _
+ | VernacCheckMayEval _ -> VtQuery, VtLater
+ (* ProofStep *)
+ | VernacProof _
+ | VernacFocus _ | VernacUnfocus
+ | VernacSubproof _
+ | VernacCheckGuard
+ | VernacUnfocused
+ | VernacSolveExistential _ ->
+ VtProofStep { parallel = `No; proof_block_detection = None }, VtLater
+ | VernacBullet _ ->
+ VtProofStep { parallel = `No; proof_block_detection = Some "bullet" },
+ VtLater
+ | VernacEndSubproof ->
+ VtProofStep { parallel = `No;
+ proof_block_detection = Some "curly" },
+ VtLater
+ (* StartProof *)
+ | VernacDefinition ((Decl_kinds.DoDischarge,_),({v=i},_),ProveBody _) ->
+ VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i), VtLater
+
+ | VernacDefinition (_,({v=i},_),ProveBody _) ->
+ let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
+ VtStartProof(guarantee, idents_of_name i), VtLater
+ | VernacStartTheoremProof (_,l) ->
+ let ids = List.map (fun (({v=i}, _), _) -> i) l in
+ let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
+ VtStartProof (guarantee,ids), VtLater
+ | VernacFixpoint (discharge,l) ->
+ let guarantee =
+ if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity
+ else GuaranteesOpacity
+ in
+ let ids, open_proof =
+ List.fold_left (fun (l,b) ((({v=id},_),_,_,_,p),_) ->
+ id::l, b || p = None) ([],false) l in
+ if open_proof
+ then VtStartProof (guarantee,ids), VtLater
+ else VtSideff ids, VtLater
+ | VernacCoFixpoint (discharge,l) ->
+ let guarantee =
+ if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity
+ else GuaranteesOpacity
+ in
+ let ids, open_proof =
+ List.fold_left (fun (l,b) ((({v=id},_),_,_,p),_) ->
+ id::l, b || p = None) ([],false) l in
+ if open_proof
+ then VtStartProof (guarantee,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 (fun (id, _) -> id.v) l) l) in
+ VtSideff ids, VtLater
+ | VernacPrimitive (id,_,_) ->
+ VtSideff [id.CAst.v], VtLater
+ | VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id), VtLater
+ | VernacInductive (_, _,_,l) ->
+ let ids = List.map (fun (((_,({v=id},_)),_,_,_,cl),_) -> id :: match cl with
+ | Constructors l -> List.map (fun (_,({v=id},_)) -> id) l
+ | RecordDecl (oid,l) -> (match oid with Some {v=x} -> [x] | _ -> []) @
+ CList.map_filter (function
+ | ((_,AssumExpr({v=Names.Name n},_)),_),_ -> Some n
+ | _ -> None) l) l in
+ VtSideff (List.flatten ids), VtLater
+ | VernacScheme l ->
+ let ids = List.map (fun {v}->v) (CList.map_filter (fun (x,_) -> x) l) in
+ VtSideff ids, VtLater
+ | VernacCombinedScheme ({v=id},_) -> VtSideff [id], VtLater
+ | VernacBeginSection {v=id} -> VtSideff [id], VtLater
+ | VernacUniverse _ | VernacConstraint _
+ | VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _
+ | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _
+ | VernacChdir _
+ | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _
+ | VernacArguments _
+ | VernacReserve _
+ | VernacGeneralizable _
+ | VernacSetOpacity _ | VernacSetStrategy _
+ | VernacSetOption _
+ | VernacAddOption _ | VernacRemoveOption _
+ | VernacMemOption _ | VernacPrintOption _
+ | VernacGlobalCheck _
+ | VernacDeclareReduction _
+ | VernacExistingClass _ | VernacExistingInstance _
+ | VernacRegister _
+ | VernacNameSectionHypSet _
+ | VernacComments _
+ | VernacDeclareInstance _ -> 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,{v=id},bl,_)
+ | VernacDefineModule (exp,{v=id},bl,_,_) ->
+ VtSideff [id], if bl = [] && exp = None then VtLater else VtNow
+ | VernacDeclareModuleType ({v=id},bl,_,_) ->
+ VtSideff [id], if bl = [] then VtLater else VtNow
+ (* These commands alter the parser *)
+ | VernacDeclareCustomEntry _
+ | VernacOpenCloseScope _ | VernacDeclareScope _
+ | VernacDelimiters _ | VernacBindScope _
+ | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _
+ | VernacSyntaxExtension _
+ | VernacSyntacticDefinition _
+ | VernacRequire _ | VernacImport _ | VernacInclude _
+ | VernacDeclareMLModule _
+ | VernacContext _ (* TASSI: unsure *) -> VtSideff [], VtNow
+ | VernacProofMode pm -> VtProofMode pm, VtNow
+ (* These are ambiguous *)
+ | VernacInstance _ -> VtUnknown, VtNow
+ (* Stm will install a new classifier to handle these *)
+ | VernacBack _ | VernacAbortAll
+ | VernacUndoTo _ | VernacUndo _
+ | VernacResetName _ | VernacResetInitial
+ | VernacBackTo _ | VernacRestart -> VtMeta, VtNow
+ (* What are these? *)
+ | VernacRestoreState _
+ | VernacWriteState _ -> VtSideff [], VtNow
+ (* Plugins should classify their commands *)
+ | VernacExtend (s,l) ->
+ try Vernacextend.get_vernac_classifier s l
+ with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
+ in
+ let rec static_control_classifier = function
+ | VernacExpr (f, e) ->
+ let poly = Attributes.(parse_drop_extra polymorphic_nowarn f) in
+ static_classifier ~poly e
+ | VernacTimeout (_,{v=e}) -> static_control_classifier e
+ | VernacTime (_,{v=e}) | VernacRedirect (_, {v=e}) ->
+ static_control_classifier e
+ | VernacFail {v=e} -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
+ (match static_control_classifier e with
+ | ( VtQuery | VtProofStep _ | VtSideff _
+ | VtMeta), _ as x -> x
+ | VtQed _, _ ->
+ VtProofStep { parallel = `No; proof_block_detection = None },
+ VtLater
+ | (VtStartProof _ | VtUnknown | VtProofMode _), _ -> VtQuery, VtLater)
+ in
+ static_control_classifier e
diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli
new file mode 100644
index 0000000000..9d93ad1f39
--- /dev/null
+++ b/stm/vernac_classifier.mli
@@ -0,0 +1,19 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Vernacextend
+
+val string_of_vernac_classification : vernac_classification -> string
+
+(** What does a vernacular do *)
+val classify_vernac : Vernacexpr.vernac_control -> vernac_classification
+
+(** *)
+val stm_allow_nested_proofs_option_name : string list
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
new file mode 100644
index 0000000000..69c1d9bd23
--- /dev/null
+++ b/stm/vio_checking.ml
@@ -0,0 +1,153 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Util
+
+let check_vio (ts,f) =
+ Dumpglob.noglob ();
+ let long_f_dot_v, _, _, _, _, tasks, _ = Library.load_library_todo f in
+ Stm.set_compilation_hints long_f_dot_v;
+ List.fold_left (fun acc ids -> Stm.check_task f tasks ids && acc) true ts
+
+module Worker = Spawn.Sync ()
+
+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 CErrors.user_err Pp.(str "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 String.length s > 0 && 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;
+ Worker.kill (Pool.find pid !pool);
+ pool := Pool.remove pid !pool;
+ done;
+ exit !rc
+
+let schedule_vio_compilation j fs =
+ if j < 1 then CErrors.user_err Pp.(str "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 = Loadpath.locate_file (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 "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 String.length s > 0 && 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 all_jobs = !jobs 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;
+ Worker.kill (Pool.find pid !pool);
+ pool := Pool.remove pid !pool;
+ done;
+ if !rc = 0 then begin
+ (* set the access and last modification time of all files to the same t
+ * not to confuse make into thinking that some of them are outdated *)
+ let t = Unix.gettimeofday () in
+ List.iter (fun (f,_) -> Unix.utimes (f^".vo") t t) all_jobs;
+ end;
+ exit !rc
+
+
diff --git a/stm/vio_checking.mli b/stm/vio_checking.mli
new file mode 100644
index 0000000000..177b3b2d06
--- /dev/null
+++ b/stm/vio_checking.mli
@@ -0,0 +1,15 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(* [check_vio tasks file] checks the [tasks] stored in [file] *)
+val check_vio : int list * string -> 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 0000000000..2432e72c8a
--- /dev/null
+++ b/stm/workerPool.ml
@@ -0,0 +1,130 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+type worker_id = string
+
+type 'a cpanel = {
+ exit : unit -> 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 CErrors.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 CErrors.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 = CThread.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 0000000000..0f1237b584
--- /dev/null
+++ b/stm/workerPool.mli
@@ -0,0 +1,48 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+type worker_id = string
+
+type 'a cpanel = {
+ exit : unit -> 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 23:32:27 +0000