Imported Upstream version 8.5~beta1+dfsg

31 files changed, 5857 insertions, 0 deletions

diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
new file mode 100644
index 00000000..672527d9
--- /dev/null
+++ b/stm/asyncTaskQueue.ml
@@ -0,0 +1,344 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Errors
+open Pp
+open Util
+
+let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr
+
+let prerr_endline s = if !Flags.debug then begin pr_err s end else ()
+
+type 'a worker_status = [ `Fresh | `Old of 'a ]
+
+module type Task = sig
+
+  type task
+  type 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 : competence worker_status -> task -> request option
+  val task_match : competence worker_status -> task -> bool
+  val use_response :
+    competence worker_status -> task -> response ->
+      [ `Stay of competence * task list | `End ]
+  val on_marshal_error : string -> task -> unit
+  val on_task_cancellation_or_expiration_or_slave_death : task option -> unit
+  val forward_feedback : Feedback.feedback -> unit
+ 
+  (* run by the worker *)
+  val perform : request -> response
+
+  (* debugging *)
+  val name_of_task : task -> string
+  val name_of_request : request -> string
+
+end
+
+type expiration = bool ref
+
+module Make(T : Task) = struct
+
+  exception Die
+  type response =
+    | Response of T.response
+    | RespFeedback of Feedback.feedback
+    | RespGetCounterNewUnivLevel
+  type request = Request of T.request
+
+  type more_data =
+    | MoreDataUnivLevel of Univ.universe_level list
+ 
+  let request_expiry_of_task (t, c) = T.request_of_task t, c
+  
+  let slave_respond (Request r) =
+    let res = T.perform r in
+    Response res
+
+  exception MarshalError of string
+  
+  let marshal_to_channel oc data =
+    Marshal.to_channel oc data [];
+    flush oc
+  
+  let marshal_err s = raise (MarshalError s)
+  
+  let marshal_request oc (req : request) =
+    try marshal_to_channel oc req
+    with Failure s | Invalid_argument s | Sys_error s ->
+      marshal_err ("marshal_request: "^s)
+  
+  let unmarshal_request ic =
+    try (CThread.thread_friendly_input_value ic : request)
+    with Failure s | Invalid_argument s | Sys_error s ->
+      marshal_err ("unmarshal_request: "^s)
+  
+  let marshal_response oc (res : response) =
+    try marshal_to_channel oc res
+    with Failure s | Invalid_argument s | Sys_error s ->
+      marshal_err ("marshal_response: "^s)
+  
+  let unmarshal_response ic =
+    try (CThread.thread_friendly_input_value ic : response)
+    with Failure s | Invalid_argument s | Sys_error s ->
+      marshal_err ("unmarshal_response: "^s)
+  
+  let marshal_more_data oc (res : more_data) =
+    try marshal_to_channel oc res
+    with Failure s | Invalid_argument s | Sys_error s ->
+      marshal_err ("marshal_more_data: "^s)
+  
+  let unmarshal_more_data ic =
+    try (CThread.thread_friendly_input_value ic : more_data)
+    with Failure s | Invalid_argument s | Sys_error s ->
+      marshal_err ("unmarshal_more_data: "^s)
+
+  let report_status ?(id = !Flags.async_proofs_worker_id) s =
+    Pp.feedback ~state_id:Stateid.initial (Feedback.WorkerStatus(id, s))
+
+  module Worker = Spawn.Sync(struct end)
+
+  module Model = struct
+
+  type process = Worker.process
+  type extra = (T.task * expiration) TQueue.t
+
+  let spawn id =
+    let name = Printf.sprintf "%s:%d" !T.name id in
+    let proc, ic, oc =
+      let rec set_slave_opt = function
+        | [] -> !Flags.async_proofs_flags_for_workers @
+                ["-toploop"; !T.name^"top";
+                 "-worker-id"; name;
+                 "-async-proofs-worker-priority";
+                   Flags.string_of_priority !Flags.async_proofs_worker_priority]
+        | ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl
+        | ("-async-proofs" |"-toploop" |"-vi2vo" |"-compile"
+          |"-load-vernac-source" |"-compile-verbose"
+          |"-async-proofs-worker-priority" |"-worker-id") :: _ :: tl ->
+          set_slave_opt tl
+        | x::tl -> x :: set_slave_opt tl in
+      let args =
+        Array.of_list (set_slave_opt (List.tl (Array.to_list Sys.argv))) in
+      let env = Array.append (T.extra_env ()) (Unix.environment ()) in
+    Worker.spawn ~env Sys.argv.(0) args in
+    name, proc, CThread.prepare_in_channel_for_thread_friendly_io ic, oc
+
+  let manager cpanel (id, proc, ic, oc) =
+    let { WorkerPool.extra = queue; exit; cancelled } = cpanel in
+    let exit () =  report_status ~id "Dead"; exit () in
+    let last_task = ref None in
+    let worker_age = ref `Fresh in
+    let got_token = ref false in
+    let giveback_exec_token () =
+      if !got_token then (CoqworkmgrApi.giveback 1; got_token := false) in
+    let stop_waiting = ref false in
+    let expiration_date = ref (ref false) in
+    let pick_task () =
+      prerr_endline "waiting for a task";
+      let pick age (t, c) = not !c && T.task_match age t in
+      let task, task_expiration =
+        TQueue.pop ~picky:(pick !worker_age) ~destroy:stop_waiting queue in
+      expiration_date := task_expiration;
+      last_task := Some task;
+      prerr_endline ("got task: "^T.name_of_task task);
+      task in
+    let add_tasks l =
+      List.iter (fun t -> TQueue.push queue (t,!expiration_date)) l in
+    let get_exec_token () =
+      ignore(CoqworkmgrApi.get 1);
+      got_token := true;
+      prerr_endline ("got execution token") in
+    let kill proc =
+      Worker.kill proc;
+      prerr_endline ("Worker exited: " ^
+        match Worker.wait proc with
+        | Unix.WEXITED 0x400 -> "exit code unavailable"
+        | Unix.WEXITED i -> Printf.sprintf "exit(%d)" i
+        | Unix.WSIGNALED sno -> Printf.sprintf "signalled(%d)" sno
+        | Unix.WSTOPPED sno -> Printf.sprintf "stopped(%d)" sno) in
+    let more_univs n =
+      CList.init 10 (fun _ ->
+        Universes.new_univ_level (Global.current_dirpath ())) in
+
+    let rec kill_if () =
+      if not (Worker.is_alive proc) then ()
+      else if cancelled () || !(!expiration_date) then
+        let () = stop_waiting := true in
+        let () = TQueue.signal_destruction queue in
+        Worker.kill proc
+      else
+        let () = Unix.sleep 1 in
+        kill_if ()
+    in
+    let _ = Thread.create kill_if () in
+
+    try while true do
+      report_status ~id "Idle";
+      let task = pick_task () in
+      match T.request_of_task !worker_age task with
+      | None -> prerr_endline ("Task expired: " ^ T.name_of_task task)
+      | Some req ->
+      try
+        get_exec_token ();
+        marshal_request oc (Request req);
+        let rec continue () =
+          match unmarshal_response ic with
+          | RespGetCounterNewUnivLevel ->
+              marshal_more_data oc (MoreDataUnivLevel (more_univs 10));
+              continue ()
+          | RespFeedback fbk -> T.forward_feedback fbk; continue ()
+          | Response resp ->
+              match T.use_response !worker_age task resp with
+              | `End -> raise Die
+              | `Stay(competence, new_tasks) ->
+                   last_task := None;
+                   giveback_exec_token ();
+                   worker_age := `Old competence;
+                   add_tasks new_tasks
+        in
+          continue ()
+      with
+      | (Sys_error _|Invalid_argument _|End_of_file|Die) as e ->
+          raise e (* we pass the exception to the external handler *)
+      | MarshalError s -> T.on_marshal_error s task; raise Die
+      | e ->
+          pr_err ("Uncaught exception in worker manager: "^
+            string_of_ppcmds (print e));
+          flush_all (); raise Die
+    done with
+    | (Die | TQueue.BeingDestroyed) ->
+        giveback_exec_token (); kill proc; exit ()
+    | Sys_error _ | Invalid_argument _ | End_of_file ->
+        giveback_exec_token ();
+        T.on_task_cancellation_or_expiration_or_slave_death !last_task;
+        kill proc;
+        exit ()
+  end
+
+  module Pool = WorkerPool.Make(Model)
+
+  type queue = {
+    active : Pool.pool;
+    queue : (T.task * expiration) TQueue.t;
+    cleaner : Thread.t;
+  }
+
+  let create size =
+    let cleaner queue =
+      while true do
+        try ignore(TQueue.pop ~picky:(fun (_,cancelled) -> !cancelled) queue)
+        with TQueue.BeingDestroyed -> Thread.exit ()
+      done in
+    let queue = TQueue.create () in
+    {
+      active = Pool.create queue ~size;
+      queue;
+      cleaner = Thread.create cleaner queue;
+    }
+  
+  let destroy { active; queue } =
+    Pool.destroy active;
+    TQueue.destroy queue
+
+  let enqueue_task { queue; active } (t, _ as item) =
+    prerr_endline ("Enqueue task "^T.name_of_task t);
+    TQueue.push queue item
+
+  let cancel_worker { active } n = Pool.cancel n active
+
+  let name_of_request (Request r) = T.name_of_request r
+
+  let set_order { queue } cmp =
+    TQueue.set_order queue (fun (t1,_) (t2,_) -> cmp t1 t2)
+
+  let join { queue; active } =
+    if not (Pool.is_empty active) then
+      TQueue.wait_until_n_are_waiting_and_queue_empty
+        (Pool.n_workers active + 1(*cleaner*))
+        queue
+
+  let cancel_all { queue; active } =
+    TQueue.clear queue;
+    Pool.cancel_all active
+
+  let slave_ic = ref None
+  let slave_oc = ref None
+
+  let init_stdout () =
+    let ic, oc = Spawned.get_channels () in
+    slave_oc := Some oc; slave_ic := Some ic
+
+  let bufferize f =
+    let l = ref [] in
+    fun () ->
+      match !l with
+      | [] -> let data = f () in l := List.tl data; List.hd data
+      | x::tl -> l := tl; x
+
+  let slave_handshake () =
+    Pool.worker_handshake (Option.get !slave_ic) (Option.get !slave_oc)
+
+  let main_loop () =
+    let slave_feeder oc fb =
+      Marshal.to_channel oc (RespFeedback fb) []; flush oc in
+    Pp.set_feeder (fun x -> slave_feeder (Option.get !slave_oc) x);
+    Pp.log_via_feedback ();
+    Universes.set_remote_new_univ_level (bufferize (fun () ->
+      marshal_response (Option.get !slave_oc) RespGetCounterNewUnivLevel;
+      match unmarshal_more_data (Option.get !slave_ic) with
+      | MoreDataUnivLevel l -> l));
+    let working = ref false in
+    slave_handshake ();
+    while true do
+      try
+        working := false;
+        let request = unmarshal_request (Option.get !slave_ic) in
+        working := true;
+        report_status (name_of_request request);
+        let response = slave_respond request in
+        report_status "Idle";
+        marshal_response (Option.get !slave_oc) response;
+        Ephemeron.clear ()
+      with
+      | MarshalError s ->
+        pr_err ("Fatal marshal error: " ^ s); flush_all (); exit 2
+      | End_of_file ->
+        prerr_endline "connection lost"; flush_all (); exit 2
+      | e ->
+        pr_err ("Slave: critical exception: " ^ Pp.string_of_ppcmds (print e));
+        flush_all (); exit 1
+    done
+
+  let clear { queue; active } =
+    assert(Pool.is_empty active); (* We allow that only if no slaves *)
+    TQueue.clear queue
+  
+  let snapshot { queue; active } =
+    List.map fst
+     (TQueue.wait_until_n_are_waiting_then_snapshot
+       (Pool.n_workers active) queue)
+
+  let with_n_workers n f =
+    let q = create n in 
+    try let rc = f q in destroy q; rc
+    with e -> let e = Errors.push e in destroy q; iraise e
+
+  let n_workers { active } = Pool.n_workers active
+
+end
+
+module MakeQueue(T : Task) = struct include Make(T) end
+module MakeWorker(T : Task) = struct include Make(T) end
diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli
new file mode 100644
index 00000000..78f295d3
--- /dev/null
+++ b/stm/asyncTaskQueue.mli
@@ -0,0 +1,82 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+type 'a worker_status = [ `Fresh | `Old of 'a ]
+
+module type Task = sig
+
+  type task
+  type 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 : competence worker_status -> task -> request option
+  val task_match : competence worker_status -> task -> bool
+  val use_response :
+    competence worker_status -> task -> response ->
+      [ `Stay of competence * task list | `End ]
+  val on_marshal_error : string -> task -> unit
+  val on_task_cancellation_or_expiration_or_slave_death : task option -> unit
+  val forward_feedback : Feedback.feedback -> unit
+ 
+  (* run by the worker *)
+  val perform : request -> response
+
+  (* debugging *)
+  val name_of_task : task -> string
+  val name_of_request : request -> string
+
+end
+
+type expiration = bool ref
+
+module MakeQueue(T : Task) : sig
+
+  type queue
+
+  (* Number of workers, 0 = lazy local *)
+  val create : int -> queue
+  val destroy : queue -> unit
+
+  val n_workers : queue -> int
+
+  val enqueue_task : queue -> T.task * expiration -> unit
+
+  (* blocking function that waits for the task queue to be empty *)
+  val join : queue -> unit
+  val cancel_all : queue -> unit
+
+  val cancel_worker : queue -> WorkerPool.worker_id -> unit
+
+  val set_order : queue -> (T.task -> T.task -> int) -> unit
+
+  (* Take a snapshot (non destructive but waits until all workers are
+   * enqueued) *)
+  val snapshot : queue -> T.task list
+
+  (* Clears the queue, only if the worker prool is empty *)
+ val clear : queue -> unit
+ 
+  (* create a queue, run the function, destroy the queue.
+   * the user should call join *)
+  val with_n_workers : int -> (queue -> 'a) -> 'a
+
+end
+
+module MakeWorker(T : Task) : sig
+
+  val main_loop : unit -> unit
+  val init_stdout : unit -> unit
+  
+end
diff --git a/stm/coqworkmgrApi.ml b/stm/coqworkmgrApi.ml
new file mode 100644
index 00000000..c34d447e
--- /dev/null
+++ b/stm/coqworkmgrApi.ml
@@ -0,0 +1,140 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+let debug = false
+
+type request =
+  | Hello of Flags.priority
+  | Get of int
+  | TryGet of int
+  | GiveBack of int
+  | Ping
+
+type response =
+  | Tokens of int
+  | Noluck
+  | Pong of int * int * int
+
+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 Flags.Low
+  | [ "HELLO"; "HIGH" ] -> Hello Flags.High
+  | [ "GET"; n ] -> Get (positive_int_of_string n)
+  | [ "TRYGET"; n ] -> TryGet (positive_int_of_string n)
+  | [ "GIVEBACK"; n ] -> GiveBack (positive_int_of_string n)
+  | [ "PING" ] -> Ping
+  | _ -> raise ParseError
+
+let parse_response s =
+  if debug then Printf.eprintf "parsing '%s'\n" s;
+  match Str.split (Str.regexp " ") (strip_r s) with
+  | [ "TOKENS"; n ] -> Tokens (positive_int_of_string n)
+  | [ "NOLUCK" ] -> Noluck
+  | [ "PONG"; n; m; p ] ->
+      let n = try int_of_string n with _ -> raise ParseError in
+      let m = try int_of_string m with _ -> raise ParseError in
+      let p = try int_of_string p with _ -> raise ParseError in
+      Pong (n,m,p)
+  | _ -> raise ParseError
+       
+let print_request = function
+  | Hello Flags.Low -> "HELLO LOW\n"
+  | Hello Flags.High -> "HELLO HIGH\n"
+  | Get n -> Printf.sprintf "GET %d\n" n
+  | TryGet n -> Printf.sprintf "TRYGET %d\n" n
+  | GiveBack n -> Printf.sprintf "GIVEBACK %d\n" n
+  | Ping -> "PING\n"
+
+let print_response = function
+  | Tokens n -> Printf.sprintf "TOKENS %d\n" n
+  | Noluck -> "NOLUCK\n"
+  | Pong (n,m,p) -> Printf.sprintf "PONG %d %d %d\n" n m p
+
+let connect s =
+  try
+    match Str.split (Str.regexp ":") s with
+    | [ h; p ] ->
+        let open Unix in
+        let s = socket PF_INET SOCK_STREAM 0 in
+        connect s (ADDR_INET (inet_addr_of_string h,int_of_string p));
+        Some s
+    | _ -> None
+  with Unix.Unix_error _ -> None
+
+let manager = ref None
+
+let option_map f = function None -> None | Some x -> Some (f x)
+
+let init p =
+  try
+    let sock = Sys.getenv "COQWORKMGR_SOCK" in
+    manager := option_map (fun s -> 
+      let cout = Unix.out_channel_of_descr s in
+      set_binary_mode_out cout true;
+      let cin = Unix.in_channel_of_descr s in
+      set_binary_mode_in cin true;
+      output_string cout (print_request (Hello p)); flush cout;
+      cin, cout) (connect sock)
+  with Not_found | End_of_file -> ()
+
+let with_manager f g =
+  try
+    match !manager with
+    | None -> f ()
+    | Some (cin, cout) -> g cin cout
+  with
+  | ParseError | End_of_file -> manager := None; f ()
+
+let get n =
+  with_manager
+  (fun () ->
+    min n (min !Flags.async_proofs_n_workers !Flags.async_proofs_n_tacworkers))
+  (fun cin cout ->
+    output_string cout (print_request (Get n));
+    flush cout;
+    let l = input_line cin in
+    match parse_response l with
+    | Tokens m -> m
+    | _ -> raise (Failure "coqworkmgr protocol error"))
+
+let tryget n =
+  with_manager
+  (fun () ->
+    Some
+     (min n
+       (min !Flags.async_proofs_n_workers !Flags.async_proofs_n_tacworkers)))
+  (fun cin cout ->
+    output_string cout (print_request (TryGet n));
+    flush cout;
+    let l = input_line cin in
+    match parse_response l with
+    | Tokens m -> Some m
+    | Noluck -> None
+    | _ -> raise (Failure "coqworkmgr protocol error"))
+
+let giveback n =
+  with_manager
+  (fun () -> ())
+  (fun cin cout ->
+    output_string cout (print_request (GiveBack n));
+    flush cout)
+
diff --git a/stm/coqworkmgrApi.mli b/stm/coqworkmgrApi.mli
new file mode 100644
index 00000000..42dd39b9
--- /dev/null
+++ b/stm/coqworkmgrApi.mli
@@ -0,0 +1,44 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* High level api for clients of the service (like coqtop) *)
+
+(* Connects to a work manager if any. If no worker manager, then
+   -async-proofs-j and -async-proofs-tac-j are used *)
+val init : Flags.priority -> unit
+
+(* blocking *)
+val get : int -> int
+
+(* not blocking *)
+val tryget : int -> int option
+val giveback : int -> unit
+
+(* Low level *)
+type request =
+  | Hello of Flags.priority
+  | Get of int
+  | TryGet of int
+  | GiveBack of int
+  | Ping
+
+type response =
+  | Tokens of int
+  | Noluck
+  | Pong of int * int * int (* cur, max, pid *)
+
+val connect : string -> Unix.file_descr option
+
+exception ParseError
+
+(* Intended to be used with input_line and output_string *)
+val parse_request  : string -> request
+val parse_response : string -> response
+
+val print_request  : request -> string
+val print_response : response -> string
diff --git a/stm/dag.ml b/stm/dag.ml
new file mode 100644
index 00000000..d0515d3f
--- /dev/null
+++ b/stm/dag.ml
@@ -0,0 +1,134 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+module type S = sig
+
+  module Cluster :
+  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
+  end
+
+  type node
+  module NodeSet : Set.S with type elt = node
+
+  type ('edge,'info,'cdata) t
+
+  val empty : ('e,'i,'d) t
+
+  val add_edge : ('e,'i,'d) t -> node -> 'e -> node -> ('e,'i,'d) t
+  val from_node : ('e,'i,'d) t -> node -> (node * 'e) list
+  val mem : ('e,'i,'d) t -> node -> bool
+  val del_edge : ('e,'i,'d) t -> node -> node -> ('e,'i,'d) t
+  val del_nodes : ('e,'i,'d) t -> NodeSet.t  -> ('e,'i,'d) t
+  val all_nodes : ('e,'i,'d) t -> NodeSet.t
+
+  val iter : ('e,'i,'d) t ->
+    (node -> 'd Cluster.t option -> 'i option ->
+      (node * 'e) list -> unit) -> unit
+
+  val create_cluster : ('e,'i,'d) t -> node list -> 'd -> ('e,'i,'d) t
+  val cluster_of : ('e,'i,'d) t -> node -> 'd Cluster.t option
+  val del_cluster : ('e,'i,'d) t -> 'd Cluster.t -> ('e,'i,'d) t
+
+  val get_info : ('e,'i,'d) t -> node -> 'i option
+  val set_info : ('e,'i,'d) t -> node -> 'i -> ('e,'i,'d) t
+  val clear_info : ('e,'i,'d) t -> node -> ('e,'i,'d) t
+
+end
+
+module Make(OT : Map.OrderedType) = struct
+
+module Cluster =
+struct
+  type 'd t = 'd * int
+  let equal (_,i1) (_,i2) = Int.equal i1 i2
+  let compare (_,i1) (_,i2) = Int.compare i1 i2
+  let to_string (_,i) = string_of_int i
+  let data (d,_) = d
+end
+
+type node = OT.t
+
+module NodeMap = CMap.Make(OT)
+module NodeSet = Set.Make(OT)
+
+type ('edge,'info,'data) t = {
+  graph : (node * 'edge) list NodeMap.t;
+  clusters : 'data Cluster.t NodeMap.t;
+  infos : 'info NodeMap.t;
+}
+
+let empty = {
+  graph = NodeMap.empty;
+  clusters = NodeMap.empty;
+  infos = NodeMap.empty;
+}
+
+let mem { graph } id = NodeMap.mem id graph
+
+let add_edge dag from trans dest = { dag with
+  graph =
+    try NodeMap.modify from (fun _ arcs -> (dest, trans) :: arcs) dag.graph
+    with Not_found -> NodeMap.add from [dest, trans] dag.graph }
+
+let from_node { graph } id = NodeMap.find id graph
+
+let del_edge dag id tgt = { dag with
+  graph =
+    try
+      let modify _ arcs =
+        let filter (d, _) = OT.compare d tgt <> 0 in
+        List.filter filter arcs
+      in
+      NodeMap.modify id modify dag.graph
+    with Not_found -> dag.graph }
+
+let del_nodes dag s = {
+  infos = NodeMap.filter (fun n _ -> not(NodeSet.mem n s)) dag.infos;
+  clusters = NodeMap.filter (fun n _ -> not(NodeSet.mem n s)) dag.clusters;
+  graph = NodeMap.filter (fun n l ->
+      let drop = NodeSet.mem n s in
+      if not drop then
+        assert(List.for_all (fun (n',_) -> not(NodeSet.mem n' s)) l);
+      not drop)
+    dag.graph }
+
+let clid = ref 1
+let create_cluster dag l data =
+  incr clid;
+  { dag with clusters =
+     List.fold_right (fun x clusters ->
+       NodeMap.add x (data, !clid) clusters) l dag.clusters }
+
+let cluster_of dag id =
+  try Some (NodeMap.find id dag.clusters)
+  with Not_found -> None
+
+let del_cluster dag c =
+  { dag with clusters =
+     NodeMap.filter (fun _ c' -> not (Cluster.equal c' c)) dag.clusters }
+
+let get_info dag id =
+  try Some (NodeMap.find id dag.infos)
+  with Not_found -> None
+
+let set_info dag id info = { dag with infos = NodeMap.add id info dag.infos }
+
+let clear_info dag id = { dag with infos = NodeMap.remove id dag.infos }
+
+let iter dag f =
+  NodeMap.iter (fun k v -> f k (cluster_of dag k) (get_info dag k) v) dag.graph
+
+let all_nodes dag = NodeMap.domain dag.graph
+
+end
+
diff --git a/stm/dag.mli b/stm/dag.mli
new file mode 100644
index 00000000..14ccdc9f
--- /dev/null
+++ b/stm/dag.mli
@@ -0,0 +1,52 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+module type S = sig
+
+  (* A cluster is just a set of nodes.  This set holds some data.
+     Stm uses this to group nodes contribution to the same proofs and
+     that can be evaluated asynchronously *)
+  module Cluster :
+  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
+  end
+
+  type node
+  module NodeSet : Set.S with type elt = node
+
+  type ('edge,'info,'cdata) t
+  
+  val empty : ('e,'i,'d) t
+
+  val add_edge : ('e,'i,'d) t -> node -> 'e -> node -> ('e,'i,'d) t
+  val from_node : ('e,'i,'d) t -> node -> (node * 'e) list
+  val mem : ('e,'i,'d) t -> node -> bool
+  val del_edge : ('e,'i,'d) t -> node -> node -> ('e,'i,'d) t
+  val del_nodes : ('e,'i,'d) t -> NodeSet.t  -> ('e,'i,'d) t
+  val all_nodes : ('e,'i,'d) t -> NodeSet.t
+
+  val iter : ('e,'i,'d) t -> 
+    (node -> 'd Cluster.t option -> 'i option ->
+      (node * 'e) list -> unit) -> unit
+
+  val create_cluster : ('e,'i,'d) t -> node list -> 'd -> ('e,'i,'d) t
+  val cluster_of : ('e,'i,'d) t -> node -> 'd Cluster.t option
+  val del_cluster : ('e,'i,'d) t -> 'd Cluster.t -> ('e,'i,'d) t
+
+  val get_info : ('e,'i,'d) t -> node -> 'i option
+  val set_info : ('e,'i,'d) t -> node -> 'i -> ('e,'i,'d) t
+  val clear_info : ('e,'i,'d) t -> node -> ('e,'i,'d) t
+
+end
+
+module Make(OT : Map.OrderedType) : S with type node = OT.t
+
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
new file mode 100644
index 00000000..f2e68779
--- /dev/null
+++ b/stm/lemmas.ml
@@ -0,0 +1,478 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Created by Hugo Herbelin from contents related to lemma proofs in
+   file command.ml, Aug 2009 *)
+
+open Errors
+open Util
+open Flags
+open Pp
+open Names
+open Term
+open Declarations
+open Declareops
+open Entries
+open Environ
+open Nameops
+open Globnames
+open Decls
+open Decl_kinds
+open Declare
+open Pretyping
+open Termops
+open Namegen
+open Reductionops
+open Constrexpr
+open Constrintern
+open Impargs
+
+type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference -> 'a
+let mk_hook hook = hook
+let call_hook fix_exn hook l c =
+  try hook l c
+  with e when Errors.noncritical e ->
+    let e = Errors.push e in
+    iraise (fix_exn e)
+
+(* Support for mutually proved theorems *)
+
+let retrieve_first_recthm = function
+  | VarRef id ->
+      (pi2 (Global.lookup_named id),variable_opacity id)
+  | ConstRef cst ->
+      let cb = Global.lookup_constant cst in
+      (Global.body_of_constant_body cb, is_opaque cb)
+  | _ -> assert false
+
+let adjust_guardness_conditions const = function
+  | [] -> const (* Not a recursive statement *)
+  | possible_indexes ->
+  (* Try all combinations... not optimal *)
+     let env = Global.env() in
+     { const with const_entry_body =
+        Future.chain ~greedy:true ~pure:true const.const_entry_body
+        (fun ((body, ctx), eff) ->
+          match kind_of_term body with
+          | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
+(*      let possible_indexes =
+	List.map2 (fun i c -> match i with Some i -> i | None ->
+	  List.interval 0 (List.length ((lam_assum c))))
+	  lemma_guard (Array.to_list fixdefs) in
+*)
+              let add c cb e =
+                let exists c e =
+                  try ignore(Environ.lookup_constant c e); true
+                  with Not_found -> false in 
+                if exists c e then e else Environ.add_constant c cb e in
+              let env = Declareops.fold_side_effects (fun env -> function
+                | SEsubproof (c, cb,_) -> add c cb env
+                | SEscheme (l,_) ->
+                    List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l)
+                env (Declareops.uniquize_side_effects eff) in
+              let indexes =
+	        search_guard Loc.ghost env
+                  possible_indexes fixdecls in
+		(mkFix ((indexes,0),fixdecls), ctx), eff
+          | _ -> (body, ctx), eff) }
+
+let find_mutually_recursive_statements thms =
+    let n = List.length thms in
+    let inds = List.map (fun (id,(t,impls,annot)) ->
+      let (hyps,ccl) = decompose_prod_assum t in
+      let x = (id,(t,impls)) in
+      match annot with
+      (* Explicit fixpoint decreasing argument is given *)
+      | Some (Some (_,id),CStructRec) ->
+          let i,b,typ = lookup_rel_id id hyps in
+          (match kind_of_term t with
+          | Ind ((kn,_ as ind), u) when
+              let mind = Global.lookup_mind kn in
+              mind.mind_finite == Decl_kinds.Finite && Option.is_empty b ->
+              [ind,x,i],[]
+          | _ ->
+              error "Decreasing argument is not an inductive assumption.")
+      (* Unsupported cases *)
+      | Some (_,(CWfRec _|CMeasureRec _)) ->
+          error "Only structural decreasing is supported for mutual statements."
+      (* Cofixpoint or fixpoint w/o explicit decreasing argument *)
+      | None | Some (None, CStructRec) ->
+      let whnf_hyp_hds = map_rel_context_in_env
+        (fun env c -> fst (whd_betadeltaiota_stack env Evd.empty c))
+        (Global.env()) hyps in
+      let ind_hyps =
+        List.flatten (List.map_i (fun i (_,b,t) ->
+          match kind_of_term t with
+          | Ind ((kn,_ as ind),u) when
+                let mind = Global.lookup_mind kn in
+                mind.mind_finite <> Decl_kinds.CoFinite && Option.is_empty b ->
+              [ind,x,i]
+          | _ ->
+              []) 0 (List.rev whnf_hyp_hds)) in
+      let ind_ccl =
+        let cclenv = push_rel_context hyps (Global.env()) in
+        let whnf_ccl,_ = whd_betadeltaiota_stack cclenv Evd.empty ccl in
+        match kind_of_term whnf_ccl with
+        | Ind ((kn,_ as ind),u) when
+              let mind = Global.lookup_mind kn in
+              Int.equal mind.mind_ntypes n && mind.mind_finite == Decl_kinds.CoFinite ->
+            [ind,x,0]
+        | _ ->
+            [] in
+      ind_hyps,ind_ccl) thms in
+    let inds_hyps,ind_ccls = List.split inds in
+    let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> eq_mind kn kn' in
+    (* Check if all conclusions are coinductive in the same type *)
+    (* (degenerated cartesian product since there is at most one coind ccl) *)
+    let same_indccl =
+      List.cartesians_filter (fun hyp oks ->
+	if List.for_all (of_same_mutind hyp) oks
+	then Some (hyp::oks) else None) [] ind_ccls in
+    let ordered_same_indccl =
+      List.filter (List.for_all_i (fun i ((kn,j),_,_) -> Int.equal i j) 0) same_indccl in
+    (* Check if some hypotheses are inductive in the same type *)
+    let common_same_indhyp =
+      List.cartesians_filter (fun hyp oks ->
+	if List.for_all (of_same_mutind hyp) oks
+	then Some (hyp::oks) else None) [] inds_hyps in
+    let ordered_inds,finite,guard =
+      match ordered_same_indccl, common_same_indhyp with
+      | indccl::rest, _ ->
+	  assert (List.is_empty rest);
+          (* One occ. of common coind ccls and no common inductive hyps *)
+	  if not (List.is_empty common_same_indhyp) then
+	    if_verbose msg_info (str "Assuming mutual coinductive statements.");
+	  flush_all ();
+          indccl, true, []
+      | [], _::_ ->
+          let () = match same_indccl with
+          | ind :: _ ->
+            if List.distinct_f ind_ord (List.map pi1 ind)
+            then
+              if_verbose msg_info
+                (strbrk
+                   ("Coinductive statements do not follow the order of "^
+                    "definition, assuming the proof to be by induction."));
+            flush_all ()
+          | _ -> ()
+          in
+          let possible_guards = List.map (List.map pi3) inds_hyps in
+	  (* assume the largest indices as possible *)
+	  List.last common_same_indhyp, false, possible_guards
+      | _, [] ->
+	  error
+            ("Cannot find common (mutual) inductive premises or coinductive" ^
+             " conclusions in the statements.")
+    in
+    (finite,guard,None), ordered_inds
+
+let look_for_possibly_mutual_statements = function
+  | [id,(t,impls,None)] ->
+      (* One non recursively proved theorem *)
+      None,[id,(t,impls)],None
+  | _::_ as thms ->
+    (* More than one statement and/or an explicit decreasing mark: *)
+    (* we look for a common inductive hyp or a common coinductive conclusion *)
+    let recguard,ordered_inds = find_mutually_recursive_statements thms in
+    let thms = List.map pi2 ordered_inds in
+    Some recguard,thms, Some (List.map (fun (_,_,i) -> succ i) ordered_inds)
+  | [] -> anomaly (Pp.str "Empty list of theorems.")
+
+(* Saving a goal *)
+
+let save id const cstrs do_guard (locality,poly,kind) hook =
+  let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
+  try
+    let const = adjust_guardness_conditions const do_guard in
+    let k = Kindops.logical_kind_of_goal_kind kind in
+    let l,r = match locality with
+      | Discharge when Lib.sections_are_opened () ->
+          let c = SectionLocalDef const in
+          let _ = declare_variable id (Lib.cwd(), c, k) in
+          (Local, VarRef id)
+      | Local | Global | Discharge ->
+          let local = match locality with
+          | Local | Discharge -> true
+          | Global -> false
+          in
+          let kn = declare_constant id ~local (DefinitionEntry const, k) in
+          (locality, ConstRef kn) in
+    definition_message id;
+    call_hook (fun exn -> exn) hook l r
+  with e when Errors.noncritical e ->
+    let e = Errors.push e in
+    iraise (fix_exn e)
+
+let default_thm_id = Id.of_string "Unnamed_thm"
+
+let compute_proof_name locality = function
+  | Some (loc,id) ->
+      (* We check existence here: it's a bit late at Qed time *)
+      if Nametab.exists_cci (Lib.make_path id) || is_section_variable id ||
+	 locality == Global && Nametab.exists_cci (Lib.make_path_except_section id)
+      then
+        user_err_loc (loc,"",pr_id id ++ str " already exists.");
+      id
+  | None ->
+      next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()) 
+
+let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,imps))) =
+  let t_i = norm t_i in
+  match body with
+  | None ->
+      (match locality with
+      | Discharge ->
+          let impl = false in (* copy values from Vernacentries *)
+          let k = IsAssumption Conjectural in
+          let c = SectionLocalAssum ((t_i,ctx),p,impl) in
+	  let _ = declare_variable id (Lib.cwd(),c,k) in
+          (Discharge, VarRef id,imps)
+      | Local | Global ->
+          let k = IsAssumption Conjectural in
+          let local = match locality with
+          | Local -> true
+          | Global -> false
+          | Discharge -> assert false
+          in
+          let ctx = Univ.ContextSet.to_context ctx in
+          let decl = (ParameterEntry (None,p,(t_i,ctx),None), k) in
+          let kn = declare_constant id ~local decl in
+          (locality,ConstRef kn,imps))
+  | Some body ->
+      let body = norm body in
+      let k = Kindops.logical_kind_of_goal_kind kind in
+      let body_i = match kind_of_term body with
+        | Fix ((nv,0),decls) -> mkFix ((nv,i),decls)
+        | CoFix (0,decls) -> mkCoFix (i,decls)
+        | _ -> anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr body) in
+      match locality with
+      | Discharge ->
+          let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p 
+	    ~univs:(Univ.ContextSet.to_context ctx) body_i in
+	  let c = SectionLocalDef const in
+	  let _ = declare_variable id (Lib.cwd(), c, k) in
+          (Discharge,VarRef id,imps)
+      | Local | Global ->
+        let ctx = Univ.ContextSet.to_context ctx in
+        let local = match locality with
+        | Local -> true
+        | Global -> false
+        | Discharge -> assert false
+        in
+        let const =
+	  Declare.definition_entry ~types:t_i ~poly:p ~univs:ctx ~opaque:opaq body_i
+	in
+        let kn = declare_constant id ~local (DefinitionEntry const, k) in
+        (locality,ConstRef kn,imps)
+
+let save_hook = ref ignore
+let set_save_hook f = save_hook := f
+
+let save_named proof =
+  let id,const,cstrs,do_guard,persistence,hook = proof in
+  save id const cstrs do_guard persistence hook
+
+let check_anonymity id save_ident =
+  if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then
+    error "This command can only be used for unnamed theorem."
+
+
+let save_anonymous proof save_ident =
+  let id,const,cstrs,do_guard,persistence,hook = proof in
+  check_anonymity id save_ident;
+  save save_ident const cstrs do_guard persistence hook
+
+let save_anonymous_with_strength proof kind save_ident =
+  let id,const,cstrs,do_guard,_,hook = proof in
+  check_anonymity id save_ident;
+  (* we consider that non opaque behaves as local for discharge *)
+  save save_ident const cstrs do_guard (Global, const.const_entry_polymorphic, Proof kind) hook
+
+(* Admitted *)
+
+let admit hook () =
+  let (id,k,typ) = Pfedit.current_proof_statement () in
+  let ctx =
+    let evd = fst (Pfedit.get_current_goal_context ()) in
+      Evd.universe_context evd
+  in
+  let e = Pfedit.get_used_variables(), pi2 k, (typ, ctx), None in
+  let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in
+  let () = match k with
+  | Global, _, _ -> ()
+  | Local, _, _ | Discharge, _, _ ->
+    msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++
+      str "declared as an axiom.")
+  in
+  let () = assumption_message id in
+  call_hook (fun exn -> exn) hook Global (ConstRef kn)
+
+(* Starting a goal *)
+
+let start_hook = ref ignore
+let set_start_hook = (:=) start_hook
+
+
+let get_proof proof do_guard hook opacity =
+  let (id,(const,cstrs,persistence)) =
+    Pfedit.cook_this_proof proof
+  in
+  (** FIXME *)
+  id,{const with const_entry_opaque = opacity},cstrs,do_guard,persistence,hook
+
+let standard_proof_terminator compute_guard hook =
+  let open Proof_global in function
+  | Admitted ->
+      admit hook ();
+      Pp.feedback Feedback.AddedAxiom
+  | Proved (is_opaque,idopt,proof) ->
+      let proof = get_proof proof compute_guard hook is_opaque in
+      begin match idopt with
+      | None -> save_named proof
+      | Some ((_,id),None) -> save_anonymous proof id
+      | Some ((_,id),Some kind) -> 
+          save_anonymous_with_strength proof kind id
+      end
+
+let universe_proof_terminator compute_guard hook =
+  let open Proof_global in function
+  | Admitted ->
+      admit (hook None) ();
+      Pp.feedback Feedback.AddedAxiom
+  | Proved (is_opaque,idopt,proof) ->
+      let proof = get_proof proof compute_guard 
+	(hook (Some proof.Proof_global.universes)) is_opaque in
+      begin match idopt with
+      | None -> save_named proof
+      | Some ((_,id),None) -> save_anonymous proof id
+      | Some ((_,id),Some kind) -> 
+          save_anonymous_with_strength proof kind id
+      end
+
+let start_proof id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
+  let terminator = standard_proof_terminator compute_guard hook in
+  let sign = 
+    match sign with
+    | Some sign -> sign
+    | None -> initialize_named_context_for_proof ()
+  in
+  !start_hook c;
+  Pfedit.start_proof id kind sigma sign c ?init_tac terminator
+
+let start_proof_univs id kind sigma ?sign c ?init_tac ?(compute_guard=[]) hook =
+  let terminator = universe_proof_terminator compute_guard hook in
+  let sign = 
+    match sign with
+    | Some sign -> sign
+    | None -> initialize_named_context_for_proof ()
+  in
+  !start_hook c;
+  Pfedit.start_proof id kind sigma sign c ?init_tac terminator
+
+let rec_tac_initializer finite guard thms snl =
+  if finite then
+    match List.map (fun (id,(t,_)) -> (id,t)) thms with
+    | (id,_)::l -> Tactics.mutual_cofix id l 0
+    | _ -> assert false
+  else
+    (* nl is dummy: it will be recomputed at Qed-time *)
+    let nl = match snl with 
+     | None -> List.map succ (List.map List.last guard)
+     | Some nl -> nl
+    in match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with
+       | (id,n,_)::l -> Tactics.mutual_fix id n l 0
+       | _ -> assert false
+
+let start_proof_with_initialization kind ctx recguard thms snl hook =
+  let intro_tac (_, (_, (ids, _))) =
+    Tacticals.New.tclMAP (function
+    | Name id -> Tactics.intro_mustbe_force id
+    | Anonymous -> Tactics.intro) (List.rev ids) in
+  let init_tac,guard = match recguard with
+  | Some (finite,guard,init_tac) ->
+      let rec_tac = Proofview.V82.tactic (rec_tac_initializer finite guard thms snl) in
+      Some (match init_tac with
+        | None -> 
+            if Flags.is_auto_intros () then 
+              Tacticals.New.tclTHENS rec_tac (List.map intro_tac thms)
+            else
+              rec_tac
+        | Some tacl ->
+            Tacticals.New.tclTHENS rec_tac
+            (if Flags.is_auto_intros () then
+              List.map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms
+            else
+              tacl)),guard
+  | None ->
+      let () = match thms with [_] -> () | _ -> assert false in
+      (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in
+  match thms with
+  | [] -> anomaly (Pp.str "No proof to start")
+  | (id,(t,(_,imps)))::other_thms ->
+      let hook ctx strength ref =
+        let ctx = match ctx with
+        | None -> Evd.empty_evar_universe_context
+        | Some ctx -> ctx
+        in
+        let other_thms_data =
+          if List.is_empty other_thms then [] else
+            (* there are several theorems defined mutually *)
+            let body,opaq = retrieve_first_recthm ref in
+            let subst = Evd.evar_universe_context_subst ctx in
+            let norm c = Universes.subst_opt_univs_constr subst c in
+	    let ctx = Evd.evar_universe_context_set ctx in
+	    let body = Option.map norm body in
+            List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in
+        let thms_data = (strength,ref,imps)::other_thms_data in
+        List.iter (fun (strength,ref,imps) ->
+	  maybe_declare_manual_implicits false ref imps;
+	  call_hook (fun exn -> exn) hook strength ref) thms_data in
+      start_proof_univs id kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard
+
+let start_proof_com kind thms hook =
+  let env0 = Global.env () in
+  let evdref = ref (Evd.from_env env0) in
+  let thms = List.map (fun (sopt,(bl,t,guard)) ->
+    let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in
+    let t', imps' = interp_type_evars_impls ~impls env evdref t in
+    check_evars_are_solved env !evdref (Evd.empty,!evdref);
+    let ids = List.map pi1 ctx in
+      (compute_proof_name (pi1 kind) sopt,
+      (nf_evar !evdref (it_mkProd_or_LetIn t' ctx),
+       (ids, imps @ lift_implicits (List.length ids) imps'),
+       guard)))
+    thms in
+  let recguard,thms,snl = look_for_possibly_mutual_statements thms in
+  let evd, nf = Evarutil.nf_evars_and_universes !evdref in
+  let thms = List.map (fun (n, (t, info)) -> (n, (nf t, info))) thms in
+  start_proof_with_initialization kind evd
+    recguard thms snl hook
+
+
+(* Saving a proof *)
+
+let save_proof ?proof = function
+  | Vernacexpr.Admitted ->
+      Proof_global.get_terminator() Proof_global.Admitted
+  | Vernacexpr.Proved (is_opaque,idopt) ->
+      let (proof_obj,terminator) =
+        match proof with
+        | None ->
+            Proof_global.close_proof ~keep_body_ucst_sepatate:false (fun x -> x)
+        | Some proof -> proof
+      in
+      (* if the proof is given explicitly, nothing has to be deleted *)
+      if Option.is_empty proof then Pfedit.delete_current_proof ();
+      terminator (Proof_global.Proved (is_opaque,idopt,proof_obj))
+
+(* Miscellaneous *)
+
+let get_current_context () =
+  try Pfedit.get_current_goal_context ()
+  with e when Logic.catchable_exception e ->
+    (Evd.empty, Global.env())
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
new file mode 100644
index 00000000..d0669d7a
--- /dev/null
+++ b/stm/lemmas.mli
@@ -0,0 +1,62 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Term
+open Decl_kinds
+open Constrexpr
+open Tacexpr
+open Vernacexpr
+open Pfedit
+
+type 'a declaration_hook
+
+val mk_hook :
+  (Decl_kinds.locality -> Globnames.global_reference -> 'a) -> 'a declaration_hook
+
+val call_hook :
+  Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a
+
+(** A hook start_proof calls on the type of the definition being started *)
+val set_start_hook : (types -> unit) -> unit
+
+val start_proof : Id.t -> goal_kind -> Evd.evar_map -> ?sign:Environ.named_context_val -> types ->
+  ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
+   unit declaration_hook -> unit
+
+val start_proof_univs : Id.t -> goal_kind -> Evd.evar_map -> ?sign:Environ.named_context_val -> types ->
+  ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
+  (Proof_global.proof_universes option -> unit declaration_hook) -> unit
+
+val start_proof_com : goal_kind ->
+  (lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)) list ->
+  unit declaration_hook -> unit
+
+val start_proof_with_initialization : 
+  goal_kind -> Evd.evar_map -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option ->
+  (Id.t * (types * (Name.t list * Impargs.manual_explicitation list))) list
+  -> int list option -> unit declaration_hook -> unit
+
+val standard_proof_terminator :
+  Proof_global.lemma_possible_guards -> unit declaration_hook ->
+    Proof_global.proof_terminator
+
+(** {6 ... } *)
+
+(** A hook the next three functions pass to cook_proof *)
+val set_save_hook : (Proof.proof -> unit) -> unit
+
+val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit
+
+
+(** [get_current_context ()] returns the evar context and env of the
+   current open proof if any, otherwise returns the empty evar context
+   and the current global env *)
+
+val get_current_context : unit -> Evd.evar_map * Environ.env
+
diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml
new file mode 100644
index 00000000..0e40c345
--- /dev/null
+++ b/stm/proofworkertop.ml
@@ -0,0 +1,18 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask)
+
+let () = Coqtop.toploop_init := (fun args ->
+        Flags.make_silent true;
+        W.init_stdout ();
+        CoqworkmgrApi.init !Flags.async_proofs_worker_priority;
+        args)
+
+let () = Coqtop.toploop_run := W.main_loop
+
diff --git a/stm/proofworkertop.mllib b/stm/proofworkertop.mllib
new file mode 100644
index 00000000..f9f6c22d
--- /dev/null
+++ b/stm/proofworkertop.mllib
@@ -0,0 +1 @@
+Proofworkertop
diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml
new file mode 100644
index 00000000..c8e6432b
--- /dev/null
+++ b/stm/queryworkertop.ml
@@ -0,0 +1,18 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask)
+
+let () = Coqtop.toploop_init := (fun args ->
+        Flags.make_silent true;
+        W.init_stdout ();
+        CoqworkmgrApi.init !Flags.async_proofs_worker_priority;
+        args)
+
+let () = Coqtop.toploop_run := W.main_loop
+
diff --git a/stm/queryworkertop.mllib b/stm/queryworkertop.mllib
new file mode 100644
index 00000000..c2f73089
--- /dev/null
+++ b/stm/queryworkertop.mllib
@@ -0,0 +1 @@
+Queryworkertop
diff --git a/stm/spawned.ml b/stm/spawned.ml
new file mode 100644
index 00000000..18159288
--- /dev/null
+++ b/stm/spawned.ml
@@ -0,0 +1,86 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+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
+
+let handshake cin cout =
+  try
+    match input_value cin with
+    | Hello(v, pid) when v = proto_version ->
+        prerr_endline (Printf.sprintf "Handshake with %d OK" pid);
+        output_value cout (Hello (proto_version,Unix.getpid ())); flush cout
+    | _ -> raise (Failure "handshake protocol")
+  with
+  | Failure s | Invalid_argument s | Sys_error s ->
+      pr_err ("Handshake failed: "  ^ s); raise (Failure "handshake")
+  | End_of_file ->
+      pr_err "Handshake failed: End_of_file"; raise (Failure "handshake")
+
+let open_bin_connection h p =
+  let open Unix in
+  let cin, cout = open_connection (ADDR_INET (inet_addr_of_string h,p)) in
+  set_binary_mode_in cin true;
+  set_binary_mode_out cout true;
+  let cin = CThread.prepare_in_channel_for_thread_friendly_io cin in
+  cin, cout
+
+let controller h p =
+  prerr_endline "starting controller thread";
+  let main () =
+    let ic, oc = open_bin_connection h p in
+    let rec loop () =
+      try
+        match CThread.thread_friendly_input_value ic with
+        | Hello _ -> prerr_endline "internal protocol error"; exit 1
+        | ReqDie -> prerr_endline "death sentence received"; exit 0
+        | ReqStats ->
+            output_value oc (RespStats (Gc.quick_stat ())); flush oc; loop ()
+      with
+      | e ->
+        prerr_endline ("control channel broken: " ^ Printexc.to_string e);
+        exit 1 in
+    loop () in
+  ignore(Thread.create main ())
+
+let main_channel = ref None
+let control_channel = ref None
+
+let channels = ref None
+
+let init_channels () =
+  if !channels <> None then Errors.anomaly(Pp.str "init_channels called twice");
+  let () = match !main_channel with
+  | None -> ()
+  | Some (Socket(mh,mp)) ->
+    channels := Some (open_bin_connection mh mp);
+  | Some AnonPipe ->
+    let stdin = Unix.in_channel_of_descr (Unix.dup Unix.stdin) in
+    let stdout = Unix.out_channel_of_descr (Unix.dup Unix.stdout) in
+    Unix.dup2 Unix.stderr Unix.stdout;
+    set_binary_mode_in stdin true;
+    set_binary_mode_out stdout true;
+    let stdin = CThread.prepare_in_channel_for_thread_friendly_io stdin in
+    channels := Some (stdin, stdout);
+  in
+  match !control_channel with
+  | None -> ()
+  | Some (Socket (ch, cp)) ->
+    controller ch cp
+  | Some AnonPipe ->
+    Errors.anomaly (Pp.str "control channel cannot be a pipe")
+
+let get_channels () =
+  match !channels with
+  | None -> Errors.anomaly(Pp.str "init_channels not called")
+  | Some(ic, oc) -> ic, oc
+
diff --git a/stm/spawned.mli b/stm/spawned.mli
new file mode 100644
index 00000000..d9e7baff
--- /dev/null
+++ b/stm/spawned.mli
@@ -0,0 +1,22 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* To link this file, threads are needed *)
+
+type chandescr = AnonPipe | Socket of string * 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
+
diff --git a/stm/stm.ml b/stm/stm.ml
new file mode 100644
index 00000000..7b246854
--- /dev/null
+++ b/stm/stm.ml
@@ -0,0 +1,2407 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr
+
+let prerr_endline s = if !Flags.debug then begin pr_err s end else ()
+
+open Vernacexpr
+open Errors
+open Pp
+open Names
+open Util
+open Ppvernac
+open Vernac_classifier
+
+module Hooks = struct
+
+let process_error, process_error_hook = Hook.make ()
+let interp, interp_hook = Hook.make ()
+let with_fail, with_fail_hook = Hook.make ()
+
+let state_computed, state_computed_hook = Hook.make
+ ~default:(fun state_id ~in_cache ->
+    feedback ~state_id Feedback.Processed) ()
+
+let state_ready, state_ready_hook = Hook.make
+ ~default:(fun state_id -> ()) ()
+
+let forward_feedback, forward_feedback_hook = Hook.make
+ ~default:(function
+    | { Feedback.id = Feedback.Edit edit_id; route; contents } ->
+          feedback ~edit_id ~route contents
+    | { Feedback.id = Feedback.State state_id; route; contents } ->
+          feedback ~state_id ~route contents) ()
+
+let parse_error, parse_error_hook = Hook.make
+ ~default:(function
+    | Feedback.Edit edit_id -> fun loc msg ->
+        feedback ~edit_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))
+    | Feedback.State state_id -> fun loc msg ->
+        feedback ~state_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))) ()
+
+let execution_error, execution_error_hook = Hook.make
+ ~default:(fun state_id loc msg ->
+    feedback ~state_id (Feedback.ErrorMsg (loc, string_of_ppcmds msg))) ()
+
+let unreachable_state, unreachable_state_hook = Hook.make
+ ~default:(fun _ -> ()) ()
+
+include Hook
+
+(* enables:  Hooks.(call foo args) *)
+let call = get
+
+let call_process_error_once =
+  let processed : unit Exninfo.t = Exninfo.make () in
+  fun (_, info as ei) ->
+    match Exninfo.get info processed with
+    | Some _ -> ei
+    | None ->
+        let e, info = call process_error ei in
+        let info = Exninfo.add info processed () in
+        e, info
+
+end
+
+(* During interactive use we cache more states so that Undoing is fast *)
+let interactive () =
+  if !Flags.ide_slave || !Flags.print_emacs || not !Flags.batch_mode then `Yes
+  else `No
+
+let async_proofs_workers_extra_env = ref [||]
+
+type ast = { verbose : bool; loc : Loc.t; mutable expr : vernac_expr }
+let pr_ast { expr } = pr_vernac expr
+
+(* Wrapper for Vernacentries.interp to set the feedback id *)
+let vernac_interp ?proof id ?route { verbose; loc; expr } =
+  let rec internal_command = function
+    | VernacResetName _ | VernacResetInitial | VernacBack _
+    | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _
+    | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true
+    | VernacTime el -> List.for_all (fun (_,e) -> internal_command e) el
+    | _ -> false in
+  if internal_command expr then begin
+    prerr_endline ("ignoring " ^ string_of_ppcmds(pr_vernac expr))
+  end else begin
+    set_id_for_feedback ?route (Feedback.State id);
+    Aux_file.record_in_aux_set_at loc;
+    prerr_endline ("interpreting " ^ string_of_ppcmds(pr_vernac expr));
+    try Hooks.(call interp ?verbosely:(Some verbose) ?proof (loc, expr))
+    with e ->
+      let e = Errors.push e in
+      iraise Hooks.(call_process_error_once e)
+  end
+
+(* Wrapper for Vernac.parse_sentence to set the feedback id *)
+let vernac_parse ?newtip ?route eid s =
+  let feedback_id = 
+    if Option.is_empty newtip then Feedback.Edit eid
+    else Feedback.State (Option.get newtip) in
+  set_id_for_feedback ?route feedback_id;
+  let pa = Pcoq.Gram.parsable (Stream.of_string s) in
+  Flags.with_option Flags.we_are_parsing (fun () ->
+    try
+      match Pcoq.Gram.entry_parse Pcoq.main_entry pa with
+      | None -> raise (Invalid_argument "vernac_parse")
+      | Some ast -> ast
+    with e when Errors.noncritical e ->
+      let (e, info) = Errors.push e in
+      let loc = Option.default Loc.ghost (Loc.get_loc info) in
+      Hooks.(call parse_error feedback_id loc (iprint (e, info)));
+      iraise (e, info))
+  ()
+
+let pr_open_cur_subgoals () =
+  try Printer.pr_open_subgoals ()
+  with Proof_global.NoCurrentProof -> str""
+
+module Vcs_ = Vcs.Make(Stateid)
+type future_proof = Proof_global.closed_proof_output Future.computation
+type proof_mode = string
+type depth = int
+type cancel_switch = bool ref
+type branch_type =
+  [ `Master
+  | `Proof of proof_mode * depth
+  | `Edit of proof_mode * Stateid.t * Stateid.t ]
+type cmd_t = {
+  cast : ast;
+  cids : Id.t list;
+  cqueue : [ `MainQueue | `TacQueue of cancel_switch | `QueryQueue of cancel_switch ] }
+type fork_t = ast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Id.t list
+type qed_t = {
+  qast : ast;
+  keep : vernac_qed_type;
+  mutable fproof : (future_proof * cancel_switch) option;
+  brname : Vcs_.Branch.t;
+  brinfo : branch_type Vcs_.branch_info
+}
+type seff_t = ast option
+type alias_t = Stateid.t
+type transaction =
+  | Cmd    of cmd_t
+  | Fork   of fork_t
+  | Qed    of qed_t
+  | Sideff of seff_t
+  | Alias  of alias_t
+  | Noop
+type step =
+  [ `Cmd    of cmd_t
+  | `Fork   of fork_t * Stateid.t option
+  | `Qed    of qed_t * Stateid.t
+  | `Sideff of [ `Ast of ast * Stateid.t | `Id of Stateid.t ]
+  | `Alias  of alias_t ]
+type visit = { step : step; next : Stateid.t }
+
+type state = {
+  system : States.state;
+  proof : Proof_global.state;
+  shallow : bool
+}
+type branch = Vcs_.Branch.t * branch_type Vcs_.branch_info
+type backup = { mine : branch; others : branch list }
+type 'vcs state_info = { (* Make private *)
+  mutable n_reached : int;
+  mutable n_goals : int;
+  mutable state : state option;
+  mutable vcs_backup : 'vcs option * backup option;
+}
+let default_info () =
+  { n_reached = 0; n_goals = 0; state = None; vcs_backup = None,None }
+
+(* Functions that work on a Vcs with a specific branch type *)
+module Vcs_aux : sig
+
+  val proof_nesting : (branch_type, 't,'i) Vcs_.t -> int
+  val find_proof_at_depth :
+    (branch_type, 't, 'i) Vcs_.t -> int ->
+      Vcs_.Branch.t * branch_type Vcs_.branch_info
+  exception Expired
+  val visit : (branch_type, transaction,'i) Vcs_.t -> Vcs_.Dag.node -> visit
+
+end = struct (* {{{ *)
+
+  let proof_nesting vcs =
+    List.fold_left max 0
+      (List.map_filter
+        (function
+         | { Vcs_.kind = `Proof (_,n) } -> Some n
+         | { Vcs_.kind = `Edit _ } -> Some 1
+         | _ -> None)
+        (List.map (Vcs_.get_branch vcs) (Vcs_.branches vcs)))
+
+  let find_proof_at_depth vcs pl =
+    try List.find (function
+          | _, { Vcs_.kind = `Proof(m, n) } -> Int.equal n pl
+          | _, { Vcs_.kind = `Edit _ } -> anomaly(str"find_proof_at_depth")
+          | _ -> false)
+        (List.map (fun h -> h, Vcs_.get_branch vcs h) (Vcs_.branches vcs))
+    with Not_found -> failwith "find_proof_at_depth"
+
+  exception Expired
+  let visit vcs id =
+    if Stateid.equal id Stateid.initial then
+      anomaly(str"Visiting the initial state id")
+    else if Stateid.equal id Stateid.dummy then
+      anomaly(str"Visiting the dummy state id")
+    else
+    try
+      match Vcs_.Dag.from_node (Vcs_.dag vcs) id with
+      | [n, Cmd x] -> { step = `Cmd x; next = n }
+      | [n, Alias x] -> { step = `Alias x; next = n }
+      | [n, Fork x] -> { step = `Fork (x,None); next = n }
+      | [n, Fork x; p, Noop] -> { step = `Fork (x,Some p); next = n }
+      | [p, Noop; n, Fork x] -> { step = `Fork (x,Some p); next = n }
+      | [n, Qed x; p, Noop]
+      | [p, Noop; n, Qed x] -> { step = `Qed (x,p); next = n }
+      | [n, Sideff None; p, Noop]
+      | [p, Noop; n, Sideff None]-> { step = `Sideff (`Id p); next = n }
+      | [n, Sideff (Some x); p, Noop]
+      | [p, Noop; n, Sideff (Some x)]-> { step = `Sideff(`Ast (x,p)); next = n }
+      | [n, Sideff (Some x)]-> {step = `Sideff(`Ast (x,Stateid.dummy)); next=n}
+      | _ -> anomaly (str ("Malformed VCS at node "^Stateid.to_string id))
+    with Not_found -> raise Expired
+
+end (* }}} *)
+
+(*************************** THE DOCUMENT *************************************)
+(******************************************************************************)
+
+(* Imperative wrap around VCS to obtain _the_ VCS that is the
+ * representation of the document Coq is currently processing *)
+module VCS : sig
+
+  exception Expired
+
+  module Branch : (module type of Vcs_.Branch with type t = Vcs_.Branch.t)
+  type id = Stateid.t
+  type 'branch_type branch_info = 'branch_type Vcs_.branch_info = {
+    kind : [> `Master] as 'branch_type;
+    root : id;
+    pos  : id;
+  }
+
+  type vcs = (branch_type, transaction, vcs state_info) Vcs_.t
+
+  val init : id -> unit
+
+  val current_branch : unit -> Branch.t
+  val checkout : Branch.t -> unit
+  val branches : unit -> Branch.t list
+  val get_branch : Branch.t -> branch_type branch_info
+  val get_branch_pos : Branch.t -> id
+  val new_node : ?id:Stateid.t -> unit -> id
+  val merge : id -> ours:transaction -> ?into:Branch.t -> Branch.t -> unit
+  val rewrite_merge : id -> ours:transaction -> at:id -> Branch.t -> unit
+  val delete_branch : Branch.t -> unit
+  val commit : id -> transaction -> unit
+  val mk_branch_name : ast -> Branch.t
+  val edit_branch : Branch.t
+  val branch : ?root:id -> ?pos:id -> Branch.t -> branch_type -> unit
+  val reset_branch : Branch.t -> id -> unit
+  val reachable : id -> Vcs_.NodeSet.t
+  val cur_tip : unit -> id
+
+  val get_info : id -> vcs state_info
+  val reached : id -> bool -> unit
+  val goals : id -> int -> unit
+  val set_state : id -> state -> unit
+  val get_state : id -> state option
+
+  (* cuts from start -> stop, raising Expired if some nodes are not there *)
+  val slice : start:id -> stop:id -> vcs
+  val nodes_in_slice : start:id -> stop:id -> Stateid.t list
+  
+  val create_cluster : id list -> qed:id -> start:id -> unit
+  val cluster_of : id -> (id * id) option
+  val delete_cluster_of : id -> unit
+
+  val proof_nesting : unit -> int
+  val checkout_shallowest_proof_branch : unit -> unit
+  val propagate_sideff : ast option -> unit
+
+  val gc : unit -> unit
+
+  val visit : id -> visit
+
+  val print : ?now:bool -> unit -> unit
+
+  val backup : unit -> vcs
+  val restore : vcs -> unit
+
+end = struct (* {{{ *)
+
+  include Vcs_
+  exception Expired = Vcs_aux.Expired
+
+  module StateidSet = Set.Make(Stateid)
+  open Printf
+
+  let print_dag vcs () =
+    let fname =
+      "stm_" ^ Str.global_replace (Str.regexp " ") "_" (System.process_id ()) in
+    let string_of_transaction = function
+      | Cmd { cast = t } | Fork (t, _,_,_) ->
+          (try string_of_ppcmds (pr_ast t) with _ -> "ERR")
+      | Sideff (Some t) ->
+          sprintf "Sideff(%s)"
+            (try string_of_ppcmds (pr_ast t) with _ -> "ERR")
+      | Sideff None -> "EnvChange"
+      | Noop -> " "
+      | Alias id -> sprintf "Alias(%s)" (Stateid.to_string id)
+      | Qed { qast } -> string_of_ppcmds (pr_ast qast) in
+    let is_green id = 
+      match get_info vcs id with
+      | Some { state = Some _ } -> true
+      | _ -> false in
+    let is_red id =
+      match get_info vcs id with
+      | Some s -> Int.equal s.n_reached ~-1
+      | _ -> false in
+    let head = current_branch vcs in
+    let heads =
+      List.map (fun x -> x, (get_branch vcs x).pos) (branches vcs) in
+    let graph = dag vcs in
+    let quote s =
+      Str.global_replace (Str.regexp "\n") "<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 ids = ref StateidSet.empty in
+    let clus = Hashtbl.create 13 in
+    let node_info id =
+      match get_info vcs id with
+      | None -> ""
+      | Some info ->
+          sprintf "<<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 add_to_clus_or_ids from cf =
+      match cf with
+      | None -> ids := StateidSet.add from !ids; false
+      | Some c -> Hashtbl.replace clus c
+         (try let n = Hashtbl.find clus c in from::n
+         with Not_found -> [from]); true in
+    let oc = open_out fname_dot in
+    output_string oc "digraph states {\nsplines=ortho\n";
+    Dag.iter graph (fun from cf _ l ->
+      let c1 = add_to_clus_or_ids from cf in
+      List.iter (fun (dest, trans) ->
+       let c2 = add_to_clus_or_ids dest (Dag.cluster_of graph dest) in
+       fprintf oc "%s -> %s [xlabel=%s,labelfloat=%b];\n"
+           (node from) (node dest) (edge trans) (c1 && c2)) l
+    );
+    StateidSet.iter (nodefmt oc) !ids;
+    Hashtbl.iter (fun c nodes ->
+       fprintf oc "subgraph cluster_%s {\n" (Dag.Cluster.to_string c);
+       List.iter (nodefmt oc) nodes;
+       fprintf oc "color=blue; }\n"
+    ) clus;
+    List.iteri (fun i (b,id) ->
+      let shape = if Branch.equal head b then "box3d" else "box" in
+      fprintf oc "b%d -> %s;\n" i (node id);
+      fprintf oc "b%d [shape=%s,label=\"%s\"];\n" i shape
+        (Branch.to_string b);
+    ) heads;
+    output_string oc "}\n";
+    close_out oc;
+    ignore(Sys.command
+      ("dot -Tpdf -Gcharset=latin1 " ^ fname_dot ^ " -o" ^ fname_ps))
+
+  type vcs = (branch_type, transaction, vcs state_info) t
+  let vcs : vcs ref = ref (empty Stateid.dummy)
+
+  let init id =
+    vcs := empty id;
+    vcs := set_info !vcs id (default_info ())
+
+  let current_branch () = current_branch !vcs
+
+  let checkout head = vcs := checkout !vcs head
+  let branches () = branches !vcs
+  let get_branch head = get_branch !vcs head
+  let get_branch_pos head = (get_branch head).pos
+  let new_node ?(id=Stateid.fresh ()) () =
+    assert(Vcs_.get_info !vcs id = None);
+    vcs := set_info !vcs id (default_info ());
+    id
+  let merge id ~ours ?into branch =
+    vcs := merge !vcs id ~ours ~theirs:Noop ?into branch
+  let delete_branch branch = vcs := delete_branch !vcs branch
+  let reset_branch branch id = vcs := reset_branch !vcs branch id
+  let commit id t = vcs := commit !vcs id t
+  let rewrite_merge id ~ours ~at branch =
+    vcs := rewrite_merge !vcs id ~ours ~theirs:Noop ~at branch
+  let reachable id = reachable !vcs id
+  let mk_branch_name { expr = x } = Branch.make
+    (match x with
+    | VernacDefinition (_,(_,i),_) -> string_of_id i
+    | VernacStartTheoremProof (_,[Some (_,i),_],_) -> string_of_id i
+    | _ -> "branch")
+  let edit_branch = Branch.make "edit"
+  let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind
+  let get_info id =
+    match get_info !vcs id with
+    | Some x -> x
+    | None -> raise Vcs_aux.Expired
+  let set_state id s =
+    (get_info id).state <- Some s;
+    if Flags.async_proofs_is_master () then Hooks.(call state_ready id)
+  let get_state id = (get_info id).state
+  let reached id b =
+    let info = get_info id in
+    if b then info.n_reached <- info.n_reached + 1
+    else info.n_reached <- -1
+  let goals id n = (get_info id).n_goals <- n
+  let cur_tip () = get_branch_pos (current_branch ())
+
+  let proof_nesting () = Vcs_aux.proof_nesting !vcs
+
+  let checkout_shallowest_proof_branch () =
+    if List.mem edit_branch (Vcs_.branches !vcs) then begin
+      checkout edit_branch;
+      match get_branch edit_branch with
+      | { kind = `Edit (mode, _, _) } -> Proof_global.activate_proof_mode mode
+      | _ -> assert false
+    end else
+      let pl = proof_nesting () in
+      try
+        let branch, mode = match Vcs_aux.find_proof_at_depth !vcs pl with
+          | h, { Vcs_.kind = `Proof (m, _) } -> h, m | _ -> assert false in
+        checkout branch;
+        prerr_endline ("mode:" ^ mode);
+        Proof_global.activate_proof_mode mode
+      with Failure _ ->
+        checkout Branch.master;
+        Proof_global.disactivate_proof_mode "Classic"
+
+  (* copies the transaction on every open branch *)
+  let propagate_sideff t =
+    List.iter (fun b ->
+      checkout b;
+      let id = new_node () in
+      merge id ~ours:(Sideff t) ~into:b Branch.master)
+    (List.filter (fun b -> not (Branch.equal b Branch.master)) (branches ()))
+  
+  let visit id = Vcs_aux.visit !vcs id
+
+  let nodes_in_slice ~start ~stop =
+    let rec aux id =
+      if Stateid.equal id start then [] else
+      match visit id with
+      | { next = n; step = `Cmd x } -> (id,Cmd x) :: aux n
+      | { next = n; step = `Alias x } -> (id,Alias x) :: aux n
+      | { next = n; step = `Sideff (`Ast (x,_)) } ->
+           (id,Sideff (Some x)) :: aux n
+      | _ -> anomaly(str("Cannot slice from "^ Stateid.to_string start ^
+                         " to "^Stateid.to_string stop))
+    in aux stop
+
+  let slice ~start ~stop =
+    let l = nodes_in_slice ~start ~stop in
+    let copy_info v id =
+      Vcs_.set_info v id
+        { (get_info id) with state = None; vcs_backup = None,None } in
+    let copy_info_w_state v id =
+      Vcs_.set_info v id { (get_info id) with vcs_backup = None,None } in
+    let v = Vcs_.empty start in
+    let v = copy_info v start in
+    let v = List.fold_right (fun (id,tr) v ->
+      let v = Vcs_.commit v id tr in
+      let v = copy_info v id in
+      v) l v in
+    (* Stm should have reached the beginning of proof *)
+    assert (not (Option.is_empty (get_info start).state));
+    (* We put in the new dag the most recent state known to master *)
+    let rec fill id =
+      if (get_info id).state = None then fill (Vcs_aux.visit v id).next
+      else copy_info_w_state v id in
+    fill stop
+
+  let nodes_in_slice ~start ~stop =
+    List.rev (List.map fst (nodes_in_slice ~start ~stop))
+
+  let create_cluster l ~qed ~start = vcs := create_cluster !vcs l (qed,start)
+  let cluster_of id = Option.map Dag.Cluster.data (cluster_of !vcs id)
+  let delete_cluster_of id =
+    Option.iter (fun x -> vcs := delete_cluster !vcs x) (Vcs_.cluster_of !vcs id)
+
+  let gc () =
+    let old_vcs = !vcs in
+    let new_vcs, erased_nodes = gc old_vcs in
+    Vcs_.NodeSet.iter (fun id ->
+        match (Vcs_aux.visit old_vcs id).step with
+        | `Qed ({ fproof = Some (_, cancel_switch) }, _)
+        | `Cmd { cqueue = `TacQueue cancel_switch }
+        | `Cmd { cqueue = `QueryQueue cancel_switch } ->
+             cancel_switch := true
+        | _ -> ())
+      erased_nodes;
+    vcs := new_vcs
+
+  module NB : sig (* Non blocking Sys.command *)
+
+    val command : now:bool -> (unit -> unit) -> unit
+
+  end = struct
+    
+    let m = Mutex.create ()
+    let c = Condition.create ()
+    let job = ref None
+    let worker = ref None
+
+    let set_last_job j =
+      Mutex.lock m;
+      job := Some j;
+      Condition.signal c;
+      Mutex.unlock m
+
+    let get_last_job () =
+      Mutex.lock m;
+      while Option.is_empty !job do Condition.wait c m; done;
+      match !job with
+      | None -> assert false
+      | Some x -> job := None; Mutex.unlock m; x
+
+    let run_command () =
+      try while true do get_last_job () () done
+      with e -> () (* No failure *)
+
+    let command ~now job =
+      if now then job ()
+      else begin
+        set_last_job job;
+        if Option.is_empty !worker then
+          worker := Some (Thread.create run_command ())
+      end
+
+  end
+
+  let print ?(now=false) () =
+    if not !Flags.debug && not now then () else NB.command ~now (print_dag !vcs)
+
+  let backup () = !vcs
+  let restore v = vcs := v
+
+end (* }}} *)
+
+let state_of_id id =
+  try `Valid (VCS.get_info id).state
+  with VCS.Expired -> `Expired
+
+
+(****** A cache: fills in the nodes of the VCS document with their value ******)
+module State : sig
+  
+  (** The function is from unit, so it uses the current state to define
+      a new one.  I.e. one may been to install the right state before
+      defining a new one.
+      Warning: an optimization in installed_cached requires that state
+      modifying functions are always executed using this wrapper. *)
+  val define :
+    ?safe_id:Stateid.t ->
+    ?redefine:bool -> ?cache:Summary.marshallable ->
+    ?feedback_processed:bool -> (unit -> unit) -> Stateid.t -> unit
+
+  val install_cached : Stateid.t -> unit
+  val is_cached : ?cache:Summary.marshallable -> Stateid.t -> bool
+
+
+  val exn_on : Stateid.t -> ?valid:Stateid.t -> iexn -> iexn
+  (* to send states across worker/master *)
+  type frozen_state
+  val get_cached : Stateid.t -> frozen_state
+  val same_env : frozen_state -> frozen_state -> bool
+  type partial_state =
+    [ `Full of frozen_state | `Proof of Stateid.t * Proof_global.state ]
+  val proof_part_of_frozen : frozen_state -> Proof_global.state
+  val assign : Stateid.t -> partial_state -> unit
+
+end = struct (* {{{ *)
+
+  (* cur_id holds Stateid.dummy in case the last attempt to define a state
+   * failed, so the global state may contain garbage *)
+  let cur_id = ref Stateid.dummy
+
+  (* helpers *)
+  let freeze_global_state marshallable =
+    { system = States.freeze ~marshallable;
+      proof = Proof_global.freeze ~marshallable;
+      shallow = (marshallable = `Shallow) }
+  let unfreeze_global_state { system; proof } =
+    States.unfreeze system; Proof_global.unfreeze proof
+
+  (* hack to make futures functional *)
+  let in_t, out_t = Dyn.create "state4future"
+  let () = Future.set_freeze
+    (fun () -> in_t (freeze_global_state `No, !cur_id))
+    (fun t -> let s,i = out_t t in unfreeze_global_state s; cur_id := i)
+  
+  type frozen_state = state
+  type partial_state =
+    [ `Full of frozen_state | `Proof of Stateid.t * Proof_global.state ]
+  let proof_part_of_frozen { proof } = proof
+
+  let freeze marhallable id = VCS.set_state id (freeze_global_state marhallable)
+
+  let is_cached ?(cache=`No) id =
+    if Stateid.equal id !cur_id then
+      try match VCS.get_info id with
+        | { state = None } when cache = `Yes -> freeze `No id; true
+        | { state = None } when cache = `Shallow -> freeze `Shallow id; true
+        | _ -> true
+      with VCS.Expired -> false
+    else
+      try match VCS.get_info id with
+        | { state = Some _ } -> true
+        | _ -> false 
+      with VCS.Expired -> false
+
+  let install_cached id =
+    if Stateid.equal id !cur_id then () else (* optimization *)
+    let s =
+      match VCS.get_info id with
+      | { state = Some s } -> s
+      | _ -> anomaly (str "unfreezing a non existing state") in
+    unfreeze_global_state s; cur_id := id
+
+  let get_cached id =
+    try match VCS.get_info id with
+    | { state = Some s } -> s
+    | _ -> anomaly (str "not a cached state")
+    with VCS.Expired -> anomaly (str "not a cached state (expired)")
+
+  let assign id what =
+    if VCS.get_state id <> None then () else
+    try match what with
+    | `Full s -> VCS.set_state id s
+    | `Proof(ontop,p) ->
+         if is_cached ontop then (
+           VCS.set_state id { (get_cached ontop) with proof = p })
+    with VCS.Expired -> ()
+
+  let exn_on id ?valid (e, info) =
+    match Stateid.get info with
+    | Some _ -> (e, info)
+    | None ->
+        let loc = Option.default Loc.ghost (Loc.get_loc info) in
+        let (e, info) = Hooks.(call_process_error_once (e, info)) in
+        Hooks.(call execution_error id loc (iprint (e, info)));
+        (e, Stateid.add info ?valid id)
+
+  let same_env { system = s1 } { system = s2 } =
+    let s1 = States.summary_of_state s1 in
+    let e1 = Summary.project_summary s1 [Global.global_env_summary_name] in
+    let s2 = States.summary_of_state s2 in
+    let e2 = Summary.project_summary s2 [Global.global_env_summary_name] in
+    Summary.pointer_equal e1 e2
+
+  let define ?safe_id ?(redefine=false) ?(cache=`No) ?(feedback_processed=true)
+        f id
+  =
+    feedback ~state_id:id Feedback.(ProcessingIn !Flags.async_proofs_worker_id);
+    let str_id = Stateid.to_string id in
+    if is_cached id && not redefine then
+      anomaly (str"defining state "++str str_id++str" twice");
+    try
+      prerr_endline("defining "^str_id^" (cache="^
+        if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)");
+      f ();
+      if cache = `Yes then freeze `No id
+      else if cache = `Shallow then freeze `Shallow id;
+      prerr_endline ("setting cur id to "^str_id);
+      cur_id := id;
+      if feedback_processed then
+        Hooks.(call state_computed id ~in_cache:false);
+      VCS.reached id true;
+      if Proof_global.there_are_pending_proofs () then
+        VCS.goals id (Proof_global.get_open_goals ());
+    with e ->
+      let (e, info) = Errors.push e in
+      let good_id = !cur_id in
+      cur_id := Stateid.dummy;
+      VCS.reached id false;
+      Hooks.(call unreachable_state id);
+      match Stateid.get info, safe_id with
+      | None, None -> iraise (exn_on id ~valid:good_id (e, info))
+      | None, Some good_id -> iraise (exn_on id ~valid:good_id (e, info))
+      | Some _, None -> iraise (e, info)
+      | Some (_,at), Some id -> iraise (e, Stateid.add info ~valid:id at)
+
+end (* }}} *)
+
+
+(****************************** CRUFT *****************************************)
+(******************************************************************************)
+
+(* The backtrack module simulates the classic behavior of a linear document *)
+module Backtrack : sig
+
+  val record : unit -> unit
+  val backto : Stateid.t -> unit
+  val back_safe : unit -> unit
+
+  (* we could navigate the dag, but this ways easy *)
+  val branches_of : Stateid.t -> backup
+
+  (* To be installed during initialization *)
+  val undo_vernac_classifier : vernac_expr -> vernac_classification
+
+end = struct (* {{{ *)
+
+  let record () =
+    List.iter (fun current_branch ->
+      let mine = current_branch, VCS.get_branch current_branch in
+      let info = VCS.get_info (VCS.get_branch_pos current_branch) in
+      let others =
+        CList.map_filter (fun b ->
+          if Vcs_.Branch.equal b current_branch then None
+          else Some(b, VCS.get_branch b)) (VCS.branches ()) in
+      let backup = if fst info.vcs_backup <> None then fst info.vcs_backup
+        else Some (VCS.backup ()) in
+      let branches = if snd info.vcs_backup <> None then snd info.vcs_backup
+        else Some { mine; others } in
+      info.vcs_backup <- backup, branches)
+    [VCS.current_branch (); VCS.Branch.master]
+
+  let backto oid =
+    let info = VCS.get_info oid in
+    match info.vcs_backup with
+    | None, _ ->
+       anomaly(str"Backtrack.backto "++str(Stateid.to_string oid)++
+               str": a state with no vcs_backup")
+    | Some vcs, _ -> VCS.restore vcs
+
+  let branches_of id =
+    let info = VCS.get_info id in
+    match info.vcs_backup with
+    | _, None ->
+       anomaly(str"Backtrack.branches_of "++str(Stateid.to_string id)++
+               str": a state with no vcs_backup")
+    | _, Some x -> x
+
+  let rec fold_until f acc id =
+    let next acc =
+      if id = Stateid.initial then raise Not_found
+      else fold_until f acc (VCS.visit id).next in
+    let info = VCS.get_info id in
+    match info.vcs_backup with
+    | None, _ -> next acc
+    | Some vcs, _ ->
+        let ids =
+          if id = Stateid.initial || id = Stateid.dummy then [] else
+          match VCS.visit id with
+          | { step = `Fork ((_,_,_,l),_) } -> l
+          | { step = `Cmd { cids = l } } -> l
+          | _ -> [] in
+        match f acc (id, vcs, ids) with
+        | `Stop x -> x
+        | `Cont acc -> next acc
+ 
+  let back_safe () =
+    let id =
+      fold_until (fun n (id,_,_) ->
+        if n >= 0 && State.is_cached id then `Stop id else `Cont (succ n))
+        0 (VCS.get_branch_pos (VCS.current_branch ())) in
+    backto id
+
+  let undo_vernac_classifier v =
+    try
+      match v with
+      | VernacResetInitial ->
+          VtStm (VtBack Stateid.initial, true), VtNow
+      | VernacResetName (_,name) ->
+          msg_warning
+            (str"Reset not implemented for automatically generated constants");
+          let id = VCS.get_branch_pos (VCS.current_branch ()) in
+          (try
+            let oid =
+              fold_until (fun b (id,_,label) ->
+                if b then `Stop id else `Cont (List.mem name label))
+              false id in
+            VtStm (VtBack oid, true), VtNow
+          with Not_found ->
+            VtStm (VtBack id, true), VtNow)
+      | VernacBack n ->
+          let id = VCS.get_branch_pos (VCS.current_branch ()) in
+          let oid = fold_until (fun n (id,_,_) ->
+            if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in
+          VtStm (VtBack oid, true), VtNow
+      | VernacUndo n ->
+          let id = VCS.get_branch_pos (VCS.current_branch ()) in
+          let oid = fold_until (fun n (id,_,_) ->
+            if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in
+          if n = 1 && !Flags.coqtop_ui && not !Flags.batch_mode &&
+             not !Flags.print_emacs then
+           VtStm (VtBack oid, false), VtNow
+          else VtStm (VtBack oid, true), VtLater
+      | VernacUndoTo _
+      | VernacRestart as e ->
+          let m = match e with VernacUndoTo m -> m | _ -> 0 in
+          let id = VCS.get_branch_pos (VCS.current_branch ()) in
+          let vcs =
+            match (VCS.get_info id).vcs_backup with 
+            | None, _ -> anomaly(str"Backtrack: tip with no vcs_backup")
+            | Some vcs, _ -> vcs in
+          let cb, _ =
+            Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs) in
+          let n = fold_until (fun n (_,vcs,_) ->
+            if List.mem cb (Vcs_.branches vcs) then `Cont (n+1) else `Stop n)
+            0 id in
+          let oid = fold_until (fun n (id,_,_) ->
+            if Int.equal n 0 then `Stop id else `Cont (n-1)) (n-m-1) id in
+          VtStm (VtBack oid, true), VtLater
+      | VernacAbortAll ->
+          let id = VCS.get_branch_pos (VCS.current_branch ()) in
+          let oid = fold_until (fun () (id,vcs,_) ->
+            match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ())
+            () id in
+          VtStm (VtBack oid, true), VtLater
+      | VernacBacktrack (id,_,_)
+      | VernacBackTo id ->
+          VtStm (VtBack (Stateid.of_int id), not !Flags.print_emacs), VtNow
+      | _ -> VtUnknown, VtNow
+    with
+    | Not_found ->
+       msg_warning(str"undo_vernac_classifier: going back to the initial state.");
+       VtStm (VtBack Stateid.initial, true), VtNow
+
+end (* }}} *)
+
+let hints = ref Aux_file.empty_aux_file
+let set_compilation_hints file =
+  hints := Aux_file.load_aux_file_for file
+let get_hint_ctx loc =
+  let s = Aux_file.get !hints loc "context_used" in
+  let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") s) in
+  let ids = List.map (fun id -> Loc.ghost, id) ids in
+  SsExpr (SsSet ids)
+
+let get_hint_bp_time proof_name =
+  try float_of_string (Aux_file.get !hints Loc.ghost proof_name)
+  with Not_found -> 1.0
+
+let record_pb_time proof_name loc time =
+  let proof_build_time = Printf.sprintf "%.3f" time in
+  Aux_file.record_in_aux_at loc "proof_build_time" proof_build_time;
+  if proof_name <> "" then begin
+    Aux_file.record_in_aux_at Loc.ghost proof_name proof_build_time;
+    hints := Aux_file.set !hints Loc.ghost proof_name proof_build_time
+  end
+ 
+exception RemoteException of std_ppcmds
+let _ = Errors.register_handler (function
+  | RemoteException ppcmd -> ppcmd
+  | _ -> raise Unhandled)
+
+(****************************** THE SCHEDULER *********************************)
+(******************************************************************************)
+
+module rec ProofTask : sig
+ 
+  type competence = Stateid.t list
+  type task_build_proof = {
+    t_exn_info : Stateid.t * Stateid.t;
+    t_start    : Stateid.t;
+    t_stop     : Stateid.t;
+    t_states   : competence;
+    t_assign   : Proof_global.closed_proof_output Future.assignement -> unit;
+    t_loc      : Loc.t;
+    t_uuid     : Future.UUID.t;
+    t_name     : string }
+
+  type task =
+    | BuildProof of task_build_proof
+    | States of Stateid.t list
+
+  type request =
+    | ReqBuildProof of (Future.UUID.t,VCS.vcs) Stateid.request * competence
+    | ReqStates of Stateid.t list
+
+  include AsyncTaskQueue.Task
+  with type task := task
+  and  type competence := competence
+  and  type request := request
+
+  val build_proof_here :
+    Stateid.t * Stateid.t -> Loc.t -> Stateid.t ->
+      Proof_global.closed_proof_output Future.computation
+   
+end = struct (* {{{ *)
+
+  let forward_feedback msg = Hooks.(call forward_feedback msg)
+
+  type competence = Stateid.t list
+  type task_build_proof = {
+    t_exn_info : Stateid.t * Stateid.t;
+    t_start    : Stateid.t;
+    t_stop     : Stateid.t;
+    t_states   : competence;
+    t_assign   : Proof_global.closed_proof_output Future.assignement -> unit;
+    t_loc      : Loc.t;
+    t_uuid     : Future.UUID.t;
+    t_name     : string }
+
+  type task =
+    | BuildProof of task_build_proof
+    | States of Stateid.t list
+
+  type request =
+    | ReqBuildProof of (Future.UUID.t,VCS.vcs) Stateid.request * competence
+    | ReqStates of Stateid.t list
+  
+  type error = {
+    e_error_at    : Stateid.t;
+    e_safe_id     : Stateid.t;
+    e_msg         : std_ppcmds;
+    e_safe_states : Stateid.t list }
+
+  type response =
+    | RespBuiltProof of Proof_global.closed_proof_output * float
+    | RespError of error
+    | RespStates of (Stateid.t * State.partial_state) list
+    | RespDone
+
+  let name = ref "proofworker"
+  let extra_env () = !async_proofs_workers_extra_env
+
+  let task_match age t =
+    match age, t with
+    | `Fresh, BuildProof _ -> true
+    | `Old my_states, States l ->
+        List.for_all (fun x -> CList.mem_f Stateid.equal x my_states) l
+    | _ -> false
+
+  let name_of_task = function
+    | BuildProof t -> "proof: " ^ t.t_name
+    | States l -> "states: " ^ String.concat "," (List.map Stateid.to_string l)
+  let name_of_request = function
+    | ReqBuildProof(r,_) -> "proof: " ^ r.Stateid.name
+    | ReqStates l -> "states: "^String.concat "," (List.map Stateid.to_string l)
+
+  let request_of_task age = function
+    | States l -> Some (ReqStates l)
+    | BuildProof { t_exn_info;t_start;t_stop;t_loc;t_uuid;t_name;t_states } ->
+        assert(age = `Fresh);
+        try Some (ReqBuildProof ({
+          Stateid.exn_info = t_exn_info;
+          stop = t_stop;
+          document = VCS.slice ~start:t_start ~stop:t_stop;
+          loc = t_loc;
+          uuid = t_uuid;
+          name = t_name }, t_states))
+        with VCS.Expired -> None
+
+  let use_response (s : competence AsyncTaskQueue.worker_status) t r =
+    match s, t, r with
+    | `Old c, States _, RespStates l ->
+        List.iter (fun (id,s) -> State.assign id s) l; `End
+    | `Fresh, BuildProof { t_assign; t_loc; t_name; t_states },
+              RespBuiltProof (pl, time) ->
+        feedback (Feedback.InProgress ~-1);
+        t_assign (`Val pl);
+        record_pb_time t_name t_loc time;
+        if not !Flags.async_proofs_full then `End
+        else `Stay(t_states,[States t_states])
+    | `Fresh, BuildProof { t_assign; t_loc; t_name; t_states },
+            RespError { e_error_at; e_safe_id = valid; e_msg; e_safe_states } ->
+        feedback (Feedback.InProgress ~-1);
+        let info = Stateid.add ~valid Exninfo.null e_error_at in
+        let e = (RemoteException e_msg, info) in
+        t_assign (`Exn e);
+        `Stay(t_states,[States e_safe_states])
+    | _ -> assert false
+
+  let on_task_cancellation_or_expiration_or_slave_death = function
+    | None -> ()
+    | Some (States _) -> ()
+    | Some (BuildProof { t_start = start; t_assign }) ->
+        let s = "Worker dies or task expired" in
+        let info = Stateid.add ~valid:start Exninfo.null start in
+        let e = (RemoteException (strbrk s), info) in
+        t_assign (`Exn e);
+        Hooks.(call execution_error start Loc.ghost (strbrk s));
+        feedback (Feedback.InProgress ~-1)
+
+  let build_proof_here (id,valid) loc eop =
+    Future.create (State.exn_on id ~valid) (fun () ->
+      let wall_clock1 = Unix.gettimeofday () in
+      if !Flags.batch_mode then Reach.known_state ~cache:`No eop
+      else Reach.known_state ~cache:`Shallow eop;
+      let wall_clock2 = Unix.gettimeofday () in
+      Aux_file.record_in_aux_at loc "proof_build_time"
+        (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
+      Proof_global.return_proof ())
+
+  let perform_buildp { Stateid.exn_info; stop; document; loc } my_states =
+    try
+      VCS.restore document;
+      VCS.print ();
+      let proof, future_proof, time =
+        let wall_clock = Unix.gettimeofday () in
+        let fp = build_proof_here exn_info loc stop in
+        let proof = Future.force fp in
+        proof, fp, Unix.gettimeofday () -. wall_clock in
+      (* We typecheck the proof with the kernel (in the worker) to spot
+       * the few errors tactics don't catch, like the "fix" tactic building
+       * a bad fixpoint *)
+      let fix_exn = Future.fix_exn_of future_proof in
+      let checked_proof = Future.chain ~pure:false future_proof (fun p ->
+        let pobject, _ =
+          Proof_global.close_future_proof stop (Future.from_val ~fix_exn p) in
+        let terminator = (* The one sent by master is an InvalidKey *)
+          Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in
+        vernac_interp stop
+          ~proof:(pobject, terminator)
+          { verbose = false; loc;
+            expr = (VernacEndProof (Proved (true,None))) }) in
+      ignore(Future.join checked_proof);
+      RespBuiltProof(proof,time)
+    with
+    | e when Errors.noncritical e ->
+        let (e, info) = Errors.push e in
+        (* This can happen if the proof is broken.  The error has also been
+         * signalled as a feedback, hence we can silently recover *)
+        let e_error_at, e_safe_id = match Stateid.get info with
+          | Some (safe, err) -> err, safe
+          | None -> Stateid.dummy, Stateid.dummy in
+        let e_msg = iprint (e, info) in
+        prerr_endline "failed with the following exception:";
+        prerr_endline (string_of_ppcmds e_msg);
+        let e_safe_states = List.filter State.is_cached my_states in
+        RespError { e_error_at; e_safe_id; e_msg; e_safe_states }
+  
+  let perform_states query =
+    if query = [] then [] else
+    let initial = 
+      let rec aux id =
+        try match VCS.visit id with { next } -> aux next
+        with VCS.Expired -> id in
+      aux (List.hd query) in
+    let get_state seen id =
+      let prev =
+        try
+          let { next = prev; step } = VCS.visit id in
+          if State.is_cached prev && List.mem prev seen
+          then Some (prev, State.get_cached prev, step)
+          else None
+        with VCS.Expired -> None in
+      let this = 
+        if State.is_cached id then Some (State.get_cached id) else None in
+      match prev, this with
+      | _, None -> None
+      | Some (prev, o, `Cmd { cast = { expr = VernacSolve _ }}), Some n
+        when State.same_env o n -> (* A pure tactic *)
+          Some (id, `Proof (prev, State.proof_part_of_frozen n))
+      | Some _, Some s ->
+          msg_warning (str "Sending back a fat state");
+          Some (id, `Full s)
+      | _, Some s -> Some (id, `Full s) in
+    let rec aux seen = function
+      | [] -> []
+      | id :: rest ->
+          match get_state seen id with
+          | None -> aux seen rest
+          | Some stuff -> stuff :: aux (id :: seen) rest in
+    aux [initial] query
+
+  let perform = function
+    | ReqBuildProof (bp,states) -> perform_buildp bp states
+    | ReqStates sl -> RespStates (perform_states sl)
+
+  let on_marshal_error s = function
+    | States _ -> msg_error(strbrk("Marshalling error: "^s^". "^
+        "The system state could not be sent to the master process."))
+    | BuildProof { t_exn_info; t_stop; t_assign; t_loc } ->
+      msg_error(strbrk("Marshalling error: "^s^". "^
+        "The system state could not be sent to the worker process. "^
+        "Falling back to local, lazy, evaluation."));
+      t_assign(`Comp(build_proof_here t_exn_info t_loc t_stop));
+      feedback (Feedback.InProgress ~-1)
+
+end (* }}} *)
+
+(* Slave processes (if initialized, otherwise local lazy evaluation) *)
+and Slaves : sig
+
+  (* (eventually) remote calls *)
+  val build_proof : loc:Loc.t ->
+    exn_info:(Stateid.t * Stateid.t) -> start:Stateid.t -> stop:Stateid.t ->
+      name:string -> future_proof * cancel_switch
+
+  (* blocking function that waits for the task queue to be empty *)
+  val wait_all_done : unit -> unit
+  
+  (* initialize the whole machinery (optional) *)
+  val init : unit -> unit
+
+  type 'a tasks = ('a,VCS.vcs) Stateid.request list
+  val dump_snapshot : unit -> Future.UUID.t tasks
+  val check_task : string -> int tasks -> int -> bool
+  val info_tasks : 'a tasks -> (string * float * int) list
+  val finish_task :
+    string ->
+    Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs ->
+    int tasks -> int -> Library.seg_univ
+
+  val cancel_worker : WorkerPool.worker_id -> unit
+
+  val reset_task_queue : unit -> unit
+
+  val set_perspective : Stateid.t list -> unit
+
+end = struct (* {{{ *)
+
+  module TaskQueue = AsyncTaskQueue.MakeQueue(ProofTask)
+  
+  let queue = ref None
+
+  let init () =
+    if Flags.async_proofs_is_master () then
+      queue := Some (TaskQueue.create !Flags.async_proofs_n_workers)
+    else
+      queue := Some (TaskQueue.create 0)
+
+  let check_task_aux extra name l i =
+    let { Stateid.stop; document; loc; name = r_name } = List.nth l i in
+    msg_info(
+      str(Printf.sprintf "Checking task %d (%s%s) of %s" i r_name extra name));
+    VCS.restore document;
+    let start =
+      let rec aux cur =
+        try aux (VCS.visit cur).next
+        with VCS.Expired -> cur in
+      aux stop in
+    try
+      Reach.known_state ~cache:`No stop;
+      (* The original terminator, a hook, has not been saved in the .vio*)
+      Proof_global.set_terminator
+        (Lemmas.standard_proof_terminator []
+          (Lemmas.mk_hook (fun _ _ -> ())));
+      let proof =
+        Proof_global.close_proof ~keep_body_ucst_sepatate:true (fun x -> x) in
+      (* We jump at the beginning since the kernel handles side effects by also
+       * looking at the ones that happen to be present in the current env *)
+      Reach.known_state ~cache:`No start;
+      vernac_interp stop ~proof
+        { verbose = false; loc;
+          expr = (VernacEndProof (Proved (true,None))) };
+      Some proof
+    with e ->
+      let (e, info) = Errors.push e in
+      (try match Stateid.get info with
+      | None ->
+          pperrnl (
+            str"File " ++ str name ++ str ": proof of " ++ str r_name ++
+            spc () ++ iprint (e, info))
+      | Some (_, cur) ->
+          match VCS.visit cur with
+          | { step = `Cmd { cast = { loc } } }
+          | { step = `Fork (( { loc }, _, _, _), _) } 
+          | { step = `Qed ( { qast = { loc } }, _) } 
+          | { step = `Sideff (`Ast ( { loc }, _)) } ->
+              let start, stop = Loc.unloc loc in
+              pperrnl (
+                str"File " ++ str name ++ str ": proof of " ++ str r_name ++
+                str ": chars " ++ int start ++ str "-" ++ int stop ++
+                spc () ++ iprint (e, info))
+          | _ ->
+              pperrnl (
+                str"File " ++ str name ++ str ": proof of " ++ str r_name ++
+                spc () ++ iprint (e, info))
+    with e ->
+      msg_error (str"unable to print error message: " ++
+                    str (Printexc.to_string e))); None
+
+  let finish_task name (u,cst,_) d p l i =
+    let bucket = (List.nth l i).Stateid.uuid in
+    match check_task_aux (Printf.sprintf ", bucket %d" bucket) name l i with
+    | None -> exit 1
+    | Some (po,_) ->
+        let discharge c = List.fold_right Cooking.cook_constr d.(bucket) c in
+        let con =
+          Nametab.locate_constant
+            (Libnames.qualid_of_ident po.Proof_global.id) in
+        let c = Global.lookup_constant con in
+        let o = match c.Declarations.const_body with
+          | Declarations.OpaqueDef o -> o
+          | _ -> assert false in
+        let uc =
+          Option.get
+            (Opaqueproof.get_constraints (Global.opaque_tables ()) o) in
+        let pr =
+          Future.from_val (Option.get (Global.body_of_constant_body c)) in
+        let uc =
+          Future.chain
+            ~greedy:true ~pure:true uc Univ.hcons_universe_context_set in
+        let pr = Future.chain ~greedy:true ~pure:true pr discharge in
+        let pr = Future.chain ~greedy:true ~pure:true pr Constr.hcons in
+        Future.sink pr;
+        let extra = Future.join uc in
+        u.(bucket) <- uc;
+        p.(bucket) <- pr;
+        u, Univ.ContextSet.union cst extra, false
+  
+  let check_task name l i =
+    match check_task_aux "" name l i with
+    | Some _ -> true
+    | None -> false
+
+  let info_tasks l =
+    CList.map_i (fun i { Stateid.loc; name } ->
+      let time1 =
+        try float_of_string (Aux_file.get !hints loc "proof_build_time")
+        with Not_found -> 0.0 in
+      let time2 =
+        try float_of_string (Aux_file.get !hints loc "proof_check_time")
+        with Not_found -> 0.0 in
+      name, max (time1 +. time2) 0.0001,i) 0 l
+
+  let set_perspective idl =
+    let open Stateid in
+    let open ProofTask in
+    let overlap s1 s2 =
+      List.exists (fun x -> CList.mem_f Stateid.equal x s2) s1 in
+    let overlap_rel s1 s2 =
+      match overlap s1 idl, overlap s2 idl with
+      | true, true | false, false -> 0
+      | true, false -> -1
+      | false, true -> 1 in
+    TaskQueue.set_order (Option.get !queue) (fun task1 task2 ->
+     match task1, task2 with
+     | BuildProof { t_states = s1 },
+       BuildProof { t_states = s2 } -> overlap_rel s1 s2
+     | _ -> 0)
+
+  let build_proof ~loc ~exn_info ~start ~stop ~name:pname =
+    let id, valid as t_exn_info = exn_info in
+    let cancel_switch = ref false in
+    if TaskQueue.n_workers (Option.get !queue) = 0 then
+      if !Flags.compilation_mode = Flags.BuildVio then begin
+        let f,assign =
+          Future.create_delegate ~blocking:true (State.exn_on id ~valid) in
+        let t_uuid = Future.uuid f in
+        let task = ProofTask.(BuildProof {
+          t_exn_info; t_start = start; t_stop = stop;
+          t_assign = assign; t_loc = loc; t_uuid; t_name = pname;
+          t_states = VCS.nodes_in_slice ~start ~stop }) in
+        TaskQueue.enqueue_task (Option.get !queue) (task,cancel_switch);
+        f, cancel_switch
+      end else
+        ProofTask.build_proof_here t_exn_info loc stop, cancel_switch
+    else 
+      let f, t_assign = Future.create_delegate (State.exn_on id ~valid) in
+      let t_uuid = Future.uuid f in
+      feedback (Feedback.InProgress 1);
+      let task = ProofTask.(BuildProof {
+        t_exn_info; t_start = start; t_stop = stop; t_assign;
+        t_loc = loc; t_uuid; t_name = pname;
+        t_states = VCS.nodes_in_slice ~start ~stop }) in
+      TaskQueue.enqueue_task (Option.get !queue) (task,cancel_switch);
+      f, cancel_switch
+
+  let wait_all_done () = TaskQueue.join (Option.get !queue)
+
+  let cancel_worker n = TaskQueue.cancel_worker (Option.get !queue) n
+
+  (* For external users this name is nicer than request *)
+  type 'a tasks = ('a,VCS.vcs) Stateid.request list
+  let dump_snapshot () =
+    let tasks = TaskQueue.snapshot (Option.get !queue) in
+    let reqs =
+      CList.map_filter
+        ProofTask.(fun x ->
+             match request_of_task `Fresh x with
+             | Some (ReqBuildProof (r, _)) -> Some r
+             | _ -> None)
+        tasks in
+    prerr_endline (Printf.sprintf "dumping %d tasks\n" (List.length reqs));
+    reqs
+
+  let reset_task_queue () = TaskQueue.clear (Option.get !queue)
+
+end (* }}} *)
+
+and TacTask : sig
+
+  type output = Constr.constr * Evd.evar_universe_context
+  type task = {
+    t_state    : Stateid.t;
+    t_state_fb : Stateid.t;
+    t_assign   : output Future.assignement -> unit;
+    t_ast      : ast;
+    t_goal     : Goal.goal;
+    t_kill     : unit -> unit;
+    t_name     : string }  
+
+  include AsyncTaskQueue.Task with type task := task
+
+end = struct (* {{{ *)
+
+  type output = Constr.constr * Evd.evar_universe_context
+  
+  let forward_feedback msg = Hooks.(call forward_feedback msg)
+
+  type task = {
+    t_state    : Stateid.t;
+    t_state_fb : Stateid.t;
+    t_assign   : output Future.assignement -> unit;
+    t_ast      : ast;
+    t_goal     : Goal.goal;
+    t_kill     : unit -> unit;
+    t_name     : string }  
+
+  type request = {
+    r_state    : Stateid.t;
+    r_state_fb : Stateid.t;
+    r_document : VCS.vcs option;
+    r_ast      : ast;
+    r_goal     : Goal.goal;
+    r_name     : string }
+
+  type response =
+    | RespBuiltSubProof of output
+    | RespError of std_ppcmds
+
+  let name = ref "tacworker"
+  let extra_env () = [||]
+  type competence = unit
+  let task_match _ _ = true
+
+  (* run by the master, on a thread *)
+  let request_of_task age { t_state; t_state_fb; t_ast; t_goal; t_name } =
+    try Some {
+      r_state    = t_state;
+      r_state_fb = t_state_fb;
+      r_document =
+        if age <> `Fresh then None
+        else Some (VCS.slice ~start:t_state ~stop:t_state);
+      r_ast      = t_ast;
+      r_goal     = t_goal;
+      r_name     = t_name }
+    with VCS.Expired -> None
+          
+  let use_response _ { t_assign; t_state; t_state_fb; t_kill } resp =
+    match resp with
+    | RespBuiltSubProof o -> t_assign (`Val o); `Stay ((),[])
+    | RespError msg ->
+        let info = Stateid.add ~valid:t_state Exninfo.null t_state_fb in
+        let e = (RemoteException msg, info) in
+        t_assign (`Exn e);
+        t_kill ();
+        `Stay ((),[])
+                    
+  let on_marshal_error err { t_name } =
+    pr_err ("Fatal marshal error: " ^ t_name );
+    flush_all (); exit 1
+
+  let on_task_cancellation_or_expiration_or_slave_death = function
+    | Some { t_kill } -> t_kill ()
+    | _ -> ()
+ 
+  let perform { r_state = id; r_state_fb; r_document = vcs; r_ast; r_goal } =
+    Option.iter VCS.restore vcs;
+    try
+      Reach.known_state ~cache:`No id;
+      let t, uc = Future.purify (fun () ->
+        vernac_interp r_state_fb r_ast;
+        let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in
+        match Evd.(evar_body (find sigma r_goal)) with
+        | Evd.Evar_empty -> Errors.errorlabstrm "Stm" (str "no progress")
+        | Evd.Evar_defined t ->
+            let t = Evarutil.nf_evar sigma t in
+            if Evarutil.is_ground_term sigma t then
+              t, Evd.evar_universe_context sigma
+            else Errors.errorlabstrm "Stm" (str"The solution is not ground"))
+        () in
+      RespBuiltSubProof (t,uc) 
+    with e when Errors.noncritical e -> RespError (Errors.print e)
+
+  let name_of_task { t_name } = t_name
+  let name_of_request { r_name } = r_name
+  
+end (* }}} *)
+
+and Partac : sig
+
+  val vernac_interp :
+    cancel_switch -> int -> Stateid.t -> Stateid.t -> ast -> unit
+
+end = struct (* {{{ *)
+    
+  module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask)
+
+  let vernac_interp cancel nworkers safe_id id { verbose; loc; expr = e } =
+    let e, etac, time, fail =
+      let rec find time fail = function
+        | VernacSolve(_,_,re,b) -> re, b, time, fail
+        | VernacTime [_,e] -> find true fail e
+        | VernacFail e -> find time true e
+        | _ -> errorlabstrm "Stm" (str"unsupported") in find false false e in
+    Hooks.call Hooks.with_fail fail (fun () ->
+    (if time then System.with_time false else (fun x -> x)) (fun () ->
+    ignore(TaskQueue.with_n_workers nworkers (fun queue ->
+    Proof_global.with_current_proof (fun _ p ->
+      let goals, _, _, _, _ = Proof.proof p in
+      let open TacTask in
+      let res = CList.map_i (fun i g ->
+        let f,assign= Future.create_delegate (State.exn_on id ~valid:safe_id) in
+        let t_ast =
+          { verbose;loc;expr = VernacSolve(SelectNth i,None,e,etac) } in
+        let t_name = Goal.uid g in
+        TaskQueue.enqueue_task queue
+          ({ t_state = safe_id; t_state_fb = id;
+            t_assign = assign; t_ast; t_goal = g; t_name;
+            t_kill = (fun () -> TaskQueue.cancel_all queue) }, cancel);
+        Goal.uid g,f)
+        1 goals in
+      TaskQueue.join queue;
+      let assign_tac : unit Proofview.tactic =
+        Proofview.V82.tactic (fun gl ->
+          let open Tacmach in
+          let sigma, g = project gl, sig_it gl in
+          let gid = Goal.uid g in
+          let f =
+            try List.assoc gid res
+            with Not_found -> Errors.anomaly(str"Partac: wrong focus") in
+          if Future.is_over f then
+            let pt, uc = Future.join f in
+            prerr_endline (string_of_ppcmds(hov 0 (
+              str"g=" ++ str gid ++ spc () ++
+              str"t=" ++ (Printer.pr_constr pt) ++ spc () ++
+              str"uc=" ++ Evd.pr_evar_universe_context uc)));
+            let sigma = Goal.V82.partial_solution sigma g pt in
+            let sigma = Evd.merge_universe_context sigma uc in
+            re_sig [] sigma
+          else (* One has failed and cancelled the others, but not this one *)
+            re_sig [g] sigma) in
+      Proof.run_tactic (Global.env()) assign_tac p)))) ())
+  
+end (* }}} *)
+
+and QueryTask : sig
+
+  type task = { t_where : Stateid.t; t_for : Stateid.t ; t_what : ast }
+  include AsyncTaskQueue.Task with type task := task
+
+end = struct (* {{{ *)
+  
+  type task =
+    { t_where : Stateid.t; t_for : Stateid.t ; t_what : ast }
+  
+  type request =
+    { r_where : Stateid.t ; r_for : Stateid.t ; r_what : ast; r_doc : VCS.vcs }
+  type response = unit
+
+  let name = ref "queryworker"
+  let extra_env _ = [||]
+  type competence = unit
+  let task_match _ _ = true
+
+  let request_of_task _ { t_where; t_what; t_for } =
+    try Some {
+      r_where = t_where;
+      r_for   = t_for;
+      r_doc   = VCS.slice ~start:t_where ~stop:t_where;
+      r_what  = t_what }
+    with VCS.Expired -> None
+  
+  let use_response _ _ _ = `End
+
+  let on_marshal_error _ _ =
+    pr_err ("Fatal marshal error in query");
+    flush_all (); exit 1
+
+  let on_task_cancellation_or_expiration_or_slave_death _ = ()
+  
+  let forward_feedback msg = Hooks.(call forward_feedback msg)
+
+  let perform { r_where; r_doc; r_what; r_for } =
+    VCS.restore r_doc;
+    VCS.print ();
+    Reach.known_state ~cache:`No r_where;
+    try
+      vernac_interp r_for { r_what with verbose = true };
+      feedback ~state_id:r_for Feedback.Processed     
+    with e when Errors.noncritical e ->
+      let msg = string_of_ppcmds (print e) in
+      feedback ~state_id:r_for (Feedback.ErrorMsg (Loc.ghost, msg))
+    
+  let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what)
+  let name_of_request { r_what } = string_of_ppcmds (pr_ast r_what)
+
+end (* }}} *)
+
+and Query : sig 
+
+  val init : unit -> unit
+  val vernac_interp : cancel_switch -> Stateid.t ->  Stateid.t -> ast -> unit
+
+end = struct (* {{{ *)
+
+  module TaskQueue = AsyncTaskQueue.MakeQueue(QueryTask)
+
+  let queue = ref None
+
+  let vernac_interp switch prev id q =
+    assert(TaskQueue.n_workers (Option.get !queue) > 0);
+    TaskQueue.enqueue_task (Option.get !queue)
+      QueryTask.({ QueryTask.t_where = prev; t_for = id; t_what = q }, switch)
+
+  let init () = queue := Some (TaskQueue.create
+    (if !Flags.async_proofs_full then 1 else 0))
+
+end (* }}} *)
+
+(* Runs all transactions needed to reach a state *)
+and Reach : sig
+
+  val known_state :
+    ?redefine_qed:bool -> cache:Summary.marshallable -> Stateid.t -> unit
+
+end = struct (* {{{ *)
+
+let pstate = ["meta counter"; "evar counter"; "program-tcc-table"]
+
+let async_policy () =
+  let open Flags in
+  if interactive () = `Yes then
+    (async_proofs_is_master () || !async_proofs_mode = Flags.APonLazy)
+  else
+    (!compilation_mode = Flags.BuildVio || !async_proofs_mode <> Flags.APoff)
+
+let delegate name =
+  let time = get_hint_bp_time name in
+  time >= 1.0 || !Flags.compilation_mode = Flags.BuildVio
+
+let collect_proof keep cur hd brkind id =
+ prerr_endline ("Collecting proof ending at "^Stateid.to_string id);
+ let no_name = "" in
+ let name = function
+   | [] -> no_name
+   | id :: _ -> Id.to_string id in
+ let loc = (snd cur).loc in
+ let is_defined = function
+   | _, { expr = VernacEndProof (Proved (false,_)) } -> true
+   | _ -> false in
+ let proof_using_ast = function
+   | Some (_, ({ expr = VernacProof(_,Some _) } as v)) -> Some v
+   | _ -> None in
+ let has_proof_using x = proof_using_ast x <> None in
+ let proof_no_using = function
+   | Some (_, ({ expr = VernacProof(t,None) } as v)) -> t,v
+   | _ -> assert false in
+ let has_proof_no_using = function
+   | Some (_, { expr = VernacProof(_,None) }) -> true
+   | _ -> false in
+ let parent = function Some (p, _) -> p | None -> assert false in
+ let rec collect last accn id =
+    let view = VCS.visit id in
+    match view.step with
+    | `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next
+    (* An Alias could jump everywhere... we hope we can ignore it*)
+    | `Alias _ -> `Sync (no_name,None,`Alias)
+    | `Fork((_,_,_,_::_::_), _) ->
+        `Sync (no_name,proof_using_ast last,`MutualProofs)
+    | `Fork((_,_,Doesn'tGuaranteeOpacity,_), _) ->
+        `Sync (no_name,proof_using_ast last,`Doesn'tGuaranteeOpacity)
+    | `Fork((_,hd',GuaranteesOpacity,ids), _) when has_proof_using last ->
+        assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
+        let name = name ids in
+        `ASync (parent last,proof_using_ast last,accn,name,delegate name)
+    | `Fork((_, hd', GuaranteesOpacity, ids), _) when
+       has_proof_no_using last && not (State.is_cached (parent last)) &&
+       !Flags.compilation_mode = Flags.BuildVio ->
+        assert (VCS.Branch.equal hd hd'||VCS.Branch.equal hd VCS.edit_branch);
+        (try
+          let name, hint = name ids, get_hint_ctx loc  in
+          let t, v = proof_no_using last in
+          v.expr <- VernacProof(t, Some hint);
+          `ASync (parent last,proof_using_ast last,accn,name,delegate name)
+        with Not_found -> `Sync (no_name,None,`NoHint))
+    | `Fork((_, hd', GuaranteesOpacity, ids), _) ->
+        assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
+        let name = name ids in
+        `MaybeASync (parent last, None, accn, name, delegate name)
+    | `Sideff _ -> `Sync (no_name,None,`NestedProof)
+    | _ -> `Sync (no_name,None,`Unknown) in
+ let make_sync why = function
+   | `Sync(name,pua,_) -> `Sync (name,pua,why)
+   | `MaybeASync(_,pua,_,name,_) -> `Sync (name,pua,why)
+   | `ASync(_,pua,_,name,_) -> `Sync (name,pua,why) in
+ let check_policy rc = if async_policy () then rc else make_sync `Policy rc in
+ match cur, (VCS.visit id).step, brkind with
+ | (parent, { expr = VernacExactProof _ }), `Fork _, _ ->
+     `Sync (no_name,None,`Immediate)
+ | _, _, { VCS.kind = `Edit _ }  -> check_policy (collect (Some cur) [] id)
+ | _ ->
+     if is_defined cur then `Sync (no_name,None,`Transparent)
+     else if keep == VtDrop then `Sync (no_name,None,`Aborted)
+     else
+       let rc = collect (Some cur) [] id in
+       if keep == VtKeep &&
+          (not(State.is_cached id) || !Flags.async_proofs_full)
+       then check_policy rc
+       else make_sync `AlreadyEvaluated rc
+
+let string_of_reason = function
+  | `Transparent -> "Transparent"
+  | `AlreadyEvaluated -> "AlreadyEvaluated"
+  | `Policy -> "Policy"
+  | `NestedProof -> "NestedProof"
+  | `Immediate -> "Immediate"
+  | `Alias -> "Alias"
+  | `NoHint -> "NoHint"
+  | `Doesn'tGuaranteeOpacity -> "Doesn'tGuaranteeOpacity"
+  | `Aborted -> "Aborted"
+  | _ -> "Unknown Reason"
+
+let wall_clock_last_fork = ref 0.0
+
+let known_state ?(redefine_qed=false) ~cache id =
+
+  (* ugly functions to process nested lemmas, i.e. hard to reproduce
+   * side effects *)
+  let cherry_pick_non_pstate () =
+    Summary.freeze_summary ~marshallable:`No ~complement:true pstate,
+    Lib.freeze ~marshallable:`No in
+  let inject_non_pstate (s,l) = Summary.unfreeze_summary s; Lib.unfreeze l in
+
+  let rec pure_cherry_pick_non_pstate id = Future.purify (fun id ->
+    prerr_endline ("cherry-pick non pstate " ^ Stateid.to_string id);
+    reach id;
+    cherry_pick_non_pstate ()) id
+
+  (* traverses the dag backward from nodes being already calculated *)
+  and reach ?(redefine_qed=false) ?(cache=cache) id =
+    prerr_endline ("reaching: " ^ Stateid.to_string id);
+    if not redefine_qed && State.is_cached ~cache id then begin
+      State.install_cached id;
+      Hooks.(call state_computed id ~in_cache:true);
+      prerr_endline ("reached (cache)")
+    end else
+    let step, cache_step, feedback_processed =
+      let view = VCS.visit id in
+      match view.step with
+      | `Alias id -> (fun () ->
+            reach view.next; reach id
+          ), cache, true
+      | `Cmd { cast = x; cqueue = `TacQueue cancel } -> (fun () ->
+            reach ~cache:`Shallow view.next;
+            Partac.vernac_interp
+              cancel !Flags.async_proofs_n_tacworkers view.next id x
+          ), cache, true
+      | `Cmd { cast = x; cqueue = `QueryQueue cancel }
+        when Flags.async_proofs_is_master () -> (fun () ->
+            reach ~cache:`Shallow view.next;
+            Query.vernac_interp cancel view.next id x
+          ), cache, false
+      | `Cmd { cast = x } -> (fun () ->
+            reach view.next; vernac_interp id x
+          ), cache, true
+      | `Fork ((x,_,_,_), None) -> (fun () ->
+            reach view.next; vernac_interp id x;
+            wall_clock_last_fork := Unix.gettimeofday ()
+          ), `Yes, true
+      | `Fork ((x,_,_,_), Some prev) -> (fun () ->
+            reach ~cache:`Shallow prev;
+            reach view.next;
+            (try vernac_interp id x;
+            with e when Errors.noncritical e ->
+              let (e, info) = Errors.push e in
+              let info = Stateid.add info ~valid:prev id in
+              iraise (e, info));
+            wall_clock_last_fork := Unix.gettimeofday ()
+          ), `Yes, true
+      | `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) ->
+          let rec aux = function
+          | `ASync (start, pua, nodes, name, delegate) -> (fun () ->
+                assert(keep == VtKeep);
+                let stop, exn_info, loc = eop, (id, eop), x.loc in
+                prerr_endline ("Asynchronous " ^ Stateid.to_string id);
+                VCS.create_cluster nodes ~qed:id ~start;
+                begin match brinfo, qed.fproof with
+                | { VCS.kind = `Edit _ }, None -> assert false
+                | { VCS.kind = `Edit _ }, Some (ofp, cancel) ->
+                    assert(redefine_qed = true);
+                    let fp, cancel =
+                      Slaves.build_proof ~loc ~exn_info ~start ~stop ~name in
+                    Future.replace ofp fp;
+                    qed.fproof <- Some (fp, cancel)
+                | { VCS.kind = `Proof _ }, Some _ -> assert false
+                | { VCS.kind = `Proof _ }, None ->
+                    reach ~cache:`Shallow start;
+                    let fp, cancel =
+                      if delegate then
+                        Slaves.build_proof ~loc ~exn_info ~start ~stop ~name
+                      else
+                        ProofTask.build_proof_here exn_info loc stop, ref false
+                    in
+                    qed.fproof <- Some (fp, cancel);
+                    let proof =
+                      Proof_global.close_future_proof ~feedback_id:id fp in
+                    if not delegate then ignore(Future.compute fp);
+                    reach view.next;
+                    vernac_interp id ~proof x;
+                    feedback ~state_id:id Feedback.Incomplete
+                | { VCS.kind = `Master }, _ -> assert false
+                end;
+                Proof_global.discard_all ()
+              ), (if redefine_qed then `No else `Yes), true
+          | `Sync (name, _, `Immediate) -> (fun () -> 
+                assert (Stateid.equal view.next eop);
+                reach eop; vernac_interp id x; Proof_global.discard_all ()
+              ), `Yes, true
+          | `Sync (name, pua, reason) -> (fun () ->
+                prerr_endline ("Synchronous " ^ Stateid.to_string id ^ " " ^
+                  string_of_reason reason);
+                reach eop;
+                let wall_clock = Unix.gettimeofday () in
+                record_pb_time name x.loc (wall_clock -. !wall_clock_last_fork);
+                let proof =
+                  if keep != VtKeep then None
+                  else Some(Proof_global.close_proof
+                              ~keep_body_ucst_sepatate:false
+                              (State.exn_on id ~valid:eop)) in
+                if proof = None then prerr_endline "NONE!!!!!";
+                reach view.next;
+                if keep == VtKeepAsAxiom then
+                  Option.iter (vernac_interp id) pua;
+                let wall_clock2 = Unix.gettimeofday () in
+                vernac_interp id ?proof x;
+                let wall_clock3 = Unix.gettimeofday () in
+                Aux_file.record_in_aux_at x.loc "proof_check_time"
+                  (Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2));
+                Proof_global.discard_all ()
+              ), `Yes, true
+          | `MaybeASync (start, pua, nodes, name, delegate) -> (fun () ->
+                prerr_endline ("MaybeAsynchronous " ^ Stateid.to_string id);
+                reach ~cache:`Shallow start;
+                (* no sections *)
+                if List.is_empty (Environ.named_context (Global.env ()))
+                then pi1 (aux (`ASync (start, pua, nodes, name, delegate))) ()
+                else pi1 (aux (`Sync (name, pua, `Unknown))) ()
+              ), (if redefine_qed then `No else `Yes), true
+          in
+          aux (collect_proof keep (view.next, x) brname brinfo eop)
+      | `Sideff (`Ast (x,_)) -> (fun () ->
+            reach view.next; vernac_interp id x;
+          ), cache, true
+      | `Sideff (`Id origin) -> (fun () ->
+            reach view.next;
+            inject_non_pstate (pure_cherry_pick_non_pstate origin);
+          ), cache, true
+    in
+    let cache_step =
+      if !Flags.async_proofs_cache = Some Flags.Force then `Yes
+      else cache_step in
+    State.define
+      ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id;
+    prerr_endline ("reached: "^ Stateid.to_string id) in
+  reach ~redefine_qed id
+
+end (* }}} *)
+
+(********************************* STM API ************************************)
+(******************************************************************************)
+
+let init () =
+  VCS.init Stateid.initial;
+  set_undo_classifier Backtrack.undo_vernac_classifier;
+  State.define ~cache:`Yes (fun () -> ()) Stateid.initial;
+  Backtrack.record ();
+  Slaves.init ();
+  if Flags.async_proofs_is_master () then begin
+    prerr_endline "Initialising workers";
+    Query.init ();
+    let opts = match !Flags.async_proofs_private_flags with
+      | None -> []
+      | Some s -> Str.split_delim (Str.regexp ",") s in
+    begin try
+      let env_opt = Str.regexp "^extra-env=" in
+      let env = List.find (fun s -> Str.string_match env_opt s 0) opts in
+      async_proofs_workers_extra_env := Array.of_list
+        (Str.split_delim (Str.regexp ";") (Str.replace_first env_opt "" env))
+    with Not_found -> () end;
+  end
+
+let observe id =
+  let vcs = VCS.backup () in
+  try
+    Reach.known_state ~cache:(interactive ()) id;
+    VCS.print ()
+  with e ->
+    let e = Errors.push e in
+    VCS.print ();
+    VCS.restore vcs;
+    iraise e
+
+let finish ?(print_goals=false) () =
+  observe (VCS.get_branch_pos (VCS.current_branch ()));
+  if print_goals then msg_notice (pr_open_cur_subgoals ());
+  VCS.print ()
+
+let wait () =
+  Slaves.wait_all_done ();
+  VCS.print ()
+
+let join () =
+  finish ();
+  wait ();
+  prerr_endline "Joining the environment";
+  Global.join_safe_environment ();
+  VCS.print ();
+  VCS.print ()
+
+let dump_snapshot () = Slaves.dump_snapshot (), RemoteCounter.snapshot ()
+type document = VCS.vcs
+type tasks = int Slaves.tasks * RemoteCounter.remote_counters_status
+let check_task name (tasks,rcbackup) i =
+  RemoteCounter.restore rcbackup;
+  let vcs = VCS.backup () in
+  try
+    let rc = Future.purify (Slaves.check_task name tasks) i in
+    pperr_flush ();
+    VCS.restore vcs;
+    rc
+  with e when Errors.noncritical e -> VCS.restore vcs; false
+let info_tasks (tasks,_) = Slaves.info_tasks tasks
+let finish_tasks name u d p (t,rcbackup as tasks) =
+  RemoteCounter.restore rcbackup;
+  let finish_task u (_,_,i) =
+    let vcs = VCS.backup () in
+    let u = Future.purify (Slaves.finish_task name u d p t) i in
+    pperr_flush ();
+    VCS.restore vcs;
+    u in
+  try
+    let u, a, _ = List.fold_left finish_task u (info_tasks tasks) in
+    (u,a,true), p
+  with e ->
+    let e = Errors.push e in
+    pperrnl (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e);
+    exit 1
+
+let merge_proof_branch ?id qast keep brname =
+  let brinfo = VCS.get_branch brname in
+  let qed fproof = { qast; keep; brname; brinfo; fproof } in
+  match brinfo with
+  | { VCS.kind = `Proof _ } ->
+      VCS.checkout VCS.Branch.master;
+      let id = VCS.new_node ?id () in
+      VCS.merge id ~ours:(Qed (qed None)) brname;
+      VCS.delete_branch brname;
+      if keep <> VtDrop then VCS.propagate_sideff None;
+      `Ok
+  | { VCS.kind = `Edit (mode, qed_id, master_id) } ->
+      let ofp =
+        match VCS.visit qed_id with
+        | { step = `Qed ({ fproof }, _) } -> fproof
+        | _ -> assert false in
+      VCS.rewrite_merge qed_id ~ours:(Qed (qed ofp)) ~at:master_id brname;
+      VCS.delete_branch brname;
+      VCS.gc ();
+      Reach.known_state ~redefine_qed:true ~cache:`No qed_id;
+      VCS.checkout VCS.Branch.master;
+      `Unfocus qed_id
+  | { VCS.kind = `Master } ->
+       iraise (State.exn_on Stateid.dummy (Proof_global.NoCurrentProof, Exninfo.null))
+
+(* When tty is true, this code also does some of the job of the user interface:
+   jump back to a state that is valid *)
+let handle_failure (e, info) vcs tty =
+  if e = Errors.Drop then iraise (e, info) else
+  match Stateid.get info with
+  | None ->
+      VCS.restore vcs;
+      VCS.print ();
+      if tty && interactive () = `Yes then begin
+        (* Hopefully the 1 to last state is valid *)
+        Backtrack.back_safe (); 
+        VCS.checkout_shallowest_proof_branch ();
+      end;
+      VCS.print ();
+      anomaly(str"error with no safe_id attached:" ++ spc() ++
+        Errors.print_no_report e)
+  | Some (safe_id, id) ->
+      prerr_endline ("Failed at state " ^ Stateid.to_string id);
+      VCS.restore vcs;
+      if tty && interactive () = `Yes then begin
+        (* We stay on a valid state *)
+        Backtrack.backto safe_id;
+        VCS.checkout_shallowest_proof_branch ();
+        Reach.known_state ~cache:(interactive ()) safe_id;
+      end;
+      VCS.print ();
+      iraise (e, info)
+
+let snapshot_vio ldir long_f_dot_v =
+  finish ();
+  if List.length (VCS.branches ()) > 1 then
+    Errors.errorlabstrm "stm" (str"Cannot dump a vio with open proofs");
+  Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_v
+    (Global.opaque_tables ())
+
+let reset_task_queue = Slaves.reset_task_queue
+
+(* Document building *)
+let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
+  let warn_if_pos a b =
+    if b then msg_warning(pr_ast a ++ str" should not be part of a script") in
+  let v, x = expr, { verbose = verbose; loc; expr } in
+  prerr_endline ("{{{ processing: "^ string_of_ppcmds (pr_ast x));
+  let vcs = VCS.backup () in
+  try
+    let head = VCS.current_branch () in
+    VCS.checkout head;
+    let rc = begin
+      prerr_endline ("  classified as: " ^ string_of_vernac_classification c);
+      match c with
+      (* PG stuff *)    
+      | VtStm(VtPG,false), VtNow -> vernac_interp Stateid.dummy x; `Ok
+      | VtStm(VtPG,_), _ -> anomaly(str "PG command in script or VtLater")
+      (* Joining various parts of the document *)
+      | VtStm (VtJoinDocument, b), VtNow -> warn_if_pos x b; join (); `Ok
+      | VtStm (VtFinish, b),       VtNow -> warn_if_pos x b; finish (); `Ok
+      | VtStm (VtWait, b),     VtNow -> warn_if_pos x b; finish (); wait (); `Ok
+      | VtStm (VtPrintDag, b), VtNow ->
+          warn_if_pos x b; VCS.print ~now:true (); `Ok
+      | VtStm (VtObserve id, b),   VtNow -> warn_if_pos x b; observe id; `Ok
+      | VtStm ((VtObserve _ | VtFinish | VtJoinDocument
+                |VtPrintDag |VtWait),_), VtLater ->
+          anomaly(str"classifier: join actions cannot be classified as VtLater")
+      
+      (* Back *)
+      | VtStm (VtBack oid, true), w ->
+          let id = VCS.new_node ~id:newtip () in
+          let { mine; others } = Backtrack.branches_of oid in
+          List.iter (fun branch ->
+            if not (List.mem_assoc branch (mine::others)) then
+              ignore(merge_proof_branch x VtDrop branch))
+            (VCS.branches ());
+          VCS.checkout_shallowest_proof_branch ();
+          let head = VCS.current_branch () in
+          List.iter (fun b ->
+            if not(VCS.Branch.equal b head) then begin
+              VCS.checkout b;
+              VCS.commit (VCS.new_node ()) (Alias oid);
+            end)
+            (VCS.branches ());
+          VCS.checkout_shallowest_proof_branch ();
+          VCS.commit id (Alias oid);
+          Backtrack.record (); if w == VtNow then finish (); `Ok
+      | VtStm (VtBack id, false), VtNow ->
+          prerr_endline ("undo to state " ^ Stateid.to_string id);
+          Backtrack.backto id;
+          VCS.checkout_shallowest_proof_branch ();
+          Reach.known_state ~cache:(interactive ()) id; `Ok
+      | VtStm (VtBack id, false), VtLater ->
+          anomaly(str"classifier: VtBack + VtLater must imply part_of_script")
+
+      (* Query *)
+      | VtQuery (false,(report_id,route)), VtNow when tty = true ->
+          finish ();
+          (try Future.purify (vernac_interp report_id ~route)
+                  { verbose = true; loc; expr }
+           with e when Errors.noncritical e ->
+             let e = Errors.push e in
+             iraise (State.exn_on report_id e)); `Ok
+      | VtQuery (false,(report_id,route)), VtNow ->
+          (try vernac_interp report_id ~route x
+           with e when Errors.noncritical e ->
+             let e = Errors.push e in
+             iraise (State.exn_on report_id e)); `Ok
+      | VtQuery (true,(report_id,_)), w ->
+          assert(Stateid.equal report_id Stateid.dummy);
+          let id = VCS.new_node ~id:newtip () in
+          let queue =
+            if !Flags.async_proofs_full then `QueryQueue (ref false)
+            else `MainQueue in
+          VCS.commit id (Cmd { cast = x; cids = []; cqueue = queue });
+          Backtrack.record (); if w == VtNow then finish (); `Ok
+      | VtQuery (false,_), VtLater ->
+          anomaly(str"classifier: VtQuery + VtLater must imply part_of_script")
+
+      (* Proof *)
+      | VtStartProof (mode, guarantee, names), w ->
+          let id = VCS.new_node ~id:newtip () in
+          let bname = VCS.mk_branch_name x in
+          VCS.checkout VCS.Branch.master;
+          if VCS.Branch.equal head VCS.Branch.master then begin
+            VCS.commit id (Fork (x, bname, guarantee, names));
+            VCS.branch bname (`Proof (mode, VCS.proof_nesting () + 1))
+          end else begin
+            VCS.branch bname (`Proof (mode, VCS.proof_nesting () + 1));
+            VCS.merge id ~ours:(Fork (x, bname, guarantee, names)) head
+          end;
+          Proof_global.activate_proof_mode mode;
+          Backtrack.record (); if w == VtNow then finish (); `Ok
+      | VtProofMode _, VtLater ->
+          anomaly(str"VtProofMode must be executed VtNow")
+      | VtProofMode mode, VtNow ->
+          let id = VCS.new_node ~id:newtip () in
+          VCS.checkout VCS.Branch.master;
+          VCS.commit id (Cmd {cast = x; cids=[]; cqueue = `MainQueue});
+          VCS.propagate_sideff (Some x);
+          List.iter
+            (fun bn -> match VCS.get_branch bn with
+            | { VCS.root; kind = `Master; pos } -> ()
+            | { VCS.root; kind = `Proof(_,d); pos } ->
+                VCS.delete_branch bn;
+                VCS.branch ~root ~pos bn (`Proof(mode,d))
+            | { VCS.root; kind = `Edit(_,f,q); pos } ->
+                VCS.delete_branch bn;
+                VCS.branch ~root ~pos bn (`Edit(mode,f,q)))
+            (VCS.branches ());
+          VCS.checkout_shallowest_proof_branch ();
+          Backtrack.record ();
+          finish ();
+          `Ok
+      | VtProofStep paral, w ->
+          let id = VCS.new_node ~id:newtip () in
+          let queue = if paral then `TacQueue (ref false) else `MainQueue in
+          VCS.commit id (Cmd {cast = x; cids = []; cqueue = queue });
+          Backtrack.record (); if w == VtNow then finish (); `Ok
+      | VtQed keep, w ->
+          let rc = merge_proof_branch ~id:newtip x keep head in
+          VCS.checkout_shallowest_proof_branch ();
+          Backtrack.record (); if w == VtNow then finish ();
+          rc
+          
+      (* Side effect on all branches *)
+      | VtUnknown, _ when expr = VernacToplevelControl Drop ->
+          vernac_interp (VCS.get_branch_pos head) x; `Ok
+
+      | VtSideff l, w ->
+          let id = VCS.new_node ~id:newtip () in
+          VCS.checkout VCS.Branch.master;
+          VCS.commit id (Cmd { cast = x; cids = l; cqueue = `MainQueue});
+          VCS.propagate_sideff (Some x);
+          VCS.checkout_shallowest_proof_branch ();
+          Backtrack.record (); if w == VtNow then finish (); `Ok
+
+      (* Unknown: we execute it, check for open goals and propagate sideeff *)
+      | VtUnknown, VtNow ->
+          let id = VCS.new_node ~id:newtip () in
+          let head_id = VCS.get_branch_pos head in
+          Reach.known_state ~cache:`Yes head_id; (* ensure it is ok *)
+          let step () =
+            VCS.checkout VCS.Branch.master;
+            let mid = VCS.get_branch_pos VCS.Branch.master in
+            Reach.known_state ~cache:(interactive ()) mid;
+            vernac_interp id x;
+            (* Vernac x may or may not start a proof *)
+            if VCS.Branch.equal head VCS.Branch.master &&
+               Proof_global.there_are_pending_proofs ()
+            then begin
+              let bname = VCS.mk_branch_name x in
+              VCS.commit id (Fork (x,bname,Doesn'tGuaranteeOpacity,[]));
+              VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1));
+              Proof_global.activate_proof_mode "Classic";
+            end else begin
+              VCS.commit id (Cmd { cast = x; cids = []; cqueue = `MainQueue});
+              VCS.propagate_sideff (Some x);
+              VCS.checkout_shallowest_proof_branch ();
+            end in
+          State.define ~safe_id:head_id ~cache:`Yes step id;
+          Backtrack.record (); `Ok
+
+      | VtUnknown, VtLater ->
+          anomaly(str"classifier: VtUnknown must imply VtNow")
+    end in
+    (* Proof General *)
+    begin match v with 
+      | VernacStm (PGLast _) ->
+        if not (VCS.Branch.equal head VCS.Branch.master) then
+          vernac_interp Stateid.dummy
+            { verbose = true; loc = Loc.ghost;
+              expr = VernacShow (ShowGoal OpenSubgoals) }
+      | _ -> ()
+    end;
+    prerr_endline "processed }}}";
+    VCS.print ();
+    rc
+  with e ->
+    let e = Errors.push e in
+    handle_failure e vcs tty
+
+let print_ast id =
+  try
+    match VCS.visit id with
+    | { step = `Cmd { cast = { loc; expr } } }
+    | { step = `Fork (({ loc; expr }, _, _, _), _) } 
+    | { step = `Qed ({ qast = { loc; expr } }, _) } ->
+        let xml = 
+          try Texmacspp.tmpp expr loc
+          with e -> Xml_datatype.PCData ("ERROR " ^ Printexc.to_string e) in
+        xml;
+    | _ -> Xml_datatype.PCData "ERROR"
+  with _ -> Xml_datatype.PCData "ERROR"
+
+let stop_worker n = Slaves.cancel_worker n
+
+let add ~ontop ?newtip ?(check=ignore) verb eid s =
+  let cur_tip = VCS.cur_tip () in
+  if Stateid.equal ontop cur_tip then begin
+    let _, ast as loc_ast = vernac_parse ?newtip eid s in
+    check(loc_ast);
+    let clas = classify_vernac ast in
+    match process_transaction ?newtip ~tty:false verb clas loc_ast with
+    | `Ok -> VCS.cur_tip (), `NewTip
+    | `Unfocus qed_id -> qed_id, `Unfocus (VCS.cur_tip ())
+  end else begin
+    (* For now, arbitrary edits should be announced with edit_at *)
+    anomaly(str"Not yet implemented, the GUI should not try this")
+  end
+
+let set_perspective id_list = Slaves.set_perspective id_list
+
+type focus = {
+  start : Stateid.t;
+  stop : Stateid.t;
+  tip : Stateid.t
+}
+
+let query ~at ?(report_with=(Stateid.dummy,Feedback.default_route)) s =
+  Future.purify (fun s ->
+    if Stateid.equal at Stateid.dummy then finish ()
+    else Reach.known_state ~cache:`Yes at;
+    let newtip, route = report_with in
+    let _, ast as loc_ast = vernac_parse ~newtip ~route 0 s in
+    let clas = classify_vernac ast in
+    match clas with
+    | VtStm (w,_), _ ->
+       ignore(process_transaction
+         ~tty:false true (VtStm (w,false), VtNow) loc_ast)
+    | _ ->
+       ignore(process_transaction
+         ~tty:false true (VtQuery (false,report_with), VtNow) loc_ast))
+  s
+
+let edit_at id =
+  if Stateid.equal id Stateid.dummy then anomaly(str"edit_at dummy") else
+  let vcs = VCS.backup () in
+  let on_cur_branch id =
+    let rec aux cur =
+      if id = cur then true
+      else match VCS.visit cur with
+      | { step = `Fork _ } -> false
+      | { next } -> aux next in
+    aux (VCS.get_branch_pos (VCS.current_branch ())) in
+  let is_ancestor_of_cur_branch id =
+    Vcs_.NodeSet.mem id
+      (VCS.reachable (VCS.get_branch_pos (VCS.current_branch ()))) in
+  let has_failed qed_id =
+    match VCS.visit qed_id with
+    | { step = `Qed ({ fproof = Some (fp,_) }, _) } -> Future.is_exn fp
+    | _ -> false in
+  let rec master_for_br root tip =
+      if Stateid.equal tip Stateid.initial then tip else
+      match VCS.visit tip with
+      | { next } when next = root -> root
+      | { step = `Fork _ } -> tip
+      | { step = `Sideff (`Ast(_,id)|`Id id) } -> id
+      | { next } -> master_for_br root next in
+  let reopen_branch start at_id mode qed_id tip =
+    let master_id, cancel_switch =
+      (* Hum, this should be the real start_id in the clusted and not next *)
+      match VCS.visit qed_id with
+      | { step = `Qed ({ fproof = Some (_,cs)},_) } -> start, cs
+      | _ -> anomaly (str "Cluster not ending with Qed") in
+    VCS.branch ~root:master_id ~pos:id
+      VCS.edit_branch (`Edit (mode, qed_id, master_id));
+    VCS.delete_cluster_of id;
+    cancel_switch := true;
+    Reach.known_state ~cache:(interactive ()) id;
+    VCS.checkout_shallowest_proof_branch ();
+    `Focus { stop = qed_id; start = master_id; tip } in
+  let backto id =
+    List.iter VCS.delete_branch (VCS.branches ());
+    let ancestors = VCS.reachable id in
+    let { mine = brname, brinfo; others } = Backtrack.branches_of id in
+    List.iter (fun (name,{ VCS.kind = k; root; pos }) ->
+      if not(VCS.Branch.equal name VCS.Branch.master) &&
+         Vcs_.NodeSet.mem root ancestors then
+        VCS.branch ~root ~pos name k)
+      others;
+    VCS.reset_branch VCS.Branch.master (master_for_br brinfo.VCS.root id);
+    VCS.branch ~root:brinfo.VCS.root ~pos:brinfo.VCS.pos brname brinfo.VCS.kind;
+    VCS.delete_cluster_of id;
+    VCS.gc ();
+    Reach.known_state ~cache:(interactive ()) id;
+    VCS.checkout_shallowest_proof_branch ();
+    `NewTip in
+  try
+    let rc =
+      let focused = List.exists ((=) VCS.edit_branch) (VCS.branches ()) in
+      let branch_info =
+        match snd (VCS.get_info id).vcs_backup with
+        | Some{ mine = _, { VCS.kind = (`Proof(m,_)|`Edit(m,_,_)) }} -> Some m
+        | _ -> None in
+      match focused, VCS.cluster_of id, branch_info with
+      | _, Some _, None -> assert false
+      | false, Some (qed_id,start), Some mode ->
+          let tip = VCS.cur_tip () in
+          if has_failed qed_id && not !Flags.async_proofs_never_reopen_branch
+          then reopen_branch start id mode qed_id tip
+          else backto id
+      | true, Some (qed_id,_), Some mode ->
+          if on_cur_branch id then begin
+            assert false
+          end else if is_ancestor_of_cur_branch id then begin
+            backto id
+          end else begin
+            anomaly(str"Cannot leave an `Edit branch open")
+          end
+      | true, None, _ ->
+          if on_cur_branch id then begin
+            VCS.reset_branch (VCS.current_branch ()) id;
+            Reach.known_state ~cache:(interactive ()) id;
+            VCS.checkout_shallowest_proof_branch ();
+            `NewTip
+          end else if is_ancestor_of_cur_branch id then begin
+            backto id
+          end else begin
+            anomaly(str"Cannot leave an `Edit branch open")
+          end
+      | false, None, _ -> backto id
+    in
+    VCS.print ();
+    rc
+  with e ->
+    let (e, info) = Errors.push e in
+    match Stateid.get info with
+    | None ->
+        VCS.print ();
+        anomaly (str ("edit_at "^Stateid.to_string id^": ") ++
+          Errors.print_no_report e)
+    | Some (_, id) ->
+        prerr_endline ("Failed at state " ^ Stateid.to_string id);
+        VCS.restore vcs;
+        VCS.print ();
+        iraise (e, info)
+
+(*********************** TTY API (PG, coqtop, coqc) ***************************)
+(******************************************************************************)
+
+let interp verb (_,e as lexpr) =
+  let clas = classify_vernac e in
+  let rc = process_transaction ~tty:true verb clas lexpr in
+  if rc <> `Ok then anomaly(str"tty loop can't be mixed with the STM protocol");
+  if interactive () = `Yes ||
+     (!Flags.async_proofs_mode = Flags.APoff &&
+      !Flags.compilation_mode = Flags.BuildVo) then
+    let vcs = VCS.backup () in
+    let print_goals =
+      verb && match clas with
+       | VtQuery _, _ -> false
+       | (VtProofStep _ | VtStm (VtBack _, _)), _ -> true
+       | _ -> not !Flags.coqtop_ui || !Flags.print_emacs in
+    try finish ~print_goals ()
+    with e ->
+      let e = Errors.push e in
+      handle_failure e vcs true
+
+let finish () = finish ()
+
+let get_current_state () = VCS.cur_tip ()
+
+let current_proof_depth () =
+  let head = VCS.current_branch () in
+  match VCS.get_branch head with
+  | { VCS.kind = `Master } -> 0
+  | { VCS.pos = cur; VCS.kind = (`Proof _ | `Edit _); VCS.root = root } ->
+      let rec distance root =
+        if Stateid.equal cur root then 0
+        else 1 + distance (VCS.visit cur).next in
+      distance cur
+
+let unmangle n =
+  let n = VCS.Branch.to_string n in
+  let idx = String.index n '_' + 1 in
+  Names.id_of_string (String.sub n idx (String.length n - idx))
+
+let proofname b = match VCS.get_branch b with
+  | { VCS.kind = (`Proof _| `Edit _) } -> Some b
+  | _ -> None
+
+let get_all_proof_names () =
+  List.map unmangle (List.map_filter proofname (VCS.branches ()))
+
+let get_current_proof_name () =
+  Option.map unmangle (proofname (VCS.current_branch ()))
+
+let get_script prf =
+  let branch, test =
+    match prf with
+    | None -> VCS.Branch.master, fun _ -> true
+    | Some name -> VCS.current_branch (),  List.mem name in
+  let rec find acc id =
+    if Stateid.equal id Stateid.initial ||
+       Stateid.equal id Stateid.dummy then acc else
+    let view = VCS.visit id in
+    match view.step with
+    | `Fork((_,_,_,ns), _) when test ns -> acc
+    | `Qed (qed, proof) -> find [qed.qast.expr, (VCS.get_info id).n_goals] proof
+    | `Sideff (`Ast (x,_)) ->
+         find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next
+    | `Sideff (`Id id)  -> find acc id
+    | `Cmd {cast = x} -> find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next 
+    | `Alias id -> find acc id
+    | `Fork _ -> find acc view.next
+    in
+  find [] (VCS.get_branch_pos branch)
+
+(* indentation code for Show Script, initially contributed
+   by D. de Rauglaudre *)
+
+let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) =
+  (* ng1 : number of goals remaining at the current level (before cmd)
+     ngl1 : stack of previous levels with their remaining goals
+     ng : number of goals after the execution of cmd
+     beginend : special indentation stack for { } *)
+  let ngprev = List.fold_left (+) ng1 ngl1 in
+  let new_ngl =
+    if ng > ngprev then
+      (* We've branched *)
+      (ng - ngprev + 1, ng1 - 1 :: ngl1)
+    else if ng < ngprev then
+      (* A subgoal have been solved. Let's compute the new current level
+	 by discarding all levels with 0 remaining goals. *)
+      let rec loop = function
+	| (0, ng2::ngl2) -> loop (ng2,ngl2)
+	| p -> p
+      in loop (ng1-1, ngl1)
+    else
+      (* Standard case, same goal number as before *)
+      (ng1, ngl1)
+  in
+  (* When a subgoal have been solved, separate this block by an empty line *)
+  let new_nl = (ng < ngprev)
+  in
+  (* Indentation depth *)
+  let ind = List.length ngl1
+  in
+  (* Some special handling of bullets and { }, to get a nicer display *)
+  let pred n = max 0 (n-1) in
+  let ind, nl, new_beginend = match cmd with
+    | VernacSubproof _ -> pred ind, nl, (pred ind)::beginend
+    | VernacEndSubproof -> List.hd beginend, false, List.tl beginend
+    | VernacBullet _ -> pred ind, nl, beginend
+    | _ -> ind, nl, beginend
+  in
+  let pp =
+    (if nl then fnl () else mt ()) ++
+    (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd))
+  in
+  (new_ngl, new_nl, new_beginend, pp :: ppl)
+
+let show_script ?proof () =
+  try
+    let prf =
+      try match proof with
+      | None -> Some (Pfedit.get_current_proof_name ())
+      | Some (p,_) -> Some (p.Proof_global.id)
+      with Proof_global.NoCurrentProof -> None
+    in
+    let cmds = get_script prf in
+    let _,_,_,indented_cmds =
+      List.fold_left indent_script_item ((1,[]),false,[],[]) cmds
+    in
+    let indented_cmds = List.rev (indented_cmds) in
+    msg_notice (v 0 (prlist_with_sep fnl (fun x -> x) indented_cmds))
+  with Vcs_aux.Expired -> ()
+
+(* Export hooks *)
+let state_computed_hook = Hooks.state_computed_hook
+let state_ready_hook = Hooks.state_ready_hook
+let parse_error_hook = Hooks.parse_error_hook
+let execution_error_hook = Hooks.execution_error_hook
+let forward_feedback_hook = Hooks.forward_feedback_hook
+let process_error_hook = Hooks.process_error_hook
+let interp_hook = Hooks.interp_hook
+let with_fail_hook = Hooks.with_fail_hook
+let unreachable_state_hook = Hooks.unreachable_state_hook
+
+(* vim:set foldmethod=marker: *)
diff --git a/stm/stm.mli b/stm/stm.mli
new file mode 100644
index 00000000..1d926e99
--- /dev/null
+++ b/stm/stm.mli
@@ -0,0 +1,132 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Vernacexpr
+open Names
+open Feedback
+
+(** state-transaction-machine interface *)
+
+(* [add ontop check vebose eid s] adds a new command [s] on the state [ontop]
+   having edit id [eid].  [check] is called on the AST.
+   The [ontop] parameter is just for asserting the GUI is on sync, but
+   will eventually call edit_at on the fly if needed.
+   The sentence [s] is parsed in the state [ontop].
+   If [newtip] is provided, then the returned state id is guaranteed to be
+   [newtip] *)
+val add : ontop:Stateid.t -> ?newtip:Stateid.t -> ?check:(located_vernac_expr -> unit) ->
+  bool -> edit_id -> string ->
+    Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
+
+(* parses and executes a command at a given state, throws away its side effects
+   but for the printings.  Feedback is sent with report_with (defaults to dummy
+   state id)  *)
+val query :
+  at:Stateid.t -> ?report_with:(Stateid.t * Feedback.route_id) -> string -> unit
+
+(* [edit_at id] is issued to change the editing zone.  [`NewTip] is returned if
+   the requested id is the new document tip hence the document portion following
+   [id] is dropped by Coq.  [`Focus fo] is returned to say that [fo.tip] is the
+   new document tip, the document between [id] and [fo.stop] has been dropped.
+   The portion between [fo.stop] and [fo.tip] has been kept.  [fo.start] is
+   just to tell the gui where the editing zone starts, in case it wants to
+   graphically denote it.  All subsequent [add] happen on top of [id]. *)
+type focus = { start : Stateid.t; stop : Stateid.t; tip : Stateid.t }
+val edit_at : Stateid.t -> [ `NewTip | `Focus of focus ]
+
+(* Evaluates the tip of the current branch *)
+val finish : unit -> unit
+
+val observe : Stateid.t -> unit
+
+val stop_worker : string -> unit
+
+(* Joins the entire document.  Implies finish, but also checks proofs *)
+val join : unit -> unit
+
+(* Saves on the dist a .vio corresponding to the current status:
+   - if the worker prool is empty, all tasks are saved
+   - if the worker proof is not empty, then it waits until all workers
+     are done with their current jobs and then dumps (or fails if one
+     of the completed tasks is a failuere) *)
+val snapshot_vio : DirPath.t -> string -> unit
+
+(* Empties the task queue, can be used only if the worker pool is empty (E.g.
+ * after having built a .vio in batch mode *)
+val reset_task_queue : unit -> unit
+
+(* A .vio contains tasks to be completed *)
+type tasks
+val check_task : string -> tasks -> int -> bool
+val info_tasks : tasks -> (string * float * int) list
+val finish_tasks : string ->
+  Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs ->
+    tasks -> Library.seg_univ * Library.seg_proofs
+
+(* Id of the tip of the current branch *)
+val get_current_state : unit -> Stateid.t
+
+(* Misc *)
+val init : unit -> unit
+val print_ast : Stateid.t -> Xml_datatype.xml
+
+(* Filename *)
+val set_compilation_hints : string -> unit
+
+(* Reorders the task queue putting forward what is in the perspective *)
+val set_perspective : Stateid.t list -> unit
+
+(** workers **************************************************************** **)
+
+module ProofTask : AsyncTaskQueue.Task
+module TacTask   : AsyncTaskQueue.Task
+module QueryTask : AsyncTaskQueue.Task
+
+(** customization ********************************************************** **)
+
+(* From the master (or worker, but beware that to install the hook
+ * into a worker one has to build the worker toploop to do so and
+ * the alternative toploop for the worker can be selected by changing
+ * the name of the Task(s) above) *)
+
+val state_computed_hook : (Stateid.t -> in_cache:bool -> unit) Hook.t
+val parse_error_hook :
+  (Feedback.edit_or_state_id -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t
+val execution_error_hook : (Stateid.t -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t
+val unreachable_state_hook : (Stateid.t -> unit) Hook.t
+(* ready means that master has it at hand *)
+val state_ready_hook : (Stateid.t -> unit) Hook.t
+
+(* Messages from the workers to the master *)
+val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t
+
+type state = {
+  system : States.state;
+  proof : Proof_global.state;
+  shallow : bool
+}
+val state_of_id : Stateid.t -> [ `Valid of state option | `Expired ]
+
+(** read-eval-print loop compatible interface ****************************** **)
+
+(* Adds a new line to the document.  It replaces the core of Vernac.interp.
+   [finish] is called as the last bit of this function is the system
+   is running interactively (-emacs or coqtop). *)
+val interp : bool -> located_vernac_expr -> unit
+
+(* Queries for backward compatibility *)
+val current_proof_depth : unit -> int
+val get_all_proof_names : unit -> Id.t list
+val get_current_proof_name : unit -> Id.t option
+val show_script : ?proof:Proof_global.closed_proof -> unit -> unit
+
+(** Reverse dependency hooks *)
+val process_error_hook : Future.fix_exn Hook.t
+val interp_hook : (?verbosely:bool -> ?proof:Proof_global.closed_proof ->
+  Loc.t * Vernacexpr.vernac_expr -> unit) Hook.t
+val with_fail_hook : (bool -> (unit -> unit) -> unit) Hook.t
diff --git a/stm/stm.mllib b/stm/stm.mllib
new file mode 100644
index 00000000..92b3a869
--- /dev/null
+++ b/stm/stm.mllib
@@ -0,0 +1,12 @@
+Spawned
+Dag
+Vcs
+TQueue
+WorkerPool
+Vernac_classifier
+Lemmas
+CoqworkmgrApi
+AsyncTaskQueue
+Texmacspp
+Stm
+Vio_checking
diff --git a/stm/tQueue.ml b/stm/tQueue.ml
new file mode 100644
index 00000000..8a62fe79
--- /dev/null
+++ b/stm/tQueue.ml
@@ -0,0 +1,133 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+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
+end = struct
+  type 'a item = int * 'a
+  type 'a rel = 'a item -> 'a item -> int
+  type 'a t = ('a item list * 'a rel) ref
+  let sort_timestamp (i,_) (j,_) = i - j
+  let age = ref 0
+  let create () = ref ([],sort_timestamp)
+  let is_empty t = fst !t = []
+  let exists p t = List.exists (fun (_,x) -> p x) (fst !t)
+  let pop ?(picky=(fun _ -> true)) ({ contents = (l, rel) } as t) =
+    let rec aux acc = function
+      | [] -> raise Queue.Empty
+      | (_,x) :: xs when picky x -> t := (List.rev acc @ xs, rel); x
+      | (_,x) as hd :: xs -> aux (hd :: acc) xs in
+    aux [] l
+  let push ({ contents = (xs, rel) } as t) x =
+    incr age;
+    (* re-roting the whole list is not the most efficient way... *)
+    t := (List.sort rel (xs @ [!age,x]), rel)
+  let clear ({ contents = (l, rel) } as t) = t := ([], rel)
+  let set_rel rel ({ contents = (xs, _) } as t) =
+    let rel (_,x) (_,y) = rel x y in
+    t := (List.sort rel xs, rel)
+end
+
+type 'a t = {
+  queue: 'a PriorityQueue.t;
+  lock : Mutex.t;
+  cond : Condition.t;
+  mutable nwaiting : int;
+  cond_waiting : Condition.t;
+  mutable release : bool;
+}
+
+exception BeingDestroyed
+
+let create () = {
+  queue = PriorityQueue.create ();
+  lock = Mutex.create ();
+  cond = Condition.create ();
+  nwaiting = 0;
+  cond_waiting = Condition.create ();
+  release = false;
+}
+
+let pop ?(picky=(fun _ -> true)) ?(destroy=ref false)
+  ({ queue = q; lock = m; cond = c; cond_waiting = cn } as tq)
+=
+  Mutex.lock m;
+  if tq.release then (Mutex.unlock m; raise BeingDestroyed);
+  while not (PriorityQueue.exists picky q || !destroy) do
+    tq.nwaiting <- tq.nwaiting + 1;
+    Condition.broadcast cn;
+    Condition.wait c m;
+    tq.nwaiting <- tq.nwaiting - 1;
+    if tq.release || !destroy then (Mutex.unlock m; raise BeingDestroyed)
+  done;
+  if !destroy then (Mutex.unlock m; raise BeingDestroyed);
+  let x = PriorityQueue.pop ~picky q in
+  Condition.signal c;
+  Condition.signal cn;
+  Mutex.unlock m;
+  x
+
+let signal_destruction { lock = m; cond = c } =
+  Mutex.lock m;
+  Condition.broadcast c;
+  Mutex.unlock m
+
+let push { queue = q; lock = m; cond = c; release } x =
+  if release then Errors.anomaly(Pp.str
+    "TQueue.push while being destroyed! Only 1 producer/destroyer allowed");
+  Mutex.lock m;
+  PriorityQueue.push q x;
+  Condition.broadcast c;
+  Mutex.unlock m
+
+let clear { queue = q; lock = m; cond = c } =
+  Mutex.lock m;
+  PriorityQueue.clear q;
+  Mutex.unlock m
+
+let is_empty { queue = q } = PriorityQueue.is_empty q
+
+let destroy tq =
+  tq.release <- true;
+  while tq.nwaiting > 0 do
+    Mutex.lock tq.lock;
+    Condition.broadcast tq.cond;
+    Mutex.unlock tq.lock;
+  done;
+  tq.release <- false
+
+let wait_until_n_are_waiting_and_queue_empty j tq =
+  Mutex.lock tq.lock;
+  while not (PriorityQueue.is_empty tq.queue) || tq.nwaiting < j do
+    Condition.wait tq.cond_waiting tq.lock
+  done;
+  Mutex.unlock tq.lock
+
+let wait_until_n_are_waiting_then_snapshot j tq =
+  let l = ref [] in
+  Mutex.lock tq.lock;
+  while not (PriorityQueue.is_empty tq.queue) do
+    l := PriorityQueue.pop tq.queue :: !l
+  done;
+  while tq.nwaiting < j do Condition.wait tq.cond_waiting tq.lock done;
+  List.iter (PriorityQueue.push tq.queue) (List.rev !l);
+  if !l <> [] then Condition.broadcast tq.cond;
+  Mutex.unlock tq.lock;
+  List.rev !l
+
+let set_order tq rel =
+  Mutex.lock tq.lock;
+  PriorityQueue.set_rel rel tq.queue;
+  Mutex.unlock tq.lock
diff --git a/stm/tQueue.mli b/stm/tQueue.mli
new file mode 100644
index 00000000..bc3922b3
--- /dev/null
+++ b/stm/tQueue.mli
@@ -0,0 +1,28 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* 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
+val signal_destruction : 'a t -> unit
+
+(* Non destructive *)
+val wait_until_n_are_waiting_then_snapshot : int -> 'a t -> 'a list
+
+val clear : 'a t -> unit
+val is_empty : 'a t -> bool
+
+exception BeingDestroyed
+(* Threads blocked in pop can get this exception if the queue is being
+ * destroyed *)
+val destroy : 'a t -> unit
diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml
new file mode 100644
index 00000000..c1a37fed
--- /dev/null
+++ b/stm/tacworkertop.ml
@@ -0,0 +1,18 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+module W = AsyncTaskQueue.MakeWorker(Stm.TacTask)
+
+let () = Coqtop.toploop_init := (fun args ->
+        Flags.make_silent true;
+        W.init_stdout ();
+        CoqworkmgrApi.init !Flags.async_proofs_worker_priority;
+        args)
+
+let () = Coqtop.toploop_run := W.main_loop
+
diff --git a/stm/tacworkertop.mllib b/stm/tacworkertop.mllib
new file mode 100644
index 00000000..db38fde2
--- /dev/null
+++ b/stm/tacworkertop.mllib
@@ -0,0 +1 @@
+Tacworkertop
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
new file mode 100644
index 00000000..d71c169d
--- /dev/null
+++ b/stm/texmacspp.ml
@@ -0,0 +1,763 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Xml_datatype
+open Vernacexpr
+open Constrexpr
+open Names
+open Misctypes
+open Bigint
+open Decl_kinds
+open Extend
+open Libnames
+open Flags
+
+let unlock loc =
+  let start, stop = Loc.unloc loc in
+  (string_of_int start, string_of_int stop)
+
+let xmlNoop = (* almost noop  *)
+  PCData ""
+
+let xmlWithLoc loc ename attr xml =
+  let start, stop = unlock loc in
+  Element(ename, [ "begin", start; "end", stop ] @ attr, xml)
+
+let get_fst_attr_in_xml_list attr xml_list =
+  let attrs_list =
+    List.map (function
+      | Element (_, attrs, _) -> (List.filter (fun (a,_) -> a = attr) attrs)
+      | _ -> [])
+    xml_list in
+  match List.flatten attrs_list with
+  | [] -> (attr, "")
+  | l  -> (List.hd l)
+
+let backstep_loc xmllist =
+  let start_att = get_fst_attr_in_xml_list "begin" xmllist in
+  let stop_att =  get_fst_attr_in_xml_list "end" (List.rev xmllist) in
+  [start_att ; stop_att]
+
+let compare_begin_att xml1 xml2 =
+  let att1 = get_fst_attr_in_xml_list "begin" [xml1] in
+  let att2 = get_fst_attr_in_xml_list "begin" [xml2] in
+  match att1, att2 with
+  | (_, s1), (_, s2) when s1 == "" || s2 == "" -> 0
+  | (_, s1), (_, s2) when int_of_string s1 > int_of_string s2 -> 1
+  | (_, s1), (_, s2) when int_of_string s1 < int_of_string s2 -> -1
+  | _ -> 0
+
+let xmlBeginSection loc name = xmlWithLoc loc "beginsection" ["name", name] []
+
+let xmlEndSegment loc name = xmlWithLoc loc "endsegment" ["name", name] []
+
+let xmlThm typ name loc xml =
+  xmlWithLoc loc "theorem" ["type", typ; "name", name] xml
+
+let xmlDef typ name loc xml =
+  xmlWithLoc loc "definition" ["type", typ; "name", name] xml
+
+let xmlNotation attr name loc xml =
+  xmlWithLoc loc "notation" (("name", name) :: attr) xml
+
+let xmlReservedNotation attr name loc =
+  xmlWithLoc loc "reservednotation" (("name", name) :: attr) []
+
+let xmlCst name ?(attr=[]) loc =
+  xmlWithLoc loc "constant" (("name", name) :: attr) []
+
+let xmlOperator name ?(attr=[]) ?(pprules=[]) loc =
+  xmlWithLoc loc "operator"
+    (("name", name) :: List.map (fun (a,b) -> "format"^a,b) pprules @ attr) []
+
+let xmlApply loc ?(attr=[]) xml = xmlWithLoc loc "apply" attr xml
+
+let xmlToken loc ?(attr=[]) xml = xmlWithLoc loc "token" attr xml
+
+let xmlTyped xml = Element("typed", (backstep_loc xml), xml)
+
+let xmlReturn ?(attr=[]) xml = Element("return", attr, xml)
+
+let xmlCase xml = Element("case", [], xml)
+
+let xmlScrutinee ?(attr=[]) xml = Element("scrutinee", attr, xml)
+
+let xmlWith xml = Element("with", [], xml)
+
+let xmlAssign id xml = Element("assign", ["target",string_of_id id], [xml])
+
+let xmlInductive kind loc xml = xmlWithLoc loc "inductive" ["kind",kind] xml
+
+let xmlCoFixpoint xml = Element("cofixpoint", [], xml)
+
+let xmlFixpoint xml = Element("fixpoint", [], xml)
+
+let xmlCheck loc xml = xmlWithLoc loc "check" [] xml
+
+let xmlAssumption kind loc xml = xmlWithLoc loc "assumption" ["kind",kind] xml
+
+let xmlComment loc xml = xmlWithLoc loc "comment" [] xml
+
+let xmlCanonicalStructure attr loc = xmlWithLoc loc "canonicalstructure" attr []
+
+let xmlQed ?(attr=[]) loc = xmlWithLoc loc "qed" attr []
+
+let xmlPatvar id loc = xmlWithLoc loc "patvar" ["id", id] []
+
+let xmlReference ref =
+  let name = Libnames.string_of_reference ref in
+  let i, j = Loc.unloc (Libnames.loc_of_reference ref) in
+  let b, e = string_of_int i, string_of_int j in
+  Element("reference",["name", name; "begin", b; "end", e] ,[])
+
+let xmlRequire loc ?(attr=[]) xml = xmlWithLoc loc "require" attr xml
+let xmlImport loc ?(attr=[]) xml = xmlWithLoc loc "import" attr xml
+
+let xmlAddLoaPath loc ?(attr=[]) xml = xmlWithLoc loc "addloadpath" attr xml
+let xmlRemoveLoaPath loc ?(attr=[]) = xmlWithLoc loc "removeloadpath" attr
+let xmlAddMLPath loc ?(attr=[]) = xmlWithLoc loc "addmlpath" attr
+
+let xmlExtend loc xml = xmlWithLoc loc "extend" [] xml
+
+let xmlScope loc action ?(attr=[]) name xml =
+  xmlWithLoc loc "scope" (["name",name;"action",action] @ attr) xml
+
+let xmlProofMode loc name = xmlWithLoc loc "proofmode" ["name",name] []
+
+let xmlProof loc xml = xmlWithLoc loc "proof" [] xml
+
+let xmlRawTactic name rtac =
+  Element("rawtactic", ["name",name],
+    [PCData (Pp.string_of_ppcmds (Pptactic.pr_raw_tactic rtac))])
+
+let xmlSectionSubsetDescr name ssd =
+  Element("sectionsubsetdescr",["name",name],
+    [PCData (Proof_using.to_string ssd)])
+
+let xmlDeclareMLModule loc s =
+  xmlWithLoc loc "declarexmlmodule" []
+    (List.map (fun x -> Element("path",["value",x],[])) s)
+
+(* tactics *)
+let xmlLtac loc xml = xmlWithLoc loc "ltac" [] xml
+
+(* toplevel commands *)
+let xmlGallina loc xml = xmlWithLoc loc "gallina" [] xml
+
+let xmlTODO loc x =
+  xmlWithLoc loc "todo" [] [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
+
+let string_of_name n =
+  match n with
+  | Anonymous -> "_"
+  | Name id -> Id.to_string id
+
+let string_of_glob_sort s =
+  match s with
+  | GProp -> "Prop"
+  | GSet -> "Set"
+  | GType _ -> "Type"
+
+let string_of_cast_sort c =
+  match c with
+  | CastConv _ -> "CastConv"
+  | CastVM _ -> "CastVM"
+  | CastNative _ -> "CastNative"
+  | CastCoerce -> "CastCoerce"
+
+let string_of_case_style s =
+  match s with
+  | LetStyle -> "Let"
+  | IfStyle -> "If"
+  | LetPatternStyle -> "LetPattern"
+  | MatchStyle -> "Match"
+  | RegularStyle -> "Regular"
+
+let attribute_of_syntax_modifier sm =
+match sm with
+  | SetItemLevel (sl, NumLevel n) ->
+      List.map (fun s -> ("itemlevel", s)) sl @ ["level", string_of_int n]
+  | SetItemLevel (sl, NextLevel) ->
+      List.map (fun s -> ("itemlevel", s)) sl @ ["level", "next"]
+  | SetLevel i -> ["level", string_of_int i]
+  | SetAssoc a ->
+      begin match a with
+      | NonA -> ["",""]
+      | RightA -> ["associativity", "right"]
+      | LeftA -> ["associativity", "left"]
+      end
+  | SetEntryType (s, _) -> ["entrytype", s]
+  | SetOnlyParsing v -> ["compat", Flags.pr_version v]
+  | SetFormat (system, (loc, s)) ->
+      let start, stop = unlock loc in
+      ["format-"^system, s; "begin", start; "end", stop]
+
+let string_of_assumption_kind l a many =
+  match l, a, many with
+  | (Discharge, Logical,      true)  -> "Hypotheses"
+  | (Discharge, Logical,      false) -> "Hypothesis"
+  | (Discharge, Definitional, true)  -> "Variables"
+  | (Discharge, Definitional, false) -> "Variable"
+  | (Global,    Logical,      true)  -> "Axioms"
+  | (Global,    Logical,      false) -> "Axiom"
+  | (Global,    Definitional, true)  -> "Parameters"
+  | (Global,    Definitional, false) -> "Parameter"
+  | (Local,     Logical,      true)  -> "Local Axioms"
+  | (Local,     Logical,      false) -> "Local Axiom"
+  | (Local,     Definitional, true)  -> "Local Parameters"
+  | (Local,     Definitional, false) -> "Local Parameter"
+  | (Global,    Conjectural, _)      -> "Conjecture"
+  | ((Discharge | Local), Conjectural, _) -> assert false
+
+let rec pp_bindlist bl =
+  let tlist =
+    List.flatten
+        (List.map
+          (fun (loc_names, _, e) ->
+            let names =
+              (List.map
+                (fun (loc, name) ->
+                  xmlCst (string_of_name name) loc) loc_names) in
+            match e with
+              | CHole _ -> names
+              | _ -> names @ [pp_expr e])
+          bl) in
+  match tlist with
+    | [e] -> e
+    | l -> xmlTyped l
+and pp_decl_notation ((_, s), ce, sc) = (* don't know what it is for now *)
+  Element ("decl_notation", ["name", s], [pp_expr ce])
+and pp_local_binder lb = (* don't know what it is for now *)
+  match lb with
+  | LocalRawDef ((_, nam), ce) ->
+      let attrs = ["name", string_of_name nam] in
+      pp_expr ~attr:attrs ce
+  | LocalRawAssum (namll, _, ce) ->
+      let ppl =
+        List.map (fun (loc, nam) -> (xmlCst (string_of_name nam) loc)) namll in
+      xmlTyped (ppl @ [pp_expr ce])
+and pp_local_decl_expr lde = (* don't know what it is for now *)
+  match lde with
+  | AssumExpr (_, ce) -> pp_expr ce
+  | DefExpr (_, ce, _) -> pp_expr ce
+and pp_inductive_expr ((_, (l, id)), lbl, ceo, _, cl_or_rdexpr) =
+  (* inductive_expr *)
+  let b,e = Loc.unloc l in
+  let location = ["begin", string_of_int b; "end", string_of_int e] in
+  [Element ("lident", ["name", Id.to_string id] @ location, [])] @ (* inductive name *)
+  begin match cl_or_rdexpr with
+  | Constructors coel -> List.map (fun (_, (_, ce)) -> pp_expr ce) coel
+  | RecordDecl (_, ldewwwl) ->
+      List.map (fun (((_, x), _), _) -> pp_local_decl_expr x) ldewwwl
+  end @
+  begin match ceo with (* don't know what it is for now *)
+  | Some ce -> [pp_expr ce]
+  | None -> []
+  end @
+  (List.map pp_local_binder lbl)
+and pp_recursion_order_expr optid roe = (* don't know what it is for now *)
+  let attrs =
+    match optid with
+    | None -> []
+    | Some (loc, id) ->
+        let start, stop = unlock loc in
+        ["begin", start; "end", stop ; "name", Id.to_string id] in
+  let kind, expr =
+    match roe with
+    | CStructRec -> "struct", []
+    | CWfRec e -> "rec", [pp_expr e]
+    | CMeasureRec (e, None) -> "mesrec", [pp_expr e]
+    | CMeasureRec (e, Some rel) -> "mesrec", [pp_expr e] @ [pp_expr rel] in
+  Element ("recursion_order", ["kind", kind] @ attrs, expr)
+and pp_fixpoint_expr ((loc, id), (optid, roe), lbl, ce, ceo) =
+  (* fixpoint_expr *)
+  let start, stop = unlock loc in
+  let id = Id.to_string id in
+  [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @
+  (* fixpoint name *)
+  [pp_recursion_order_expr optid roe] @
+  (List.map pp_local_binder lbl) @
+  [pp_expr ce] @
+  begin match ceo with (* don't know what it is for now *)
+  | Some ce -> [pp_expr ce]
+  | None -> []
+  end
+and pp_cofixpoint_expr ((loc, id), lbl, ce, ceo) = (* cofixpoint_expr *)
+  (* Nota: it is like fixpoint_expr without (optid, roe)
+   * so could be merged if there is no more differences *)
+  let start, stop = unlock loc in
+  let id = Id.to_string id in
+  [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @
+  (* cofixpoint name *)
+  (List.map pp_local_binder lbl) @
+  [pp_expr ce] @
+  begin match ceo with (* don't know what it is for now *)
+  | Some ce -> [pp_expr ce]
+  | None -> []
+  end
+and pp_lident (loc, id) = xmlCst (Id.to_string id) loc
+and pp_simple_binder (idl, ce) = List.map pp_lident idl @ [pp_expr ce]
+and pp_cases_pattern_expr cpe =
+  match cpe with
+  | CPatAlias (loc, cpe, id) ->
+      xmlApply loc
+        (xmlOperator "alias" ~attr:["name", string_of_id id] loc ::
+          [pp_cases_pattern_expr cpe])
+  | CPatCstr (loc, ref, cpel1, cpel2) ->
+      xmlApply loc
+        (xmlOperator "reference"
+           ~attr:["name", Libnames.string_of_reference ref] loc ::
+         [Element ("impargs", [], (List.map pp_cases_pattern_expr cpel1));
+          Element ("args", [], (List.map pp_cases_pattern_expr cpel2))])
+  | CPatAtom (loc, optr) ->
+      let attrs = match optr with
+        | None -> []
+        | Some r -> ["name", Libnames.string_of_reference r] in
+      xmlApply loc (xmlOperator "atom" ~attr:attrs loc :: [])
+  | CPatOr (loc, cpel) ->
+      xmlApply loc (xmlOperator "or" loc :: List.map pp_cases_pattern_expr cpel)
+  | CPatNotation (loc, n, (subst_constr, subst_rec), cpel) ->
+      xmlApply loc
+        (xmlOperator "notation" loc ::
+          [xmlOperator n loc;
+           Element ("subst", [],
+             [Element ("subterms", [],
+                List.map pp_cases_pattern_expr subst_constr);
+              Element ("recsubterms", [],
+                List.map
+                  (fun (cpel) ->
+                     Element ("recsubterm", [],
+                       List.map pp_cases_pattern_expr cpel))
+                subst_rec)]);
+           Element ("args", [], (List.map pp_cases_pattern_expr cpel))])
+  | CPatPrim (loc, tok) -> pp_token loc tok
+  | CPatRecord (loc, rcl) ->
+      xmlApply loc
+        (xmlOperator "record" loc ::
+           List.map (fun (r, cpe) ->
+             Element ("field",
+               ["reference", Libnames.string_of_reference r],
+               [pp_cases_pattern_expr cpe]))
+           rcl)
+  | CPatDelimiters (loc, delim, cpe) ->
+      xmlApply loc
+        (xmlOperator "delimiter" ~attr:["name", delim] loc ::
+          [pp_cases_pattern_expr cpe])
+and pp_case_expr (e, (name, pat)) =
+  match name, pat with
+  | None, None -> xmlScrutinee [pp_expr e]
+  | Some (loc, name), None ->
+      let start, stop= unlock loc in
+      xmlScrutinee ~attr:["name", string_of_name name;
+                          "begin", start; "end", stop] [pp_expr e]
+  | Some (loc, name), Some p ->
+      let start, stop= unlock loc in
+      xmlScrutinee ~attr:["name", string_of_name name;
+                          "begin", start; "end", stop]
+        [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e]
+  | None, Some p ->
+      xmlScrutinee [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e]
+and pp_branch_expr_list bel =
+  xmlWith
+    (List.map
+      (fun (_, cpel, e) ->
+        let ppcepl =
+          List.map pp_cases_pattern_expr (List.flatten (List.map snd cpel)) in
+        let ppe = [pp_expr e] in
+        xmlCase (ppcepl @ ppe))
+     bel)
+and pp_token loc tok =
+  let tokstr =
+    match tok with
+    | String s -> PCData s
+    | Numeral n -> PCData (to_string n) in
+  xmlToken loc [tokstr]
+and pp_local_binder_list lbl =
+  let l = (List.map pp_local_binder lbl) in
+  Element ("recurse", (backstep_loc l), l)
+and pp_const_expr_list cel =
+  let l = List.map pp_expr cel in
+  Element ("recurse", (backstep_loc l), l)
+and pp_expr ?(attr=[]) e =
+  match e with
+  | CRef (r, _) ->
+      xmlCst ~attr
+        (Libnames.string_of_reference r) (Libnames.loc_of_reference r)
+  | CProdN (loc, bl, e) ->
+      xmlApply loc
+        (xmlOperator "forall" loc :: [pp_bindlist bl] @ [pp_expr e])
+  | CApp (loc, (_, hd), args) ->
+       xmlApply ~attr loc (pp_expr hd :: List.map (fun (e,_) -> pp_expr e) args)
+  | CAppExpl (loc, (_, r, _), args) ->
+       xmlApply ~attr loc
+         (xmlCst (Libnames.string_of_reference r)
+                 (Libnames.loc_of_reference r) :: List.map pp_expr args)
+  | CNotation (loc, notation,  ([],[],[])) ->
+       xmlOperator notation loc
+  | CNotation (loc, notation,  (args, cell, lbll)) ->
+      let fmts = Notation.find_notation_extra_printing_rules notation in
+      let oper = xmlOperator notation loc ~pprules:fmts in
+      let cels = List.map pp_const_expr_list cell in
+      let lbls = List.map pp_local_binder_list lbll in
+      let args = List.map pp_expr args in
+      xmlApply loc (oper :: (List.sort compare_begin_att (args @ cels @ lbls)))
+  | CSort(loc, s) ->
+      xmlOperator (string_of_glob_sort s) loc
+  | CDelimiters (loc, scope, ce) ->
+      xmlApply loc (xmlOperator "delimiter" ~attr:["name", scope] loc ::
+        [pp_expr ce])
+  | CPrim (loc, tok) -> pp_token loc tok
+  | CGeneralization (loc, kind, _, e) ->
+      let kind= match kind with
+      | Explicit -> "explicit"
+      | Implicit -> "implicit" in
+      xmlApply loc
+        (xmlOperator "generalization" ~attr:["kind", kind] loc :: [pp_expr e])
+  | CCast (loc, e, tc) ->
+      begin match tc with
+      | CastConv t | CastVM t |CastNative t ->
+          xmlApply loc
+            (xmlOperator ":" loc ~attr:["kind", (string_of_cast_sort tc)] ::
+             [pp_expr e; pp_expr t])
+      | CastCoerce   ->
+          xmlApply loc
+            (xmlOperator ":" loc ~attr:["kind", "CastCoerce"] ::
+             [pp_expr e])
+      end
+  | CEvar (loc, ek, cel) ->
+      let ppcel = List.map (fun (id,e) -> xmlAssign id (pp_expr e)) cel in
+      xmlApply loc
+        (xmlOperator "evar" loc ~attr:["id", string_of_id ek] ::
+          ppcel)
+  | CPatVar (loc, id) -> xmlPatvar (string_of_id id) loc
+  | CHole (loc, _, _, _) -> xmlCst ~attr  "_" loc
+  | CIf (loc, test, (_, ret), th, el) ->
+      let return = match ret with
+      | None -> []
+      | Some r -> [xmlReturn [pp_expr r]] in
+      xmlApply loc
+        (xmlOperator "if" loc ::
+          return @ [pp_expr th] @ [pp_expr el])
+  | CLetTuple (loc, names, (_, ret), value, body) ->
+      let return = match ret with
+      | None -> []
+      | Some r -> [xmlReturn [pp_expr r]] in
+      xmlApply loc
+        (xmlOperator "lettuple" loc ::
+          return @
+          (List.map (fun (loc, var) -> xmlCst (string_of_name var) loc) names) @
+          [pp_expr value; pp_expr body])
+  | CCases (loc, sty, ret, cel, bel) ->
+      let return = match ret with
+      | None -> []
+      | Some r -> [xmlReturn [pp_expr r]] in
+      xmlApply loc
+        (xmlOperator "match" loc  ~attr:["style", (string_of_case_style sty)] ::
+          (return @
+           [Element ("scrutinees", [], List.map pp_case_expr cel)] @
+           [pp_branch_expr_list bel]))
+  | CRecord (_, _, _) -> assert false
+  | CLetIn (loc, (varloc, var), value, body) ->
+      xmlApply loc
+        (xmlOperator "let" loc ::
+         [xmlCst (string_of_name var) varloc; pp_expr value; pp_expr body])
+  | CLambdaN (loc, bl, e) ->
+      xmlApply loc
+        (xmlOperator "lambda" loc :: [pp_bindlist bl] @ [pp_expr e])
+  | CCoFix (_, _, _) -> assert false
+  | CFix (loc, lid, fel) ->
+      xmlApply loc
+        (xmlOperator "fix" loc ::
+           List.flatten (List.map
+             (fun (a,b,cl,c,d) -> pp_fixpoint_expr (a,b,cl,c,Some d))
+             fel))
+
+let pp_comment (c) =
+  match c with
+  | CommentConstr e -> [pp_expr e]
+  | CommentString s -> [Element ("string", [], [PCData s])]
+  | CommentInt i -> [PCData (string_of_int i)]
+
+let rec tmpp v loc =
+  match v with
+  (* Control *)
+  | VernacLoad (verbose,f) ->
+      xmlWithLoc loc "load" ["verbose",string_of_bool verbose;"file",f] []
+  | VernacTime l ->
+      xmlApply loc (Element("time",[],[]) ::
+                    List.map (fun(loc,e) ->tmpp e loc) l)
+  | VernacTimeout (s,e) ->
+      xmlApply loc (Element("timeout",["val",string_of_int s],[]) ::
+                    [tmpp e loc])
+  | VernacFail e -> xmlApply loc (Element("fail",[],[]) :: [tmpp e loc])
+  | VernacError _ -> xmlWithLoc loc "error" [] []
+
+  (* Syntax *)
+  | VernacTacticNotation _ as x ->
+      xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
+
+  | VernacSyntaxExtension (_, ((_, name), sml)) ->
+      let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
+      xmlReservedNotation attrs name loc
+
+  | VernacOpenCloseScope (_,(true,name)) -> xmlScope loc "open" name []
+  | VernacOpenCloseScope (_,(false,name)) -> xmlScope loc "close" name []
+  | VernacDelimiters (name,tag) ->
+      xmlScope loc "delimit" name ~attr:["delimiter",tag] []
+  | VernacBindScope (name,l) ->
+      xmlScope loc "bind" name
+        (List.map (function
+          | ByNotation(loc,name,None) -> xmlNotation [] name loc []
+          | ByNotation(loc,name,Some d) ->
+              xmlNotation ["delimiter",d] name loc []
+          | AN ref -> xmlReference ref) l)
+  | VernacInfix (_,((_,name),sml),ce,sn) ->
+      let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
+      let sc_attr =
+        match sn with
+        | Some scope -> ["scope", scope]
+        | None -> [] in
+      xmlNotation (sc_attr @ attrs) name loc [pp_expr ce]
+  | VernacNotation (_, ce, (lstr, sml), sn) ->
+      let name = snd lstr in
+      let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
+      let sc_attr =
+        match sn with
+        | Some scope -> ["scope", scope]
+        | None -> [] in
+      xmlNotation (sc_attr @ attrs) name loc [pp_expr ce]
+  | VernacNotationAddFormat _ as x -> xmlTODO loc x
+  | VernacUniverse _
+  | VernacConstraint _
+  | VernacPolymorphic (_, _) as x -> xmlTODO loc x
+  (* Gallina *)
+  | VernacDefinition (ldk, (_,id), de) ->
+      let l, dk =
+        match ldk with
+        | Some l, dk -> (l, dk)
+        | None, dk -> (Global, dk) in (* Like in ppvernac.ml, l 585 *)
+      let e =
+        match de with
+        | ProveBody (_, ce) -> ce
+        | DefineBody (_, Some _, ce, None) -> ce
+        | DefineBody (_, None  , ce, None) -> ce
+        | DefineBody (_, Some _, ce, Some _) -> ce
+        | DefineBody (_, None  , ce, Some _) -> ce in
+      let str_dk = Kindops.string_of_definition_kind (l, false, dk) in
+      let str_id = Id.to_string id in
+      (xmlDef str_dk str_id loc [pp_expr e])
+  | VernacStartTheoremProof (tk, [ Some (_,id), ([], statement, None) ], b) ->
+      let str_tk = Kindops.string_of_theorem_kind tk in
+      let str_id = Id.to_string id in
+      (xmlThm str_tk str_id loc [pp_expr statement])
+  | VernacStartTheoremProof _ as x -> xmlTODO loc x
+  | VernacEndProof pe ->
+      begin
+        match pe with
+        | Admitted -> xmlQed loc
+        | Proved (_, Some ((_, id), Some tk)) ->
+            let nam = Id.to_string id in
+            let typ = Kindops.string_of_theorem_kind tk in
+            xmlQed ~attr:["name", nam; "type", typ] loc
+        | Proved (_, Some ((_, id), None)) ->
+            let nam = Id.to_string id in
+            xmlQed ~attr:["name", nam] loc
+        | Proved _ -> xmlQed loc
+      end
+  | VernacExactProof _ as x -> xmlTODO loc x
+  | VernacAssumption ((l, a), _, sbwcl) ->
+      let many =
+        List.length (List.flatten (List.map fst (List.map snd sbwcl))) > 1 in
+      let exprs =
+        List.flatten (List.map pp_simple_binder (List.map snd sbwcl)) in
+      let l = match l with Some x -> x | None -> Decl_kinds.Global in
+      let kind = string_of_assumption_kind l a many in
+      xmlAssumption kind loc exprs
+  | VernacInductive (_, _, iednll) ->
+      let kind =
+        let (_, _, _, k, _),_ = List.hd iednll in
+	  begin
+            match k with
+            | Record -> "Record"
+            | Structure -> "Structure"
+            | Inductive_kw -> "Inductive"
+            | CoInductive -> "CoInductive"
+            | Class _ -> "Class"
+            | Variant -> "Variant"
+          end in
+      let exprs =
+        List.flatten (* should probably not be flattened *)
+          (List.map
+            (fun (ie, dnl) -> (pp_inductive_expr ie) @
+                              (List.map pp_decl_notation dnl)) iednll) in
+      xmlInductive kind loc exprs
+  | VernacFixpoint (_, fednll) ->
+      let exprs =
+        List.flatten (* should probably not be flattened *)
+          (List.map
+            (fun (fe, dnl) -> (pp_fixpoint_expr fe) @
+                              (List.map pp_decl_notation dnl)) fednll) in
+      xmlFixpoint exprs
+  | VernacCoFixpoint (_, cfednll) ->
+      (* Nota: it is like VernacFixpoint without so could be merged *)
+      let exprs =
+        List.flatten (* should probably not be flattened *)
+          (List.map
+            (fun (cfe, dnl) -> (pp_cofixpoint_expr cfe) @
+                              (List.map pp_decl_notation dnl)) cfednll) in
+      xmlCoFixpoint exprs
+  | VernacScheme _ as x -> xmlTODO loc x
+  | VernacCombinedScheme _ as x -> xmlTODO loc x
+
+  (* Gallina extensions *)
+  | VernacBeginSection (_, id) -> xmlBeginSection loc (Id.to_string id)
+  | VernacEndSegment (_, id) -> xmlEndSegment loc (Id.to_string id)
+  | VernacNameSectionHypSet _ as x -> xmlTODO loc x
+  | VernacRequire (None,l) ->
+      xmlRequire loc (List.map (fun ref ->
+        xmlReference ref) l)
+  | VernacRequire (Some true,l) ->
+      xmlRequire loc ~attr:["export","true"] (List.map (fun ref ->
+        xmlReference ref) l)
+  | VernacRequire (Some false,l) ->
+      xmlRequire loc ~attr:["import","true"] (List.map (fun ref ->
+        xmlReference ref) l)
+  | VernacImport (true,l) ->
+      xmlImport loc ~attr:["export","true"] (List.map (fun ref ->
+        xmlReference ref) l)
+  | VernacImport (false,l) ->
+      xmlImport loc (List.map (fun ref ->
+        xmlReference ref) l)
+  | VernacCanonical r ->
+      let attr =
+        match r with
+        | AN (Qualid (_, q)) -> ["qualid", string_of_qualid q]
+        | AN (Ident (_, id)) -> ["id", Id.to_string id]
+        | ByNotation (_, s, _) -> ["notation", s] in
+      xmlCanonicalStructure attr loc
+  | VernacCoercion _ as x -> xmlTODO loc x
+  | VernacIdentityCoercion _ as x -> xmlTODO loc x
+
+  (* Type classes *)
+  | VernacInstance _ as x -> xmlTODO loc x
+
+  | VernacContext _ as x -> xmlTODO loc x
+
+  | VernacDeclareInstances _ as x -> xmlTODO loc x
+
+  | VernacDeclareClass _ as x -> xmlTODO loc x
+
+  (* Modules and Module Types *)
+  | VernacDeclareModule _ as x -> xmlTODO loc x
+  | VernacDefineModule _ as x -> xmlTODO loc x
+  | VernacDeclareModuleType _ as x -> xmlTODO loc x
+  | VernacInclude _ as x -> xmlTODO loc x
+
+  (* Solving *)
+
+  | (VernacSolve _ | VernacSolveExistential _) as x ->
+      xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
+
+  (* Auxiliary file and library management *)
+  | VernacAddLoadPath (recf,name,None) ->
+      xmlAddLoaPath loc ~attr:["rec",string_of_bool recf;"path",name] []
+  | VernacAddLoadPath (recf,name,Some dp) ->
+      xmlAddLoaPath loc ~attr:["rec",string_of_bool recf;"path",name]
+        [PCData (Names.DirPath.to_string dp)]
+                 
+  | VernacRemoveLoadPath name -> xmlRemoveLoaPath loc ~attr:["path",name] []
+  | VernacAddMLPath (recf,name) ->
+      xmlAddMLPath loc ~attr:["rec",string_of_bool recf;"path",name] []
+  | VernacDeclareMLModule sl -> xmlDeclareMLModule loc sl
+  | VernacChdir _ as x -> xmlTODO loc x
+
+  (* State management *)
+  | VernacWriteState _ as x -> xmlTODO loc x
+  | VernacRestoreState _ as x -> xmlTODO loc x
+
+  (* Resetting *)
+  | VernacResetName _ as x -> xmlTODO loc x
+  | VernacResetInitial as x -> xmlTODO loc x
+  | VernacBack _ as x -> xmlTODO loc x
+  | VernacBackTo _ -> PCData "VernacBackTo"
+
+  (* Commands *)
+  | VernacDeclareTacticDefinition _ as x -> xmlTODO loc x
+  | VernacCreateHintDb _ as x -> xmlTODO loc x
+  | VernacRemoveHints _ as x -> xmlTODO loc x
+  | VernacHints _ as x -> xmlTODO loc x
+  | VernacSyntacticDefinition ((_, name), (idl, ce), _, _) ->
+      let name = Id.to_string name in
+      let attrs = List.map (fun id -> ("id", Id.to_string id)) idl in
+      xmlNotation attrs name loc [pp_expr ce]
+  | VernacDeclareImplicits _ as x -> xmlTODO loc x
+  | VernacArguments _ as x -> xmlTODO loc x
+  | VernacArgumentsScope _ as x -> xmlTODO loc x
+  | VernacReserve _ as x -> xmlTODO loc x
+  | VernacGeneralizable _ as x -> xmlTODO loc x
+  | VernacSetOpacity _ as x -> xmlTODO loc x
+  | VernacSetStrategy _ as x -> xmlTODO loc x
+  | VernacUnsetOption _ as x -> xmlTODO loc x
+  | VernacSetOption _ as x -> xmlTODO loc x
+  | VernacAddOption _ as x -> xmlTODO loc x
+  | VernacRemoveOption _ as x -> xmlTODO loc x
+  | VernacMemOption _ as x -> xmlTODO loc x
+  | VernacPrintOption _ as x -> xmlTODO loc x
+  | VernacCheckMayEval (_,_,e) -> xmlCheck loc [pp_expr e]
+  | VernacGlobalCheck _ as x -> xmlTODO loc x
+  | VernacDeclareReduction _ as x -> xmlTODO loc x
+  | VernacPrint _ as x -> xmlTODO loc x
+  | VernacSearch _ as x -> xmlTODO loc x
+  | VernacLocate _ as x -> xmlTODO loc x
+  | VernacRegister _ as x -> xmlTODO loc x
+  | VernacComments (cl) ->
+      xmlComment loc (List.flatten (List.map pp_comment cl))
+  | VernacNop as x -> xmlTODO loc x
+
+  (* Stm backdoor *)
+  | VernacStm _ as x -> xmlTODO loc x
+
+  (* Proof management *)
+  | VernacGoal _ as x -> xmlTODO loc x
+  | VernacAbort _ as x -> xmlTODO loc x
+  | VernacAbortAll -> PCData "VernacAbortAll"
+  | VernacRestart as x -> xmlTODO loc x
+  | VernacUndo _ as x -> xmlTODO loc x
+  | VernacUndoTo _ as x -> xmlTODO loc x
+  | VernacBacktrack _ as x -> xmlTODO loc x
+  | VernacFocus _ as x -> xmlTODO loc x
+  | VernacUnfocus as x -> xmlTODO loc x
+  | VernacUnfocused as x -> xmlTODO loc x
+  | VernacBullet _ as x -> xmlTODO loc x
+  | VernacSubproof _ as x -> xmlTODO loc x
+  | VernacEndSubproof as x -> xmlTODO loc x
+  | VernacShow _ as x -> xmlTODO loc x
+  | VernacCheckGuard as x -> xmlTODO loc x
+  | VernacProof (tac,using) ->
+      let tac = Option.map (xmlRawTactic "closingtactic") tac in
+      let using = Option.map (xmlSectionSubsetDescr "using") using in
+      xmlProof loc (Option.List.(cons tac (cons using [])))
+  | VernacProofMode name -> xmlProofMode loc name
+
+  (* Toplevel control *)
+  | VernacToplevelControl _ as x -> xmlTODO loc x
+
+  (* For extension *)
+  | VernacExtend _ as x ->
+      xmlExtend loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
+
+  (* Flags *)
+  | VernacProgram e -> xmlApply loc (Element("program",[],[]) :: [tmpp e loc])
+  | VernacLocal (b,e) ->
+      xmlApply loc (Element("local",["flag",string_of_bool b],[]) ::
+                    [tmpp e loc])
+
+let tmpp v loc =
+  match tmpp v loc with
+  | Element("ltac",_,_) as x -> x
+  | xml -> xmlGallina loc [xml]
diff --git a/stm/texmacspp.mli b/stm/texmacspp.mli
new file mode 100644
index 00000000..58dec8fd
--- /dev/null
+++ b/stm/texmacspp.mli
@@ -0,0 +1,12 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Xml_datatype
+open Vernacexpr
+
+val tmpp : vernac_expr -> Loc.t -> xml
diff --git a/stm/vcs.ml b/stm/vcs.ml
new file mode 100644
index 00000000..dfcbc19a
--- /dev/null
+++ b/stm/vcs.ml
@@ -0,0 +1,193 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Errors
+
+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
+
+  (* Branches have [branch_info] attached to them. *)
+  type ('kind) branch_info = {
+    kind : [> `Master] as 'kind;
+    root : id;
+    pos  : id;
+  }
+
+  type ('kind,'diff,'info) t constraint 'kind = [> `Master ]
+
+  val empty : id -> ('kind,'diff,'info) t
+
+  val current_branch : ('k,'e,'i) t -> Branch.t
+  val branches : ('k,'e,'i) t -> Branch.t list
+
+  val get_branch : ('k,'e,'i) t -> Branch.t -> 'k branch_info
+  val reset_branch : ('k,'e,'i) t -> Branch.t -> id -> ('k,'e,'i) t
+  val branch :
+    ('kind,'e,'i) t -> ?root:id -> ?pos:id ->
+        Branch.t -> 'kind -> ('kind,'e,'i) t
+  val delete_branch : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t
+  val merge :
+    ('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> ?into:Branch.t ->
+            Branch.t -> ('k,'diff,'i) t
+  val commit : ('k,'diff,'i) t -> id -> 'diff -> ('k,'diff,'i) t
+  val rewrite_merge :
+    ('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> at:id ->
+            Branch.t -> ('k,'diff,'i) t
+  val checkout : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t
+
+  val set_info : ('k,'e,'info) t -> id -> 'info -> ('k,'e,'info) t
+  val get_info : ('k,'e,'info) t -> id -> 'info option
+  
+  module NodeSet : Set.S with type elt = id
+
+  val gc : ('k,'e,'info) t -> ('k,'e,'info) t * NodeSet.t
+
+  val reachable : ('k,'e,'info) t -> id -> NodeSet.t
+
+  module Dag : Dag.S with type node = id
+  val dag : ('kind,'diff,'info) t -> ('diff,'info,id*id) Dag.t
+
+  val create_cluster : ('k,'e,'i) t -> id list -> (id * id) -> ('k,'e,'i) t
+  val cluster_of : ('k,'e,'i) t -> id -> (id * id) Dag.Cluster.t option
+  val delete_cluster : ('k,'e,'i) t -> (id * id) Dag.Cluster.t -> ('k,'e,'i) t 
+
+end
+
+module Make(OT : Map.OrderedType) = struct
+
+module Dag = Dag.Make(OT)
+
+type id = OT.t
+
+module NodeSet = Dag.NodeSet
+
+
+module Branch =
+struct
+  type t = string
+  let make =
+    let bid = ref 0 in
+    fun s -> incr bid; string_of_int !bid ^ "_" ^ s
+  let equal = CString.equal
+  let compare = CString.compare
+  let to_string s = s
+  let master = "master"
+end
+
+module BranchMap = Map.Make(Branch)
+
+type 'kind branch_info = {
+  kind : [> `Master] as 'kind;
+  root : id;
+  pos  : id;
+}
+
+type ('kind,'edge,'info) t = {
+  cur_branch   : Branch.t;
+  heads        : 'kind branch_info BranchMap.t;
+  dag          : ('edge,'info,id*id) Dag.t;
+}
+
+let empty root = {
+  cur_branch = Branch.master;
+  heads = BranchMap.singleton Branch.master { root = root; pos = root; kind = `Master };
+  dag = Dag.empty;
+}
+
+let add_node vcs id edges =
+  assert (not (CList.is_empty edges));
+  { vcs with dag =
+     List.fold_left (fun g (t,tgt) -> Dag.add_edge g id t tgt) vcs.dag edges }
+
+let get_branch vcs head =
+  try BranchMap.find head vcs.heads
+  with Not_found -> anomaly (str"head " ++ str head ++ str" not found")
+
+let reset_branch vcs head id =
+  let map name h =
+    if Branch.equal name head then { h with pos = id } else h
+  in
+  { vcs with heads = BranchMap.mapi map vcs.heads; }
+
+let current_branch vcs = vcs.cur_branch
+
+let branch
+  vcs ?(root=(get_branch vcs vcs.cur_branch).pos) ?(pos=root) name kind
+=
+  { vcs with
+      heads = BranchMap.add name { kind; root; pos } vcs.heads;
+      cur_branch = name }
+
+let delete_branch vcs name =
+  if Branch.equal Branch.master name then vcs else
+  let filter n _ = not (Branch.equal n name) in
+  { vcs with heads = BranchMap.filter filter vcs.heads }
+
+let merge vcs id ~ours:tr1 ~theirs:tr2 ?(into = vcs.cur_branch) name =
+  assert (not (Branch.equal name into));
+  let br_id = (get_branch vcs name).pos in
+  let cur_id = (get_branch vcs into).pos in
+  let vcs = add_node vcs id [tr1,cur_id; tr2,br_id] in
+  let vcs = reset_branch vcs into id in
+  vcs
+
+let del_edge id vcs tgt = { vcs with dag = Dag.del_edge vcs.dag id tgt }
+
+let rewrite_merge vcs id ~ours:tr1 ~theirs:tr2 ~at:cur_id name =
+  let br_id = (get_branch vcs name).pos in
+  let old_edges = List.map fst (Dag.from_node vcs.dag id) in
+  let vcs = List.fold_left (del_edge id) vcs old_edges in
+  let vcs = add_node vcs id [tr1,cur_id; tr2,br_id] in
+  vcs
+
+let commit vcs id tr =
+  let vcs = add_node vcs id [tr, (get_branch vcs vcs.cur_branch).pos] in
+  let vcs = reset_branch vcs vcs.cur_branch id in
+  vcs
+
+let checkout vcs name = { vcs with cur_branch = name }
+
+let set_info vcs id info = { vcs with dag = Dag.set_info vcs.dag id info }
+let get_info vcs id = Dag.get_info vcs.dag id
+
+let create_cluster vcs l i = { vcs with dag = Dag.create_cluster vcs.dag l i }
+let cluster_of vcs i = Dag.cluster_of vcs.dag i
+let delete_cluster vcs c = { vcs with dag = Dag.del_cluster vcs.dag c }
+
+let branches vcs = BranchMap.fold (fun x _ accu -> x :: accu) vcs.heads []
+let dag vcs = vcs.dag
+
+let rec closure s d n =
+  let l = try Dag.from_node d n with Not_found -> [] in
+  List.fold_left (fun s (n',_) ->
+    if Dag.NodeSet.mem n' s then s
+    else closure s d n')
+  (Dag.NodeSet.add n s) l
+
+let reachable vcs i = closure Dag.NodeSet.empty vcs.dag i
+
+let gc vcs =
+  let alive =
+    BranchMap.fold (fun b { pos } s -> closure s vcs.dag pos)
+      vcs.heads Dag.NodeSet.empty in
+  let dead = Dag.NodeSet.diff (Dag.all_nodes vcs.dag) alive in
+  { vcs with dag = Dag.del_nodes vcs.dag dead }, dead
+
+end
diff --git a/stm/vcs.mli b/stm/vcs.mli
new file mode 100644
index 00000000..fb79d02c
--- /dev/null
+++ b/stm/vcs.mli
@@ -0,0 +1,90 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* 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 3 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)
+*)
+
+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) t constraint 'kind = [> `Master ]
+  
+  val empty : id -> ('kind,'diff,'info) t
+  
+  val current_branch : ('k,'e,'i) t -> Branch.t
+  val branches : ('k,'e,'i) t -> Branch.t list
+  
+  val get_branch : ('k,'e,'i) t -> Branch.t -> 'k branch_info
+  val reset_branch : ('k,'e,'i) t -> Branch.t -> id -> ('k,'e,'i) t
+  val branch :
+    ('kind,'e,'i) t -> ?root:id -> ?pos:id ->
+        Branch.t -> 'kind -> ('kind,'e,'i) t
+  val delete_branch : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t
+  val merge :
+    ('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> ?into:Branch.t ->
+            Branch.t -> ('k,'diff,'i) t
+  val commit : ('k,'diff,'i) t -> id -> 'diff -> ('k,'diff,'i) t
+  val rewrite_merge :
+    ('k,'diff,'i) t -> id -> ours:'diff -> theirs:'diff -> at:id ->
+            Branch.t -> ('k,'diff,'i) t
+  val checkout : ('k,'e,'i) t -> Branch.t -> ('k,'e,'i) t
+  
+  val set_info : ('k,'e,'info) t -> id -> 'info -> ('k,'e,'info) t
+  val get_info : ('k,'e,'info) t -> id -> 'info option
+
+  module NodeSet : Set.S with type elt = id
+  
+  (* Removes all unreachable nodes and returns them *)
+  val gc : ('k,'e,'info) t -> ('k,'e,'info) t * NodeSet.t
+
+  val reachable : ('k,'e,'info) t -> id -> NodeSet.t
+
+  (* read only dag *)
+  module Dag : Dag.S with type node = id
+  val dag : ('kind,'diff,'info) t -> ('diff,'info,id * id) Dag.t
+ 
+  val create_cluster : ('k,'e,'i) t -> id list -> (id * id) -> ('k,'e,'i) t
+  val cluster_of : ('k,'e,'i) t -> id -> (id * id) Dag.Cluster.t option
+  val delete_cluster : ('k,'e,'i) t -> (id * id) Dag.Cluster.t -> ('k,'e,'i) t 
+
+end
+
+module Make(OT : Map.OrderedType) : S with type id = OT.t
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
new file mode 100644
index 00000000..e9302bb7
--- /dev/null
+++ b/stm/vernac_classifier.ml
@@ -0,0 +1,227 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Vernacexpr
+open Errors
+open Pp
+
+let string_of_in_script b = if b then " (inside script)" else ""
+
+let string_of_vernac_type = function
+  | VtUnknown -> "Unknown"
+  | VtStartProof _ -> "StartProof"
+  | VtSideff _ -> "Sideff"
+  | VtQed VtKeep -> "Qed(keep)"
+  | VtQed VtKeepAsAxiom -> "Qed(admitted)"
+  | VtQed VtDrop -> "Qed(drop)"
+  | VtProofStep false -> "ProofStep"
+  | VtProofStep true -> "ProofStep (parallel)"
+  | VtProofMode s -> "ProofMode " ^ s
+  | VtQuery (b,(id,route)) ->
+      "Query " ^ string_of_in_script b ^ " report " ^ Stateid.to_string id ^
+      " route " ^ string_of_int route
+  | VtStm ((VtFinish|VtJoinDocument|VtObserve _|VtPrintDag|VtWait), b) ->
+      "Stm " ^ string_of_in_script b
+  | VtStm (VtPG, b) -> "Stm PG " ^ string_of_in_script b
+  | VtStm (VtBack _, b) -> "Stm Back " ^ string_of_in_script b
+
+let string_of_vernac_when = function
+  | VtLater -> "Later"
+  | VtNow -> "Now"
+
+let string_of_vernac_classification (t,w) =
+  string_of_vernac_type t ^ " " ^ string_of_vernac_when w
+
+let classifiers = ref []
+let declare_vernac_classifier
+  (s : Vernacexpr.extend_name)
+  (f : Genarg.raw_generic_argument list -> unit -> vernac_classification)
+=
+  classifiers := !classifiers @ [s,f]
+
+let elide_part_of_script_and_now (a, _) =
+  match a with
+  | VtQuery (_,id) -> VtQuery (false,id), VtNow
+  | VtStm (x, _) -> VtStm (x, false), VtNow
+  | x -> x, VtNow
+
+let make_polymorphic (a, b as x) =
+  match a with
+  | VtStartProof (x, _, ids) ->
+      VtStartProof (x, Doesn'tGuaranteeOpacity, ids), b
+  | _ -> x
+
+let undo_classifier = ref (fun _ -> assert false)
+let set_undo_classifier f = undo_classifier := f
+
+let rec classify_vernac e =
+  let rec static_classifier e = match e with
+    (* PG compatibility *)
+    | VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"])
+    | VernacSetOption   ((["Silent"]|["Undo"]|["Printing";"Depth"]),_)
+      when !Flags.print_emacs -> VtStm(VtPG,false), VtNow
+    (* Stm *)
+    | VernacStm Finish -> VtStm (VtFinish, true), VtNow
+    | VernacStm Wait -> VtStm (VtWait, true), VtNow
+    | VernacStm JoinDocument -> VtStm (VtJoinDocument, true), VtNow
+    | VernacStm PrintDag -> VtStm (VtPrintDag, true), VtNow
+    | VernacStm (Observe id) -> VtStm (VtObserve id, true), VtNow
+    | VernacStm (Command x) -> elide_part_of_script_and_now (classify_vernac x)
+    | VernacStm (PGLast x) -> fst (classify_vernac x), VtNow
+    (* Nested vernac exprs *)
+    | VernacProgram e -> classify_vernac e
+    | VernacLocal (_,e) -> classify_vernac e
+    | VernacPolymorphic (b, e) -> 
+      if b || Flags.is_universe_polymorphism () (* Ok or not? *) then
+	make_polymorphic (classify_vernac e)
+      else classify_vernac e
+    | VernacTimeout (_,e) -> classify_vernac e
+    | VernacTime e -> classify_vernac_list e
+    | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
+        (match classify_vernac e with
+        | ( VtQuery _ | VtProofStep _ | VtSideff _
+          | VtStm _ | VtProofMode _ ), _ as x -> x
+        | VtQed _, _ -> VtProofStep false, VtNow
+        | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow)
+    (* Qed *)
+    | VernacAbort _ -> VtQed VtDrop, VtLater
+    | VernacEndProof Admitted -> VtQed VtKeepAsAxiom, VtLater
+    | VernacEndProof _ | VernacExactProof _ -> VtQed VtKeep, VtLater
+    (* Query *)
+    | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _
+    | VernacCheckMayEval _ ->
+        VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
+    (* ProofStep *)
+    | VernacSolve (SelectAllParallel,_,_,_) -> VtProofStep true, VtLater
+    | VernacProof _ 
+    | VernacBullet _ 
+    | VernacFocus _ | VernacUnfocus
+    | VernacSubproof _ | VernacEndSubproof
+    | VernacSolve _ 
+    | VernacCheckGuard
+    | VernacUnfocused
+    | VernacSolveExistential _ -> VtProofStep false, VtLater
+    (* Options changing parser *)
+    | VernacUnsetOption (["Default";"Proof";"Using"])
+    | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow
+    (* StartProof *)
+    | VernacDefinition (
+       (Some Decl_kinds.Discharge,Decl_kinds.Definition),(_,i),ProveBody _) ->
+        VtStartProof("Classic",Doesn'tGuaranteeOpacity,[i]), VtLater
+    | VernacDefinition (_,(_,i),ProveBody _) ->
+        VtStartProof("Classic",GuaranteesOpacity,[i]), VtLater
+    | VernacStartTheoremProof (_,l,_) ->
+        let ids = 
+          CList.map_filter (function (Some(_,i), _) -> Some i | _ -> None) l in
+        VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
+    | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater
+    | VernacFixpoint (_,l) ->
+        let ids, open_proof =
+          List.fold_left (fun (l,b) (((_,id),_,_,_,p),_) ->
+            id::l, b || p = None) ([],false) l in
+        if open_proof
+        then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
+        else VtSideff ids, VtLater
+    | VernacCoFixpoint (_,l) ->
+        let ids, open_proof =
+          List.fold_left (fun (l,b) (((_,id),_,_,p),_) ->
+            id::l, b || p = None) ([],false) l in
+        if open_proof
+        then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
+        else VtSideff ids, VtLater
+    (* Sideff: apply to all open branches. usually run on master only *)
+    | VernacAssumption (_,_,l) ->
+        let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd l) l) in
+        VtSideff ids, VtLater    
+    | VernacDefinition (_,(_,id),DefineBody _) -> VtSideff [id], VtLater
+    | VernacInductive (_,_,l) ->
+        let ids = List.map (fun (((_,(_,id)),_,_,_,cl),_) -> id :: match cl with
+        | Constructors l -> List.map (fun (_,((_,id),_)) -> id) l
+        | RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @
+           CList.map_filter (function
+            | ((_,AssumExpr((_,Names.Name n),_)),_),_ -> Some n
+            | _ -> None) l) l in
+        VtSideff (List.flatten ids), VtLater
+    | VernacScheme l ->
+        let ids = List.map snd (CList.map_filter (fun (x,_) -> x) l) in
+        VtSideff ids, VtLater
+    | VernacCombinedScheme ((_,id),_) -> VtSideff [id], VtLater
+    | VernacUniverse _ | VernacConstraint _
+    | VernacBeginSection _
+    | VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _
+    | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _
+    | VernacChdir _ 
+    | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _
+    | VernacDeclareImplicits _ | VernacArguments _ | VernacArgumentsScope _
+    | VernacReserve _
+    | VernacGeneralizable _
+    | VernacSetOpacity _ | VernacSetStrategy _
+    | VernacUnsetOption _ | VernacSetOption _
+    | VernacAddOption _ | VernacRemoveOption _
+    | VernacMemOption _ | VernacPrintOption _
+    | VernacGlobalCheck _
+    | VernacDeclareReduction _
+    | VernacDeclareClass _ | VernacDeclareInstances _
+    | VernacRegister _
+    | VernacDeclareTacticDefinition _
+    | VernacNameSectionHypSet _
+    | VernacComments _ -> VtSideff [], VtLater
+    (* Who knows *)
+    | VernacLoad _ -> VtSideff [], VtNow
+    (* (Local) Notations have to disappear *)
+    | VernacEndSegment _ -> VtSideff [], VtNow
+    (* Modules with parameters have to be executed: can import notations *)
+    | VernacDeclareModule (exp,(_,id),bl,_)
+    | VernacDefineModule (exp,(_,id),bl,_,_) ->
+        VtSideff [id], if bl = [] && exp = None then VtLater else VtNow
+    | VernacDeclareModuleType ((_,id),bl,_,_) ->
+        VtSideff [id], if bl = [] then VtLater else VtNow
+    (* These commands alter the parser *)
+    | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _
+    | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _
+    | VernacSyntaxExtension _ 
+    | VernacSyntacticDefinition _
+    | VernacTacticNotation _
+    | VernacRequire _ | VernacImport _ | VernacInclude _
+    | VernacDeclareMLModule _
+    | VernacContext _ (* TASSI: unsure *)
+    | VernacProofMode _ 
+    (* These are ambiguous *)
+    | VernacInstance _ -> VtUnknown, VtNow
+    (* Stm will install a new classifier to handle these *)
+    | VernacBack _ | VernacAbortAll
+    | VernacUndoTo _ | VernacUndo _
+    | VernacResetName _ | VernacResetInitial
+    | VernacBacktrack _ | VernacBackTo _ | VernacRestart -> !undo_classifier e
+    (* What are these? *)
+    | VernacNop
+    | VernacToplevelControl _
+    | VernacRestoreState _
+    | VernacWriteState _ -> VtUnknown, VtNow
+    | VernacError _ -> assert false
+    (* Plugins should classify their commands *)
+    | VernacExtend (s,l) ->
+        try List.assoc s !classifiers l ()
+        with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s))
+  and classify_vernac_list = function
+    (* spiwack: It would be better to define a monoid on classifiers.
+       So that the classifier of the list would be the composition of
+       the classifier of the individual commands. Currently: special
+       case for singleton lists.*)
+    | [_,c] -> static_classifier c
+    | l -> VtUnknown,VtNow
+  in
+  let res = static_classifier e in
+    if Flags.is_universe_polymorphism () then
+      make_polymorphic res
+    else res
+
+let classify_as_query =
+  VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
+let classify_as_sideeff = VtSideff [], VtLater
+let classify_as_proofstep = VtProofStep false, VtLater
diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli
new file mode 100644
index 00000000..0680fe84
--- /dev/null
+++ b/stm/vernac_classifier.mli
@@ -0,0 +1,28 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Vernacexpr
+open Genarg
+
+val string_of_vernac_classification : vernac_classification -> string
+
+(** What does a vernacular do *)
+val classify_vernac : vernac_expr -> vernac_classification
+
+(** Install a vernacular classifier for VernacExtend *)
+val declare_vernac_classifier :
+  Vernacexpr.extend_name -> (raw_generic_argument list -> unit -> vernac_classification) -> unit
+
+(** Set by Stm *)
+val set_undo_classifier : (vernac_expr -> vernac_classification) -> unit
+
+(** Standard constant classifiers *)
+val classify_as_query : vernac_classification
+val classify_as_sideeff : vernac_classification
+val classify_as_proofstep : vernac_classification
+
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml
new file mode 100644
index 00000000..84df3ecd
--- /dev/null
+++ b/stm/vio_checking.ml
@@ -0,0 +1,144 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+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(struct end)
+
+module IntOT = struct
+  type t = int
+  let compare = compare
+end
+
+module Pool = Map.Make(IntOT)
+
+let schedule_vio_checking j fs =
+  if j < 1 then Errors.error "The number of workers must be bigger than 0";
+  let jobs = ref [] in
+  List.iter (fun f ->
+    let f =
+      if Filename.check_suffix f ".vio" then Filename.chop_extension f
+      else f in
+    let long_f_dot_v, _,_,_, tasks, _ = Library.load_library_todo f in
+    Stm.set_compilation_hints long_f_dot_v;
+    let infos = Stm.info_tasks tasks in
+    let eta = List.fold_left (fun a (_,t,_) -> a +. t) 0.0 infos in
+    if infos <> [] then jobs := (f, eta, infos) :: !jobs)
+  fs;
+  let cmp_job (_,t1,_) (_,t2,_) = compare t2 t1 in
+  jobs := List.sort cmp_job !jobs;
+  let eta = ref (List.fold_left (fun a j -> a +. pi2 j) 0.0 !jobs) in
+  let pool : Worker.process Pool.t ref = ref Pool.empty in
+  let rec filter_argv b = function
+    | [] -> []
+    | "-schedule-vio-checking" :: rest -> filter_argv true rest
+    | s :: rest when s.[0] = '-' && b -> filter_argv false (s :: rest)
+    | _ :: rest when b -> filter_argv b rest
+    | s :: rest -> s :: filter_argv b rest in
+  let pack = function
+    | [] -> []
+    | ((f,_),_,_) :: _ as l ->
+        let rec aux last acc = function
+          | [] -> [last,acc]
+          | ((f',id),_,_) :: tl when last = f' -> aux last (id::acc) tl
+          | ((f',id),_,_) :: _ as l -> (last,acc) :: aux f' [] l in
+        aux f [] l in
+  let prog = Sys.argv.(0) in  
+  let stdargs = filter_argv false (List.tl (Array.to_list Sys.argv)) in
+  let make_job () =
+    let cur = ref 0.0 in
+    let what = ref [] in
+    let j_left = j - Pool.cardinal !pool in
+    let take_next_file () =
+      let f, t, tasks = List.hd !jobs in
+      jobs := List.tl !jobs;
+      cur := !cur +. t;
+      what := (List.map (fun (n,t,id) -> (f,id),n,t) tasks) @ !what in
+    if List.length !jobs >= j_left then take_next_file ()
+    else while !jobs <> [] &&
+         !cur < max 0.0 (min 60.0 (!eta /. float_of_int j_left)) do
+      let f, t, tasks = List.hd !jobs in
+      jobs := List.tl !jobs;
+      let n, tt, id = List.hd tasks in
+      if List.length tasks > 1 then
+        jobs := (f, t -. tt, List.tl tasks) :: !jobs;
+      cur := !cur +. tt;
+      what := ((f,id),n,tt) :: !what;
+    done;
+    if !what = [] then take_next_file ();
+    eta := !eta -. !cur;
+    let cmp_job (f1,_,_) (f2,_,_) = compare f1 f2 in
+    List.flatten
+      (List.map (fun (f, tl) ->
+        "-check-vio-tasks" :: 
+        String.concat "," (List.map string_of_int tl) :: [f])
+      (pack (List.sort cmp_job !what))) in
+  let rc = ref 0 in
+  while !jobs <> [] || Pool.cardinal !pool > 0 do
+    while Pool.cardinal !pool < j && !jobs <> [] do
+      let args = Array.of_list (stdargs @ make_job ()) in
+      let proc, _, _ = Worker.spawn prog args in
+      pool := Pool.add (Worker.unixpid proc) proc !pool;
+    done;
+    let pid, ret = Unix.wait () in
+    if ret <> Unix.WEXITED 0 then rc := 1;
+    pool := Pool.remove pid !pool;
+  done;
+  exit !rc
+
+let schedule_vio_compilation j fs =
+  if j < 1 then Errors.error "The number of workers must be bigger than 0";
+  let jobs = ref [] in
+  List.iter (fun f ->
+    let f =
+      if Filename.check_suffix f ".vio" then Filename.chop_extension f
+      else f in
+    let paths = Loadpath.get_paths () in
+    let _, long_f_dot_v =
+      System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
+    let aux = Aux_file.load_aux_file_for long_f_dot_v in
+    let eta =
+      try float_of_string (Aux_file.get aux Loc.ghost "vo_compile_time")
+      with Not_found -> 0.0 in
+    jobs := (f, eta) :: !jobs)
+  fs;
+  let cmp_job (_,t1) (_,t2) = compare t2 t1 in
+  jobs := List.sort cmp_job !jobs;
+  let pool : Worker.process Pool.t ref = ref Pool.empty in
+  let rec filter_argv b = function
+    | [] -> []
+    | "-schedule-vio2vo" :: rest -> filter_argv true rest
+    | s :: rest when s.[0] = '-' && b -> filter_argv false (s :: rest)
+    | _ :: rest when b -> filter_argv b rest
+    | s :: rest -> s :: filter_argv b rest in
+  let prog = Sys.argv.(0) in  
+  let stdargs = filter_argv false (List.tl (Array.to_list Sys.argv)) in
+  let make_job () =
+    let f, t = List.hd !jobs in
+    jobs := List.tl !jobs;
+    [ "-vio2vo"; f ] in
+  let rc = ref 0 in
+  while !jobs <> [] || Pool.cardinal !pool > 0 do
+    while Pool.cardinal !pool < j && !jobs <> [] do
+      let args = Array.of_list (stdargs @ make_job ()) in
+      let proc, _, _ = Worker.spawn prog args in
+      pool := Pool.add (Worker.unixpid proc) proc !pool;
+    done;
+    let pid, ret = Unix.wait () in
+    if ret <> Unix.WEXITED 0 then rc := 1;
+    pool := Pool.remove pid !pool;
+  done;
+  exit !rc
+
+  
diff --git a/stm/vio_checking.mli b/stm/vio_checking.mli
new file mode 100644
index 00000000..e2da5026
--- /dev/null
+++ b/stm/vio_checking.mli
@@ -0,0 +1,13 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* [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 00000000..db3bb5ad
--- /dev/null
+++ b/stm/workerPool.ml
@@ -0,0 +1,128 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+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 Errors.noncritical e ->
+    Printf.eprintf "Handshake with %s failed: %s\n"
+      worker_id (Printexc.to_string e);
+    exit 1
+
+let worker_handshake slave_ic slave_oc =
+  try
+    let v = (CThread.thread_friendly_input_value slave_ic : int) in
+    if v <> magic_no then begin
+      prerr_endline "Handshake failed: protocol mismatch\n";
+      exit 1;
+    end;
+    Marshal.to_channel slave_oc v []; flush slave_oc;
+  with e when Errors.noncritical e ->
+    prerr_endline ("Handshake failed: " ^ Printexc.to_string e);
+    exit 1
+
+let locking { lock; pool = p } f =
+  try
+    Mutex.lock lock;
+    let x = f p in
+    Mutex.unlock lock;
+    x
+  with e -> Mutex.unlock lock; raise e
+
+let rec create_worker extra pool id =
+  let cancel = ref false in
+  let name, process, ic, oc as worker = Model.spawn id in
+  master_handshake name ic oc;
+  let exit () = cancel := true; cleanup pool; Thread.exit () in
+  let cancelled () = !cancel in
+  let cpanel = { exit; cancelled; extra } in
+  let manager = Thread.create (Model.manager cpanel) worker in
+  { name; cancel; manager; process }
+  
+and cleanup x = locking x begin fun { workers; count; extra_arg } ->
+  workers := List.map (function
+    | { cancel } as w when !cancel = false -> w
+    | _ -> let n = !count in incr count; create_worker extra_arg x n)
+  !workers
+end
+
+let n_workers x = locking x begin fun { workers } ->
+   List.length !workers
+end
+
+let is_empty x = locking x begin fun { workers } -> !workers = [] end
+
+let create extra_arg ~size = let x = {
+    lock = Mutex.create ();
+    pool = {
+      extra_arg;
+      workers = ref [];
+      count = ref size;
+  }} in
+  locking x begin fun { workers } ->
+     workers := CList.init size (create_worker extra_arg x)
+  end;
+  x
+
+let cancel n x = locking x begin fun { workers } ->
+  List.iter (fun { name; cancel } -> if n = name then cancel := true) !workers
+end
+
+let cancel_all x = locking x begin fun { workers } ->
+  List.iter (fun { cancel } -> cancel := true) !workers
+end
+
+let destroy x = locking x begin fun { workers } ->
+  List.iter (fun { cancel } -> cancel := true) !workers;
+  workers := []
+end
+
+end
diff --git a/stm/workerPool.mli b/stm/workerPool.mli
new file mode 100644
index 00000000..f46303b5
--- /dev/null
+++ b/stm/workerPool.mli
@@ -0,0 +1,46 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+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