Adding a stm/ folder, as asked during last workgroup. It was essentially moving

files around. A bunch of files from lib/ that were only used in the STM were
moved, as well as part of toplevel/ related to the STM.

11 files changed, 0 insertions, 764 deletions

diff --git a/lib/dag.ml b/lib/dag.ml
deleted file mode 100644
index 9622f4c1fa..0000000000
--- a/lib/dag.ml
+++ /dev/null
@@ -1,134 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013     *)
-(*   \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/lib/dag.mli b/lib/dag.mli
deleted file mode 100644
index 702ccd80f8..0000000000
--- a/lib/dag.mli
+++ /dev/null
@@ -1,52 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013     *)
-(*   \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/lib/lib.mllib b/lib/lib.mllib
index 50621df20d..edef3da037 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -10,7 +10,6 @@ Unicode
 System
 CThread
 Spawn
-Spawned
 Trie
 Profile
 Explore
@@ -23,7 +22,3 @@ Genarg
 Ephemeron
 Future
 RemoteCounter
-Dag
-Vcs
-TQueue
-WorkerPool
diff --git a/lib/spawned.ml b/lib/spawned.ml
deleted file mode 100644
index d025945690..0000000000
--- a/lib/spawned.ml
+++ /dev/null
@@ -1,84 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \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;
-  cin, cout
-
-let controller h p =
-  prerr_endline "starting controller thread";
-  let main () =
-    let ic, oc = open_bin_connection h p in
-    let rec loop () =
-      try
-        match input_value ic with
-        | Hello _ -> prerr_endline "internal protocol error"; exit 1
-        | ReqDie -> prerr_endline "death sentence received"; exit 0
-        | ReqStats ->
-            output_value oc (RespStats (Gc.stat ())); flush oc; loop ()
-      with
-      | e ->
-        prerr_endline ("control channel broken: " ^ Printexc.to_string e);
-        exit 1 in
-    loop () in
-  ignore(Thread.create main ())
-
-let main_channel = ref None
-let control_channel = ref None
-
-let channels = ref None
-
-let init_channels () =
-  if !channels <> None then Errors.anomaly(Pp.str "init_channels called twice");
-  let () = match !main_channel with
-  | None -> ()
-  | Some (Socket(mh,mp)) ->
-    channels := Some (open_bin_connection mh mp);
-  | Some AnonPipe ->
-    let stdin = Unix.in_channel_of_descr (Unix.dup Unix.stdin) in
-    let stdout = Unix.out_channel_of_descr (Unix.dup Unix.stdout) in
-    Unix.dup2 Unix.stderr Unix.stdout;
-    set_binary_mode_in stdin true;
-    set_binary_mode_out stdout true;
-    channels := Some (stdin, stdout);
-  in
-  match !control_channel with
-  | None -> ()
-  | Some (Socket (ch, cp)) ->
-    controller ch cp
-  | Some AnonPipe ->
-    Errors.anomaly (Pp.str "control channel cannot be a pipe")
-
-let get_channels () =
-  match !channels with
-  | None -> Errors.anomaly(Pp.str "init_channels not called")
-  | Some(ic, oc) -> ic, oc
-
diff --git a/lib/spawned.mli b/lib/spawned.mli
deleted file mode 100644
index 18b88dc64b..0000000000
--- a/lib/spawned.mli
+++ /dev/null
@@ -1,22 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \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 -> in_channel * out_channel
-
diff --git a/lib/tQueue.ml b/lib/tQueue.ml
deleted file mode 100644
index 783c545fd0..0000000000
--- a/lib/tQueue.ml
+++ /dev/null
@@ -1,64 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-type 'a t = {
-  queue: 'a Queue.t;
-  lock : Mutex.t;
-  cond : Condition.t;
-  mutable nwaiting : int;
-  cond_waiting : Condition.t;
-}
-
-let create () = {
-  queue = Queue.create ();
-  lock = Mutex.create ();
-  cond = Condition.create ();
-  nwaiting = 0;
-  cond_waiting = Condition.create ();
-}
-
-let pop ({ queue = q; lock = m; cond = c; cond_waiting = cn } as tq) =
-  Mutex.lock m;
-  while Queue.is_empty q do
-    tq.nwaiting <- tq.nwaiting + 1;
-    Condition.signal cn;
-    Condition.wait c m;
-    tq.nwaiting <- tq.nwaiting - 1;
-  done;
-  let x = Queue.pop q in
-  Condition.signal c;
-  Condition.signal cn;
-  Mutex.unlock m;
-  x
-
-let push { queue = q; lock = m; cond = c } x =
-  Mutex.lock m;
-  Queue.push x q;
-  Condition.signal c;
-  Mutex.unlock m
-
-let wait_until_n_are_waiting_and_queue_empty j tq =
-  Mutex.lock tq.lock;
-  while not (Queue.is_empty tq.queue) || tq.nwaiting < j do
-    Condition.wait tq.cond_waiting tq.lock
-  done;
-  Mutex.unlock tq.lock
-
-let dump { queue; lock } =
-  let l = ref [] in
-  Mutex.lock lock;
-  while not (Queue.is_empty queue) do l := Queue.pop queue :: !l done;
-  Mutex.unlock lock;
-  List.rev !l
-
-let reorder tq rel =
-  Mutex.lock tq.lock;
-  let l = ref [] in
-  while not (Queue.is_empty tq.queue) do l := Queue.pop tq.queue :: !l done;
-  List.iter (fun x -> Queue.push x tq.queue) (List.sort rel !l);
-  Mutex.unlock tq.lock
diff --git a/lib/tQueue.mli b/lib/tQueue.mli
deleted file mode 100644
index a3ea5532fc..0000000000
--- a/lib/tQueue.mli
+++ /dev/null
@@ -1,17 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \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 : 'a t -> 'a
-val push : 'a t -> 'a -> unit
-val reorder : 'a t -> ('a -> 'a -> int) -> unit
-val wait_until_n_are_waiting_and_queue_empty : int -> 'a t -> unit
-val dump : 'a t -> 'a list
diff --git a/lib/vcs.ml b/lib/vcs.ml
deleted file mode 100644
index e2513b1c1e..0000000000
--- a/lib/vcs.ml
+++ /dev/null
@@ -1,193 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013     *)
-(*   \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) Dag.t
-
-  val create_cluster : ('k,'e,'i) t -> id list -> id -> ('k,'e,'i) t
-  val cluster_of : ('k,'e,'i) t -> id -> id Dag.Cluster.t option
-  val delete_cluster : ('k,'e,'i) t -> id Dag.Cluster.t -> ('k,'e,'i) t 
-
-end
-
-module Make(OT : Map.OrderedType) = struct
-
-module Dag = Dag.Make(OT)
-
-type id = OT.t
-
-module NodeSet = Dag.NodeSet
-
-
-module Branch =
-struct
-  type t = string
-  let make =
-    let bid = ref 0 in
-    fun s -> incr bid; string_of_int !bid ^ "_" ^ s
-  let equal = CString.equal
-  let compare = CString.compare
-  let to_string s = s
-  let master = "master"
-end
-
-module BranchMap = Map.Make(Branch)
-
-type 'kind branch_info = {
-  kind : [> `Master] as 'kind;
-  root : id;
-  pos  : id;
-}
-
-type ('kind,'edge,'info) t = {
-  cur_branch   : Branch.t;
-  heads        : 'kind branch_info BranchMap.t;
-  dag          : ('edge,'info,id) Dag.t;
-}
-
-let empty root = {
-  cur_branch = Branch.master;
-  heads = BranchMap.singleton Branch.master { root = root; pos = root; kind = `Master };
-  dag = Dag.empty;
-}
-
-let add_node vcs id edges =
-  assert (not (CList.is_empty edges));
-  { vcs with dag =
-     List.fold_left (fun g (t,tgt) -> Dag.add_edge g id t tgt) vcs.dag edges }
-
-let get_branch vcs head =
-  try BranchMap.find head vcs.heads
-  with Not_found -> anomaly (str"head " ++ str head ++ str" not found")
-
-let reset_branch vcs head id =
-  let map name h =
-    if Branch.equal name head then { h with pos = id } else h
-  in
-  { vcs with heads = BranchMap.mapi map vcs.heads; }
-
-let current_branch vcs = vcs.cur_branch
-
-let branch
-  vcs ?(root=(get_branch vcs vcs.cur_branch).pos) ?(pos=root) name kind
-=
-  { vcs with
-      heads = BranchMap.add name { kind; root; pos } vcs.heads;
-      cur_branch = name }
-
-let delete_branch vcs name =
-  if Branch.equal Branch.master name then vcs else
-  let filter n _ = not (Branch.equal n name) in
-  { vcs with heads = BranchMap.filter filter vcs.heads }
-
-let merge vcs id ~ours:tr1 ~theirs:tr2 ?(into = vcs.cur_branch) name =
-  assert (not (Branch.equal name into));
-  let br_id = (get_branch vcs name).pos in
-  let cur_id = (get_branch vcs into).pos in
-  let vcs = add_node vcs id [tr1,cur_id; tr2,br_id] in
-  let vcs = reset_branch vcs into id in
-  vcs
-
-let del_edge id vcs tgt = { vcs with dag = Dag.del_edge vcs.dag id tgt }
-
-let rewrite_merge vcs id ~ours:tr1 ~theirs:tr2 ~at:cur_id name =
-  let br_id = (get_branch vcs name).pos in
-  let old_edges = List.map fst (Dag.from_node vcs.dag id) in
-  let vcs = List.fold_left (del_edge id) vcs old_edges in
-  let vcs = add_node vcs id [tr1,cur_id; tr2,br_id] in
-  vcs
-
-let commit vcs id tr =
-  let vcs = add_node vcs id [tr, (get_branch vcs vcs.cur_branch).pos] in
-  let vcs = reset_branch vcs vcs.cur_branch id in
-  vcs
-
-let checkout vcs name = { vcs with cur_branch = name }
-
-let set_info vcs id info = { vcs with dag = Dag.set_info vcs.dag id info }
-let get_info vcs id = Dag.get_info vcs.dag id
-
-let create_cluster vcs l i = { vcs with dag = Dag.create_cluster vcs.dag l i }
-let cluster_of vcs i = Dag.cluster_of vcs.dag i
-let delete_cluster vcs c = { vcs with dag = Dag.del_cluster vcs.dag c }
-
-let branches vcs = BranchMap.fold (fun x _ accu -> x :: accu) vcs.heads []
-let dag vcs = vcs.dag
-
-let rec closure s d n =
-  let l = try Dag.from_node d n with Not_found -> [] in
-  List.fold_left (fun s (n',_) ->
-    if Dag.NodeSet.mem n' s then s
-    else closure s d n')
-  (Dag.NodeSet.add n s) l
-
-let reachable vcs i = closure Dag.NodeSet.empty vcs.dag i
-
-let gc vcs =
-  let alive =
-    BranchMap.fold (fun b { pos } s -> closure s vcs.dag pos)
-      vcs.heads Dag.NodeSet.empty in
-  let dead = Dag.NodeSet.diff (Dag.all_nodes vcs.dag) alive in
-  { vcs with dag = Dag.del_nodes vcs.dag dead }, dead
-
-end
diff --git a/lib/vcs.mli b/lib/vcs.mli
deleted file mode 100644
index 6c3571a082..0000000000
--- a/lib/vcs.mli
+++ /dev/null
@@ -1,90 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013     *)
-(*   \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) Dag.t
- 
-  val create_cluster : ('k,'e,'i) t -> id list -> id -> ('k,'e,'i) t
-  val cluster_of : ('k,'e,'i) t -> id -> id Dag.Cluster.t option
-  val delete_cluster : ('k,'e,'i) t -> id Dag.Cluster.t -> ('k,'e,'i) t 
-
-end
-
-module Make(OT : Map.OrderedType) : S with type id = OT.t
diff --git a/lib/workerPool.ml b/lib/workerPool.ml
deleted file mode 100644
index fcae4f20d6..0000000000
--- a/lib/workerPool.ml
+++ /dev/null
@@ -1,73 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-module Make(Worker : sig
-  type process
-  val spawn :
-      ?prefer_sock:bool -> ?env:string array -> string -> string array ->
-      process * in_channel * out_channel
-end) = struct
-
-type worker_id = int
-type spawn =
-  args:string array -> env:string array -> unit ->
-    in_channel * out_channel * Worker.process
-
-let slave_managers = ref None
-
-let n_workers () = match !slave_managers with
-  | None -> 0
-  | Some managers -> Array.length managers
-let is_empty () = !slave_managers = None
-
-let magic_no = 17
-
-let master_handshake worker_id ic oc =
-  try
-    Marshal.to_channel oc magic_no [];  flush oc;
-    let n = (Marshal.from_channel ic : int) in
-    if n <> magic_no then begin
-      Printf.eprintf "Handshake with %d failed: protocol mismatch\n" worker_id;
-      exit 1;
-    end
-  with e when Errors.noncritical e ->
-    Printf.eprintf "Handshake with %d failed: %s\n"
-      worker_id (Printexc.to_string e);
-    exit 1
-
-let respawn n ~args ~env () =
-  let proc, ic, oc = Worker.spawn ~env Sys.argv.(0) args in
-  master_handshake n ic oc;
-  ic, oc, proc
-
-let init ~size:n ~manager:manage_slave =
-  slave_managers := Some
-    (Array.init n (fun x ->
-       let cancel = ref false in
-       cancel, Thread.create (manage_slave ~cancel (x+1)) (respawn (x+1))))
-
-let cancel n =
-  match !slave_managers with
-  | None -> ()
-  | Some a ->
-      let switch, _ = a.(n) in
-      switch := true
-      
-let worker_handshake slave_ic slave_oc =
-  try
-    let v = (Marshal.from_channel slave_ic : int) in
-    if v <> magic_no then begin
-      prerr_endline "Handshake failed: protocol mismatch\n";
-      exit 1;
-    end;
-    Marshal.to_channel slave_oc v []; flush slave_oc;
-  with e when Errors.noncritical e ->
-    prerr_endline ("Handshake failed: " ^ Printexc.to_string e);
-    exit 1
-
-end
diff --git a/lib/workerPool.mli b/lib/workerPool.mli
deleted file mode 100644
index d7a546929f..0000000000
--- a/lib/workerPool.mli
+++ /dev/null
@@ -1,30 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-module Make(Worker : sig
-  type process
-  val spawn :
-      ?prefer_sock:bool -> ?env:string array -> string -> string array ->
-      process * in_channel * out_channel
-end) : sig
-
-type worker_id = int
-type spawn =
-  args:string array -> env:string array -> unit ->
-    in_channel * out_channel * Worker.process
-
-val init :
-  size:int -> manager:(cancel:bool ref -> worker_id -> spawn -> unit) -> unit
-val is_empty : unit -> bool
-val n_workers : unit -> int
-val cancel : worker_id -> unit
-
-(* The worker should call this function *)
-val worker_handshake : in_channel -> out_channel -> unit
-
-end