.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, 8 insertions, 5 deletions

diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 4dcd10ece..a952881c8 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -298,7 +298,7 @@ let canonize f =
     | (f,_) :: _ -> escape f
     | _ -> escape f
 
-let rec traite_fichier_Coq verbose f =
+let rec traite_fichier_Coq suffixe verbose f =
   try
     let chan = open_in f in
     let buf = Lexing.from_channel chan in
@@ -314,7 +314,7 @@ let rec traite_fichier_Coq verbose f =
 	          addQueue deja_vu_v str;
                   try
                     let file_str = safe_assoc verbose f str in
-                    printf " %s%s" (canonize file_str) !suffixe
+                    printf " %s%s" (canonize file_str) suffixe
                   with Not_found ->
 		    if verbose && not (Hashtbl.mem coqlibKnown str) then
                       warning_module_notfound f str
@@ -325,7 +325,7 @@ let rec traite_fichier_Coq verbose f =
 	        addQueue deja_vu_v [str];
                 try
                   let file_str = Hashtbl.find vKnown [str] in
-                  printf " %s%s" (canonize file_str) !suffixe
+                  printf " %s%s" (canonize file_str) suffixe
                 with Not_found ->
 		  if not (Hashtbl.mem coqlibKnown [str]) then
 		    warning_notfound f s
@@ -359,7 +359,7 @@ let rec traite_fichier_Coq verbose f =
                   let file_str = Hashtbl.find vKnown [str] in
                   let canon = canonize file_str in
                   printf " %s.v" canon;
-                  traite_fichier_Coq true (canon ^ ".v")
+                  traite_fichier_Coq suffixe true (canon ^ ".v")
                 with Not_found -> ()
        	      end
           | AddLoadPath _ | AddRecLoadPath _ -> (* TODO *) ()
@@ -417,7 +417,10 @@ let coq_dependencies () =
        let ename = escape name in
        let glob = if !option_noglob then "" else " "^ename^".glob" in
        printf "%s%s%s %s.v.beautified: %s.v" ename !suffixe glob ename ename;
-       traite_fichier_Coq true (name ^ ".v");
+       traite_fichier_Coq !suffixe true (name ^ ".v");
+       printf "\n";
+       printf "%s.vi: %s.v" ename ename;
+       traite_fichier_Coq ".vi" true (name ^ ".v");
        printf "\n";
        flush stdout)
     (List.rev !vAccu)