.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

1 files changed, 7 insertions, 5 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 366eb3695..5a1671fe6 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -301,12 +301,11 @@ let intern_from_file (dir, f) =
   let (md,table,digest) =
     try
       let ch = with_magic_number_check raw_intern_library f in
-      let (md:Cic.library_disk) = System.marshal_in f ch in
-      let digest = System.digest_in f ch in
-      let (table:Cic.opaque_table) = System.marshal_in f ch in
+      let (md:Cic.library_disk), _, digest = System.marshal_in_segment f ch in
+      let (tasks:'a option), _, _ = System.marshal_in_segment f ch in
+      let (table:Cic.opaque_table), pos, checksum =
+        System.marshal_in_segment f ch in
       (* Verification of the final checksum *)
-      let pos = pos_in ch in
-      let checksum = System.digest_in f ch in
       let () = close_in ch in
       let ch = open_in f in
       if not (String.equal (Digest.channel ch pos) checksum) then
@@ -315,6 +314,9 @@ let intern_from_file (dir, f) =
       if dir <> md.md_name then
         errorlabstrm "intern_from_file"
           (name_clash_message dir md.md_name f);
+      if tasks <> None then
+        errorlabstrm "intern_from_file"
+          (str "The file "++str f++str " contains unfinished tasks");
       (* Verification of the unmarshalled values *)
       Validate.validate !Flags.debug Values.v_lib md;
       Validate.validate !Flags.debug Values.v_opaques table;