Change in vo format : digest aren't Marshalled anymore

 Since digests are strings (of size 16), we just dump them
 now in vo files (cf. Digest.output) instead of using Marshal
 on them : this is cleaner and saves a few bytes.

 Increased VOMAGIC to clearly identify this change in the format.
 Please rerun ./configure after this commit.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16722 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 43 insertions, 29 deletions

diff --git a/CHANGES b/CHANGES
index 0cb2b7bdf..f74566ec6 100644
--- a/CHANGES
+++ b/CHANGES
@@ -88,6 +88,8 @@ Internal Infrastructure
 - The file states/initial.coq does not exist anymore. Instead, coqtop
   initially does a "Require" of Prelude.vo (or nothing when given
   the options -noinit or -nois).
+- The format of vo files has slightly changed : cf final comments in
+  checker/cic.mli
 - The build system does not produce anymore programs named coqtop.opt
   and a symbolic link to coqtop. Instead, coqtop is now directly
   an executable compiled with the best OCaml compiler available.
diff --git a/checker/check.ml b/checker/check.ml
index 0d8a4cd22..f1fe3b8c5 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -302,11 +302,11 @@ let intern_from_file (dir, f) =
     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:Digest.t) = 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
       (* Verification of the final checksum *)
       let pos = pos_in ch in
-      let (checksum:Digest.t) = System.marshal_in f 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
diff --git a/checker/cic.mli b/checker/cic.mli
index 0b732e4b9..7e0cae20a 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -390,9 +390,9 @@ type opaque_table = constr array
 
 (** A .vo file is currently made of :
 
-    1) a magic number
+    1) a magic number (4 bytes, cf output_binary_int)
     2) a marshalled [library_disk] structure
-    3) a marshalled [Digest.t] string
+    3) a [Digest.t] string (16 bytes)
     4) a marshalled [opaque_table]
-    5) a marshalled [Digest.t] string
+    5) a [Digest.t] string (16 bytes)
 *)
diff --git a/checker/values.ml b/checker/values.ml
index b39d90548..eb43ec3e1 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 09a4e5d657809e040f50837a78fe6dfe checker/cic.mli
+MD5 01def72abe22a5b53c7cbe4de4b9695b checker/cic.mli
 
 *)
 
diff --git a/checker/votour.ml b/checker/votour.ml
index afc1c17a9..11b95c93c 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -135,7 +135,7 @@ let visit_vo f =
   let ch = open_in_bin f in
   let _magic = input_binary_int ch in
   let lib = (input_value ch : Obj.t) in (* actually Cic.library_disk *)
-  let _   = (input_value ch : Digest.t) in
+  let _   = Digest.input ch in
   let tbl = (input_value ch : Obj.t) in (* actually Cic.opaque_table *)
   let () = close_in ch in
   let o = if !opaque then tbl else lib in
diff --git a/configure b/configure
index d68a4d87e..43317f1f5 100755
--- a/configure
+++ b/configure
@@ -7,8 +7,8 @@
 ##################################
 
 VERSION=trunk
-VOMAGIC=08211
-STATEMAGIC=58211
+VOMAGIC=08511
+STATEMAGIC=58511
 DATE=`LC_ALL=C LANG=C date +"%B %Y"`
 
 # Create the bin/ directory if non-existent
diff --git a/lib/system.ml b/lib/system.ml
index d2788de93..37b8dee4c 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -114,12 +114,17 @@ let try_remove filename =
     msg_warning
       (str"Could not remove file " ++ str filename ++ str" which is corrupted!")
 
-let marshal_out ch v = Marshal.to_channel ch v []
+let error_corrupted file = error (file ^ " is corrupted, try to rebuild it.")
+
+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 _ (* e.g. "truncated object" *) ->
-      error (filename ^ " is corrupted, try to rebuild it.")
+  with End_of_file | Failure _ -> error_corrupted filename
+
+let digest_out = Digest.output
+let digest_in filename ch =
+  try Digest.input ch
+  with End_of_file | Failure _ -> error_corrupted filename
 
 exception Bad_magic_number of string
 
diff --git a/lib/system.mli b/lib/system.mli
index c9c1df08a..2513ca19d 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -31,9 +31,6 @@ val find_file_in_path :
   and a suffix. The intern functions raise the exception [Bad_magic_number]
   when the check fails, with the full file name. *)
 
-val marshal_out : out_channel -> 'a -> unit
-val marshal_in : string -> in_channel -> 'a
-
 exception Bad_magic_number of string
 
 val raw_extern_intern : int ->
@@ -44,6 +41,17 @@ val extern_intern : ?warn:bool -> int ->
 
 val with_magic_number_check : ('a -> 'b) -> 'a -> 'b
 
+(** Clones of Marshal.to_channel (with flush) and
+    Marshal.from_channel (with nice error message) *)
+
+val marshal_out : out_channel -> 'a -> unit
+val marshal_in : string -> in_channel -> 'a
+
+(** Clones of Digest.output and Digest.input (with nice error message) *)
+
+val digest_out : out_channel -> Digest.t -> unit
+val digest_in : string -> in_channel -> Digest.t
+
 (** {6 Sending/receiving once with external executable } *)
 
 val connect : (out_channel -> unit) -> (in_channel -> 'a) -> string -> 'a
diff --git a/library/library.ml b/library/library.ml
index 472b1fb1d..44e8286ce 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -286,11 +286,11 @@ let fetch_opaque_table (f,pos,digest) =
     Pp.msg_info (Pp.str "Fetching opaque terms in " ++ str f);
     let ch = System.with_magic_number_check raw_intern_library f in
     let () = seek_in ch pos in
-    if not (String.equal (System.marshal_in f ch) digest) then raise Faulty;
+    if not (String.equal (System.digest_in f ch) digest) then raise Faulty;
     let table = (System.marshal_in f ch : Term.constr array) in
-    (* Verification of the final digest (the one also covering the opaques) *)
+    (* Check of the final digest (the one also covering the opaques) *)
     let pos' = pos_in ch in
-    let digest' = (System.marshal_in f ch : Digest.t) in
+    let digest' = 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') digest') then raise Faulty;
@@ -368,9 +368,9 @@ let mk_library md digest =
 
 let intern_from_file f =
   let ch = System.with_magic_number_check raw_intern_library f in
-  let lmd = System.marshal_in f ch in
+  let lmd = (System.marshal_in f ch : library_disk) in
   let pos = pos_in ch in
-  let digest = System.marshal_in f ch in
+  let digest = System.digest_in f ch in
   register_library_filename lmd.md_name f;
   add_opaque_table lmd.md_name (ToFetch (f,pos,digest));
   let library = mk_library lmd digest in
@@ -617,17 +617,16 @@ let save_library_to dir f =
     md_imports = Array.of_list (current_reexports ()) } in
   if Array.exists (fun (d,_) -> DirPath.equal d dir) md.md_deps then
     error_recursively_dependent_library dir;
+  (* Open the vo file and write the magic number *)
   let (f',ch) = raw_extern_library f in
   try
-    System.marshal_out ch md;
-    flush ch;
-    let di = Digest.file f' in
-    System.marshal_out ch di;
-    System.marshal_out ch table;
-    flush ch;
-    let di = Digest.file f' in
-    System.marshal_out ch di;
+    (* Writing vo payload *)
+    System.marshal_out ch md; (* env + objs *)
+    System.digest_out ch (Digest.file f'); (* 1st checksum *)
+    System.marshal_out ch table; (* opaques *)
+    System.digest_out ch (Digest.file f'); (* 2nd checksum *)
     close_out ch;
+    (* Writing native code files *)
     if not !Flags.no_native_compiler then begin
     let lp = Loadpath.get_load_paths () in
     let map_path p = CUnix.string_of_physical_path (Loadpath.physical p) in