.vi files: .vo files without proofs

File format:
 The .vo file format changed:
   - after the magic number there are 3 segments. A segment is made of 3
     components: bynary int, an ocaml value, a digest.  The binary int
     is the position of the digest, so that one can skip the value without
     unmarshalling it
   - the first segment is the library, as before
   - the second segment is the STM task list
   - the third segment is the opaque table, as before
 A .vo file has a complete opaque table (all proof terms are there).
 A .vi file follows the same format of a .vo file, but some entries
 in the opaque table are missing.  A proof task is stocked instead.

Utilities:
 coqc: option -quick generates a .vi insted of a .vo
 coq_makefile: target quick to generate all .vi
 coqdep: generate deps for .vi files too
 votour: can browse .vi files too, the first question is which segment
         should be read
 coqchk: rejects .vi files

4 files changed, 72 insertions, 19 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index b75a225588..ad3ce78799 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -320,6 +320,7 @@ let parse_args arglist =
     |"-q" -> no_load_rc ()
     |"-quality" -> term_quality := true; no_load_rc ()
     |"-quiet"|"-silent" -> Flags.make_silent true
+    |"-quick" -> Flags.compilation_mode := BuildVi
     |"-time" -> Flags.time := true
     |"-unicode" -> add_require "Utf8_core"
     |"-v"|"--version" -> Usage.version (exitcode ())
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index fe8cc66a85..f800b49fb9 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -594,6 +594,8 @@ module Slaves : sig
   val set_reach_known_state :
     (?redefine_qed:bool -> cache:Summary.marshallable -> Stateid.t -> unit) -> unit
 
+  type tasks
+  val dump : unit -> tasks
 
 end = struct (* {{{ *)
 
@@ -604,6 +606,7 @@ end = struct (* {{{ *)
     val pop : 'a t -> 'a
     val push : 'a t -> 'a -> unit
     val wait_until_n_are_waiting_and_queue_empty : int -> 'a t -> unit
+    val dump : 'a t -> 'a list
 
   end = struct (* {{{ *)
 
@@ -639,6 +642,13 @@ end = struct (* {{{ *)
       while not (Queue.is_empty q) || !n < j do Condition.wait cn m done;
       Mutex.unlock m
 
+    let dump (q,m,_,_,_) =
+      let l = ref [] in
+      Mutex.lock m;
+      while not (Queue.is_empty q) do l := Queue.pop q :: !l done;
+      Mutex.unlock m;
+      List.rev !l
+
   end (* }}} *)
 
   module SlavesPool : sig
@@ -745,10 +755,11 @@ end = struct (* {{{ *)
   let cancel_switch_of_task = function
     | TaskBuildProof (_,_,_,_,c,_) -> c
 
+  let build_proof_here_core eop () =
+    !reach_known_state ~cache:`No eop;
+    Proof_global.return_proof ()
   let build_proof_here (id,valid) eop =
-    Future.create (State.exn_on id ~valid) (fun () ->
-      !reach_known_state ~cache:`No eop;
-      Proof_global.return_proof ())
+    Future.create (State.exn_on id ~valid) (build_proof_here_core eop)
 
   let slave_respond msg =
     match msg with
@@ -818,13 +829,22 @@ end = struct (* {{{ *)
   let queue : task TQueue.t = TQueue.create ()
 
   let wait_all_done () =
-    TQueue.wait_until_n_are_waiting_and_queue_empty
-      (SlavesPool.n_slaves ()) queue
+    if not (SlavesPool.is_empty ()) then
+      TQueue.wait_until_n_are_waiting_and_queue_empty
+        (SlavesPool.n_slaves ()) queue
 
   let build_proof ~exn_info:(id,valid as exn_info) ~start ~stop ~name =
     let cancel_switch = ref false in
     if SlavesPool.is_empty () then
-      build_proof_here exn_info stop, cancel_switch
+      if !Flags.compilation_mode = Flags.BuildVi then begin
+        let force () : Entries.proof_output list Future.assignement =
+          try `Val (build_proof_here_core stop ()) with e -> `Exn e in
+        let f,assign = Future.create_delegate ~force (State.exn_on id ~valid) in
+        TQueue.push queue
+          (TaskBuildProof(exn_info,start,stop,assign,cancel_switch,name));
+        f, cancel_switch
+      end else
+        build_proof_here exn_info stop, cancel_switch
     else 
       let f, assign = Future.create_delegate (State.exn_on id ~valid) in
       Pp.feedback (Interface.InProgress 1);
@@ -1024,6 +1044,15 @@ end = struct (* {{{ *)
         flush_all (); exit 1
     done
 
+  (* For external users this name is nicer than request *)
+  type tasks = request list
+  let dump () =
+    assert(SlavesPool.is_empty ()); (* ATM, we allow that only if no slaves *)
+    let tasks = TQueue.dump queue in
+    prerr_endline (Printf.sprintf "dumping %d\n" (List.length tasks));
+    let tasks = List.map request_of_task tasks in
+    tasks
+
 end (* }}} *)
 
 (* Runs all transactions needed to reach a state *)
@@ -1408,6 +1437,9 @@ let join () =
   jab (VCS.get_branch_pos VCS.Branch.master);
   VCS.print ()
 
+type tasks = Slaves.tasks
+let dump () = Slaves.dump ()
+
 let merge_proof_branch qast keep brname =
   let brinfo = VCS.get_branch brname in
   let qed fproof = { qast; keep; brname; brinfo; fproof } in
diff --git a/toplevel/stm.mli b/toplevel/stm.mli
index 3c5bd63db4..d821a2536a 100644
--- a/toplevel/stm.mli
+++ b/toplevel/stm.mli
@@ -40,6 +40,9 @@ val finish : unit -> unit
 
 (* Joins the entire document.  Implies finish, but also checks proofs *)
 val join : unit -> unit
+(* To save to disk an incomplete document *)
+type tasks
+val dump : unit -> tasks
 
 (* Id of the tip of the current branch *)
 val get_current_state : unit -> Stateid.t
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index eaa5b75494..27735d2d9a 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -305,7 +305,6 @@ and read_vernac_file verbosely s =
     close_input in_chan input;    (* we must close the file first *)
     match e with
       | End_of_input ->
-          Stm.join ();
           if do_beautify () then
             pr_new_syntax (Loc.make_loc (max_int,max_int)) None
       | _ -> raise_with_file fname (disable_drop e)
@@ -341,15 +340,33 @@ let load_vernac verb file =
 
 (* Compile a vernac file (f is assumed without .v suffix) *)
 let compile verbosely f =
-  let ldir,long_f_dot_v = Flags.verbosely Library.start_library f in
-  Dumpglob.start_dump_glob long_f_dot_v;
-  Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
-  if !Flags.xml_export then Hook.get f_xml_start_library ();
-  let _ = load_vernac verbosely long_f_dot_v in
-  let pfs = Pfedit.get_all_proof_names () in
-  if not (List.is_empty pfs) then
-    (pperrnl (str "Error: There are pending proofs"); flush_all (); exit 1);
-  if !Flags.xml_export then Hook.get f_xml_end_library ();
-  Library.save_library_to ldir (long_f_dot_v ^ "o");
-  Dumpglob.end_dump_glob ()
-
+  let check_pending_proofs () =
+    let pfs = Pfedit.get_all_proof_names () in
+    if not (List.is_empty pfs) then
+      (pperrnl (str "Error: There are pending proofs"); flush_all (); exit 1) in
+  match !Flags.compilation_mode with
+  | BuildVo ->
+      let ldir,long_f_dot_v = Flags.verbosely Library.start_library f in
+      Aux_file.start_aux_file_for long_f_dot_v;
+      Dumpglob.start_dump_glob long_f_dot_v;
+      Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
+      if !Flags.xml_export then Hook.get f_xml_start_library ();
+      let wall_clock1 = Unix.gettimeofday () in
+      let _ = load_vernac verbosely long_f_dot_v in
+      Stm.join ();
+      let wall_clock2 = Unix.gettimeofday () in
+      check_pending_proofs ();
+      Library.save_library_to ldir long_f_dot_v;
+      Aux_file.record_in_aux_at Loc.ghost "vo_compile_time"
+        (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
+      Aux_file.stop_aux_file ();
+      if !Flags.xml_export then Hook.get f_xml_end_library ();
+      Dumpglob.end_dump_glob ()
+  | BuildVi ->
+      let ldir, long_f_dot_v = Flags.verbosely Library.start_library f in
+      Dumpglob.noglob ();
+      let _ = load_vernac verbosely long_f_dot_v in
+      Stm.finish ();
+      check_pending_proofs ();
+      let todo = Stm.dump () in
+      Library.save_library_to ~todo ldir long_f_dot_v