Implementing support for vos/vok files.

A .vos file stores the result of compiling statements (defs, lemmas)
but not proofs.
A .vok file is an empty file that denotes successful compilation of
the full contents of a .v file.
Unlike a .vio file, a .vos file does not store suspended proofs,
so it is more lightweight. It cannot be completed into a .vo file.

1 files changed, 160 insertions, 117 deletions

diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 8beb314046..ddedec12f8 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -235,15 +235,15 @@ let file_name s = function
 let depend_ML str =
   match search_mli_known str, search_ml_known str with
     | Some mlidir, Some mldir ->
-	let mlifile = file_name str mlidir
-	and mlfile = file_name str mldir in
-	(" "^mlifile^".cmi"," "^mlfile^".cmx")
+        let mlifile = file_name str mlidir
+        and mlfile = file_name str mldir in
+        (" "^mlifile^".cmi"," "^mlfile^".cmx")
     | None, Some mldir ->
-	let mlfile = file_name str mldir in
-	(" "^mlfile^".cmo"," "^mlfile^".cmx")
+        let mlfile = file_name str mldir in
+        (" "^mlfile^".cmo"," "^mlfile^".cmx")
     | Some mlidir, None ->
-	let mlifile = file_name str mlidir in
-	(" "^mlifile^".cmi"," "^mlifile^".cmi")
+        let mlifile = file_name str mlidir in
+        (" "^mlifile^".cmi"," "^mlifile^".cmi")
     | None, None -> "", ""
 
 let soustraite_fichier_ML dep md ext =
@@ -254,9 +254,9 @@ let soustraite_fichier_ML dep md ext =
     let a_faire_opt = ref "" in
     List.iter
       (fun str ->
-	 let byte,opt = depend_ML str in
-	 a_faire := !a_faire ^ byte;
-	 a_faire_opt := !a_faire_opt ^ opt)
+         let byte,opt = depend_ML str in
+         a_faire := !a_faire ^ byte;
+         a_faire_opt := !a_faire_opt ^ opt)
       (List.rev list);
     (!a_faire, !a_faire_opt)
   with
@@ -274,15 +274,15 @@ let autotraite_fichier_ML md ext =
     let a_faire_opt = ref "" in
     begin try
       while true do
-	let (Use_module str) = caml_action buf in
-	if StrSet.mem str !deja_vu then
-	  ()
-	else begin
-	  deja_vu := StrSet.add str !deja_vu;
-	  let byte,opt = depend_ML str in
-	  a_faire := !a_faire ^ byte;
-	  a_faire_opt := !a_faire_opt ^ opt
-	end
+        let (Use_module str) = caml_action buf in
+        if StrSet.mem str !deja_vu then
+          ()
+        else begin
+          deja_vu := StrSet.add str !deja_vu;
+          let byte,opt = depend_ML str in
+          a_faire := !a_faire ^ byte;
+          a_faire_opt := !a_faire_opt ^ opt
+        end
       done
     with Fin_fichier -> ()
     end;
@@ -301,14 +301,14 @@ let traite_fichier_modules md ext =
     let list = mllib_list (Lexing.from_channel chan) in
     List.fold_left
       (fun a_faire str -> match search_mlpack_known str with
-	| Some mldir ->
-	  let file = file_name str mldir in
+        | Some mldir ->
+          let file = file_name str mldir in
           a_faire @ [file]
-	| None ->
-	  match search_ml_known str with
-	    | Some mldir ->
-	      let file = file_name str mldir in
-              a_faire @ [file]
+        | None ->
+          match search_ml_known str with
+            | Some mldir ->
+              let file = file_name str mldir in
+                    a_faire @ [file]
             | None -> a_faire) [] list
   with
     | Sys_error _ -> []
@@ -329,16 +329,16 @@ let escape =
       let c = s.[i] in
       if c = ' ' || c = '#' || c = ':' (* separators and comments *)
         || c = '%' (* pattern *)
-	|| c = '?' || c = '[' || c = ']' || c = '*' (* expansion in filenames *)
-	|| i=0 && c = '~' && (String.length s = 1 || s.[1] = '/' || 
-	    'A' <= s.[1] && s.[1] <= 'Z' || 
-	    'a' <= s.[1] && s.[1] <= 'z') (* homedir expansion *)
+        || c = '?' || c = '[' || c = ']' || c = '*' (* expansion in filenames *)
+        || i=0 && c = '~' && (String.length s = 1 || s.[1] = '/' ||
+            'A' <= s.[1] && s.[1] <= 'Z' ||
+            'a' <= s.[1] && s.[1] <= 'z') (* homedir expansion *)
       then begin
-	let j = ref (i-1) in
-	while !j >= 0 && s.[!j] = '\\' do 
-	  Buffer.add_char s' '\\'; decr j (* escape all preceding '\' *)
-	done;
-	Buffer.add_char s' '\\';
+        let j = ref (i-1) in
+        while !j >= 0 && s.[!j] = '\\' do
+          Buffer.add_char s' '\\'; decr j (* escape all preceding '\' *)
+        done;
+        Buffer.add_char s' '\\';
       end;
       if c = '$' then Buffer.add_char s' '$';
       Buffer.add_char s' c
@@ -362,75 +362,116 @@ end
 
 module VCache = Set.Make(VData)
 
-let rec traite_fichier_Coq suffixe verbose f =
+(** To avoid reading .v files several times for computing dependencies,
+    once for .vo, once for .vio, and once for .vos extensions, the
+    following code performs a single pass and produces a structured
+    list of dependencies, separating dependencies on compiled Coq files
+    (those loaded by [Require]) from other dependencies, e.g. dependencies
+    on ".v" files (for [Load]) or ".cmx", ".cmo", etc... (for [Declare]). *)
+
+type dependency =
+  | DepRequire of string (* one basename, to which we later append .vo or .vio or .vos *)
+  | DepOther of string   (* filenames of dependencies, separated by spaces *)
+
+let string_of_dependency_list suffix_for_require deps =
+  let string_of_dep = function
+    | DepRequire basename -> basename ^ suffix_for_require
+    | DepOther s -> s
+    in
+  String.concat " " (List.map string_of_dep deps)
+
+let rec find_dependencies basename =
+  let verbose = true in (* for past/future use? *)
   try
+    (* Visited marks *)
+    let visited_ml = ref StrSet.empty in
+    let visited_v = ref VCache.empty in
+    let should_visit_v_and_mark from str =
+       if not (VCache.mem (from, str) !visited_v) then begin
+          visited_v := VCache.add (from, str) !visited_v;
+          true
+       end else false
+       in
+    (* Output: dependencies found *)
+    let dependencies = ref [] in
+    let add_dep dep =
+       dependencies := dep::!dependencies in
+    let add_dep_other s =
+       add_dep (DepOther s) in
+
+    (* Reading file contents *)
+    let f = basename ^ ".v" in
     let chan = open_in f in
     let buf = Lexing.from_channel chan in
-    let deja_vu_v = ref VCache.empty in
-    let deja_vu_ml = ref StrSet.empty in
     try
       while true do
-      	let tok = coq_action buf in
-	match tok with
-	  | Require (from, strl) ->
-	      List.iter (fun str ->
-		if not (VCache.mem (from, str) !deja_vu_v) then begin
-	          deja_vu_v := VCache.add (from, str) !deja_vu_v;
-                  try
-                    let file_str = safe_assoc from verbose f str in
-                    printf " %s%s" (canonize file_str) suffixe
-                  with Not_found ->
-		    if verbose && not (is_in_coqlib ?from str) then
-		      let str =
-			match from with
-			  | None -> str
-			  | Some pth -> pth @ str
-		      in
-                      warning_module_notfound f str
-       		end) strl
-	  | Declare sl ->
-	      let declare suff dir s =
-		let base = escape (file_name s dir) in
-                match !option_dynlink with
-                | No -> ()
-                | Byte -> printf " %s%s" base suff
-                | Opt -> printf " %s.cmxs" base
-                | Both -> printf " %s%s %s.cmxs" base suff base
-                | Variable ->
-                   printf " %s%s" base
-                    (if suff=".cmo" then "$(DYNOBJ)" else "$(DYNLIB)")
+        let tok = coq_action buf in
+        match tok with
+        | Require (from, strl) ->
+            List.iter (fun str ->
+              if should_visit_v_and_mark from str then begin
+              try
+                let file_str = safe_assoc from verbose f str in
+                add_dep (DepRequire (canonize file_str))
+              with Not_found ->
+                  if verbose && not (is_in_coqlib ?from str) then
+                    let str =
+                      match from with
+                      | None -> str
+                      | Some pth -> pth @ str
+                      in
+                  warning_module_notfound f str
+              end) strl
+        | Declare sl ->
+            let declare suff dir s =
+              let base = escape (file_name s dir) in
+              match !option_dynlink with
+              | No -> ()
+              | Byte -> add_dep_other (sprintf "%s%s" base suff)
+              | Opt -> add_dep_other (sprintf "%s.cmxs" base)
+              | Both -> add_dep_other (sprintf "%s%s" base suff);
+                        add_dep_other (sprintf "%s.cmxs" base)
+              | Variable -> add_dep_other (sprintf "%s%s" base
+                  (if suff=".cmo" then "$(DYNOBJ)" else "$(DYNLIB)"))
               in
-	      let decl str =
-                let s = basename_noext str in
-		if not (StrSet.mem s !deja_vu_ml) then begin
-		  deja_vu_ml := StrSet.add s !deja_vu_ml;
-		  match search_mllib_known s with
-		    | Some mldir -> declare ".cma" mldir s
-		    | None ->
-		      match search_mlpack_known s with
-			| Some mldir -> declare ".cmo" mldir s
-			| None ->
-			  match search_ml_known s with
-			    | Some mldir -> declare ".cmo" mldir s
-			    | None -> warning_declare f str
-		end
-	      in List.iter decl sl
-	  | Load str ->
-	      let str = Filename.basename str in
-	      if not (VCache.mem (None, [str]) !deja_vu_v) then begin
-	        deja_vu_v := VCache.add (None, [str]) !deja_vu_v;
-                try
-                  let (file_str, _) = Hashtbl.find vKnown [str] in
-                  let canon = canonize file_str in
-                  printf " %s.v" canon;
-                  traite_fichier_Coq suffixe true (canon ^ ".v")
-                with Not_found -> ()
-       	      end
-          | AddLoadPath _ | AddRecLoadPath _ -> (* TODO *) ()
-      done
-    with Fin_fichier -> close_in chan
-       | Syntax_error (i,j) -> close_in chan; error_cannot_parse f (i,j)
-  with Sys_error _ -> ()
+            let decl str =
+              let s = basename_noext str in
+              if not (StrSet.mem s !visited_ml) then begin
+                visited_ml := StrSet.add s !visited_ml;
+                match search_mllib_known s with
+                  | Some mldir -> declare ".cma" mldir s
+                  | None ->
+                    match search_mlpack_known s with
+                  | Some mldir -> declare ".cmo" mldir s
+                  | None ->
+                    match search_ml_known s with
+                      | Some mldir -> declare ".cmo" mldir s
+                      | None -> warning_declare f str
+                end
+                in
+              List.iter decl sl
+        | Load str ->
+            let str = Filename.basename str in
+            if should_visit_v_and_mark None [str] then begin
+              try
+                let (file_str, _) = Hashtbl.find vKnown [str] in
+                let canon = canonize file_str in
+                add_dep_other (sprintf "%s.v" canon);
+                let deps = find_dependencies canon in
+                List.iter add_dep deps
+              with Not_found -> ()
+            end
+        | AddLoadPath _ | AddRecLoadPath _ -> (* TODO: will this be handled? *) ()
+      done;
+      List.rev !dependencies
+    with
+    | Fin_fichier ->
+        close_in chan;
+        List.rev !dependencies
+    | Syntax_error (i,j) ->
+        close_in chan;
+        error_cannot_parse f (i,j)
+  with Sys_error _ -> [] (* TODO: report an error? *)
 
 
 let mL_dependencies () =
@@ -439,8 +480,8 @@ let mL_dependencies () =
        let fullname = file_name name dirname in
        let (dep,dep_opt) = traite_fichier_ML fullname ext in
        let intf = match search_mli_known name with
-	 | None -> ""
-	 | Some mldir -> " "^(file_name name mldir)^".cmi"
+         | None -> ""
+         | Some mldir -> " "^(file_name name mldir)^".cmi"
        in
        let efullname = escape fullname in
        printf "%s.cmo:%s%s\n" efullname dep intf;
@@ -481,12 +522,14 @@ let coq_dependencies () =
     (fun (name,_) ->
        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 !suffixe true (name ^ ".v");
-       printf "\n";
-       printf "%s.vio: %s.v" ename ename;
-       traite_fichier_Coq ".vio" true (name ^ ".v");
-       printf "\n%!")
+       let deps = find_dependencies name in
+       printf "%s%s%s %s.v.beautified %s.required_vo: %s.v %s\n" ename !suffixe glob ename ename ename
+        (string_of_dependency_list !suffixe deps);
+       printf "%s.vio: %s.v %s\n" ename ename
+        (string_of_dependency_list ".vio" deps);
+       printf "%s.vos %s.vok %s.required_vos: %s.v %s\n" ename ename ename ename
+        (string_of_dependency_list ".vos" deps);
+       printf "%!")
     (List.rev !vAccu)
 
 let rec suffixes = function
@@ -505,26 +548,26 @@ let add_caml_known phys_dir _ f =
     | _ -> ()
 
 let add_coqlib_known recur phys_dir log_dir f =
-  match get_extension f [".vo"; ".vio"] with
-    | (basename, (".vo" | ".vio")) ->
+  match get_extension f [".vo"; ".vio"; ".vos"] with
+    | (basename, (".vo" | ".vio" | ".vos")) ->
         let name = log_dir@[basename] in
         let paths = if recur then suffixes name else [name] in
         List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths
     | _ -> ()
 
 let add_known recur phys_dir log_dir f =
-  match get_extension f [".v"; ".vo"; ".vio"] with
+  match get_extension f [".v"; ".vo"; ".vio"; ".vos"] with
     | (basename,".v") ->
-	let name = log_dir@[basename] in
-	let file = phys_dir//basename in
-	let () = safe_hash_add compare_file clash_v vKnown (name, (file, true)) in
-	if recur then
+        let name = log_dir@[basename] in
+        let file = phys_dir//basename in
+        let () = safe_hash_add compare_file clash_v vKnown (name, (file, true)) in
+        if recur then
           let paths = List.tl (suffixes name) in
           let iter n = safe_hash_add compare_file clash_v vKnown (n, (file, false)) in
           List.iter iter paths
-    | (basename, (".vo" | ".vio")) when not(!option_boot) ->
+    | (basename, (".vo" | ".vio" | ".vos")) when not(!option_boot) ->
         let name = log_dir@[basename] in
-	let paths = if recur then suffixes name else [name] in
+        let paths = if recur then suffixes name else [name] in
         List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths
     | _ -> ()
 
@@ -576,12 +619,12 @@ let rec treat_file old_dirname old_name =
   let complete_name = file_name name dirname in
   match try (stat complete_name).st_kind with _ -> S_BLK with
     | S_DIR ->
-	(if name.[0] <> '.' then
+        (if name.[0] <> '.' then
            let newdirname =
              match dirname with
                | None -> name
                | Some d -> d//name
-	   in
+           in
            Array.iter (treat_file (Some newdirname)) (Sys.readdir complete_name))
     | S_REG ->
         (match get_extension name [".v";".ml";".mli";".mlg";".mllib";".mlpack"] with