.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, 47 insertions, 6 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index b79f80d22..0cefc90c4 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -45,6 +45,8 @@ let boot = ref false
 
 let batch_mode = ref false
 
+type compilation_mode = BuildVo | BuildVi
+let compilation_mode = ref BuildVo
 let coq_slave_mode = ref (-1)
 let coq_slaves_number = ref 1
 
diff --git a/lib/flags.mli b/lib/flags.mli
index 0b7adf33f..f0b676641 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -11,6 +11,8 @@
 val boot : bool ref
 
 val batch_mode : bool ref
+type compilation_mode = BuildVo | BuildVi
+val compilation_mode : compilation_mode ref
 
 val coq_slave_mode : int ref
 val coq_slaves_number : int ref
diff --git a/lib/system.ml b/lib/system.ml
index 015124e5b..aa6671116 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -114,17 +114,49 @@ let try_remove filename =
     msg_warning
       (str"Could not remove file " ++ str filename ++ str" which is corrupted!")
 
-let error_corrupted file = error (file ^ " is corrupted, try to rebuild it.")
+let error_corrupted file s = error (file ^": " ^ s ^ ". Try to rebuild it.")
+
+let input_binary_int f ch =
+  try input_binary_int ch
+  with
+  | End_of_file -> error_corrupted f "premature end of file"
+  | Failure s -> error_corrupted f s
+let output_binary_int ch x = output_binary_int ch x; flush ch
 
 let marshal_out ch v = Marshal.to_channel ch v []; flush ch
 let marshal_in filename ch =
   try Marshal.from_channel ch
-  with End_of_file | Failure _ -> error_corrupted filename
+  with
+  | End_of_file -> error_corrupted filename "premature end of file"
+  | Failure s -> error_corrupted filename s
 
 let digest_out = Digest.output
 let digest_in filename ch =
   try Digest.input ch
-  with End_of_file | Failure _ -> error_corrupted filename
+  with
+  | End_of_file -> error_corrupted filename "premature end of file"
+  | Failure s -> error_corrupted filename s
+
+let marshal_out_segment f ch v =
+  let start = pos_out ch in
+  output_binary_int ch 0;  (* dummy value for stop *)
+  marshal_out ch v;
+  let stop = pos_out ch in
+  seek_out ch start;
+  output_binary_int ch stop;
+  seek_out ch stop;
+  digest_out ch (Digest.file f)
+
+let marshal_in_segment f ch =
+  let stop = (input_binary_int f ch : int) in
+  let v = marshal_in f ch in
+  let digest = digest_in f ch in
+  v, stop, digest
+
+let skip_in_segment f ch =
+  let stop = (input_binary_int f ch : int) in
+  seek_in ch stop;
+  stop, digest_in f ch
 
 exception Bad_magic_number of string
 
@@ -136,11 +168,12 @@ let raw_extern_intern magic =
   and intern_state filename =
     try
       let channel = open_in_bin filename in
-      if not (Int.equal (input_binary_int channel) magic) then
+      if not (Int.equal (input_binary_int filename channel) magic) then
         raise (Bad_magic_number filename);
       channel
-    with End_of_file | Failure _ | Sys_error _ ->
-      error_corrupted filename
+    with
+    | End_of_file -> error_corrupted filename "premature end of file"
+    | Failure s | Sys_error s -> error_corrupted filename s
   in
   (extern_state,intern_state)
 
diff --git a/lib/system.mli b/lib/system.mli
index 2513ca19d..2e286a40c 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -52,6 +52,10 @@ val marshal_in : string -> in_channel -> 'a
 val digest_out : out_channel -> Digest.t -> unit
 val digest_in : string -> in_channel -> Digest.t
 
+val marshal_out_segment : string -> out_channel -> 'a -> unit
+val marshal_in_segment : string -> in_channel -> 'a * int * Digest.t
+val skip_in_segment : string -> in_channel -> int * Digest.t
+
 (** {6 Sending/receiving once with external executable } *)
 
 val connect : (out_channel -> unit) -> (in_channel -> 'a) -> string -> 'a