summaryrefslogtreecommitdiff
path: root/tools/coqdep_common.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdep_common.ml')
-rw-r--r--tools/coqdep_common.ml114
1 files changed, 76 insertions, 38 deletions
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 253fb037..2e6a15ce 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -22,8 +22,8 @@ let stdout = Pervasives.stdout
let option_c = ref false
let option_noglob = ref false
-let option_slash = ref false
let option_natdynlk = ref true
+let option_boot = ref false
let option_mldep = ref None
let norec_dirs = ref ([] : string list)
@@ -33,9 +33,19 @@ let suffixe = ref ".vo"
type dir = string option
-(* filename for printing *)
-let (//) s1 s2 =
- if !option_slash then s1^"/"^s2 else Filename.concat s1 s2
+(* Filename.concat but always with a '/' *)
+let is_dir_sep s i =
+ match Sys.os_type with
+ | "Unix" -> s.[i] = '/'
+ | "Cygwin" | "Win32" ->
+ let c = s.[i] in c = '/' || c = '\\' || c = ':'
+ | _ -> assert false
+
+let (//) dirname filename =
+ let l = String.length dirname in
+ if l = 0 || is_dir_sep dirname (l-1)
+ then dirname ^ filename
+ else dirname ^ "/" ^ filename
(** [get_extension f l] checks whether [f] has one of the extensions
listed in [l]. It returns [f] without its extension, alongside with
@@ -51,7 +61,7 @@ let rec get_extension f = function
let basename_noext filename =
let fn = Filename.basename filename in
- try Filename.chop_extension fn with _ -> fn
+ try Filename.chop_extension fn with Invalid_argument _ -> fn
(** ML Files specified on the command line. In the entries:
- the first string is the basename of the file, without extension nor
@@ -76,10 +86,10 @@ let vAccu = ref ([] : (string * string) list)
let addQueue q v = q := v :: !q
-let safe_hash_add clq q (k,v) =
+let safe_hash_add cmp clq q (k,v) =
try
let v2 = Hashtbl.find q k in
- if v<>v2 then
+ if not (cmp v v2) then
let rec add_clash = function
(k1,l1)::cltl when k=k1 -> (k1,v::l1)::cltl
| cl::cltl -> cl::add_clash cltl
@@ -91,19 +101,24 @@ let safe_hash_add clq q (k,v) =
(** Files found in the loadpaths.
For the ML files, the string is the basename without extension.
- To allow ML source filename to be potentially capitalized,
- we perform a double search.
*)
+let warning_ml_clash x s suff s' suff' =
+ if suff = suff' then
+ eprintf
+ "*** Warning: %s%s already found in %s (discarding %s%s)\n" x suff
+ (match s with None -> "." | Some d -> d)
+ ((match s' with None -> "." | Some d -> d) // x) suff
+
let mkknown () =
- let h = (Hashtbl.create 19 : (string, dir) Hashtbl.t) in
- let add x s = if Hashtbl.mem h x then () else Hashtbl.add h x s
- and iter f = Hashtbl.iter f h
+ let h = (Hashtbl.create 19 : (string, dir * string) Hashtbl.t) in
+ let add x s suff =
+ try let s',suff' = Hashtbl.find h x in warning_ml_clash x s' suff' s suff
+ with Not_found -> Hashtbl.add h x (s,suff)
+ and iter f = Hashtbl.iter (fun x (s,_) -> f x s) h
and search x =
- try Some (Hashtbl.find h (String.uncapitalize x))
- with Not_found ->
- try Some (Hashtbl.find h (String.capitalize x))
- with Not_found -> None
+ try Some (fst (Hashtbl.find h x))
+ with Not_found -> None
in add, iter, search
let add_ml_known, iter_ml_known, search_ml_known = mkknown ()
@@ -122,7 +137,7 @@ let error_cannot_parse s (i,j) =
let warning_module_notfound f s =
eprintf "*** Warning: in file %s, library " f;
- eprintf "%s.v is required and has not been found in loadpath!\n"
+ eprintf "%s.v is required and has not been found in the loadpath!\n"
(String.concat "." s);
flush stderr
@@ -142,7 +157,7 @@ let warning_clash file dir =
let f = Filename.basename f1 in
let d1 = Filename.dirname f1 in
let d2 = Filename.dirname f2 in
- let dl = List.map Filename.dirname (List.rev fl) in
+ let dl = List.rev_map Filename.dirname fl in
eprintf
"*** Warning: in file %s, \n required library %s matches several files in path\n (found %s.v in "
file (String.concat "." dir) f;
@@ -265,10 +280,10 @@ let escape =
Buffer.clear s';
for i = 0 to String.length s - 1 do
let c = s.[i] in
- if c = ' ' or c = '#' or c = ':' (* separators and comments *)
- or c = '%' (* pattern *)
- or c = '?' or c = '[' or c = ']' or c = '*' (* expansion in filenames *)
- or i=0 && c = '~' && (String.length s = 1 || s.[1] = '/' ||
+ 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 *)
then begin
@@ -283,13 +298,16 @@ let escape =
done;
Buffer.contents s'
+let compare_file f1 f2 =
+ absolute_dir (Filename.dirname f1) = absolute_dir (Filename.dirname f2)
+
let canonize f =
let f' = absolute_dir (Filename.dirname f) // Filename.basename f in
match List.filter (fun (_,full) -> f' = full) !vAccu with
| (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
@@ -305,7 +323,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
@@ -316,7 +334,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
@@ -350,7 +368,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 *) ()
@@ -408,7 +426,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.vio: %s.v" ename ename;
+ traite_fichier_Coq ".vio" true (name ^ ".v");
printf "\n";
flush stdout)
(List.rev !vAccu)
@@ -418,18 +439,28 @@ let rec suffixes = function
| [name] -> [[name]]
| dir::suffix as l -> l::suffixes suffix
-let add_known phys_dir log_dir f =
- match get_extension f [".v";".ml";".mli";".ml4";".mllib";".mlpack"] with
+let add_caml_known phys_dir _ f =
+ let basename,suff =
+ get_extension f [".ml";".mli";".ml4";".mllib";".mlpack"] in
+ match suff with
+ | ".ml"|".ml4" -> add_ml_known basename (Some phys_dir) suff
+ | ".mli" -> add_mli_known basename (Some phys_dir) suff
+ | ".mllib" -> add_mllib_known basename (Some phys_dir) suff
+ | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff
+ | _ -> ()
+
+let add_known recur phys_dir log_dir f =
+ match get_extension f [".v";".vo"] with
| (basename,".v") ->
let name = log_dir@[basename] in
let file = phys_dir//basename in
- let paths = suffixes name in
+ let paths = if recur then suffixes name else [name] in
List.iter
- (fun n -> safe_hash_add clash_v vKnown (n,file)) paths
- | (basename,(".ml"|".ml4")) -> add_ml_known basename (Some phys_dir)
- | (basename,".mli") -> add_mli_known basename (Some phys_dir)
- | (basename,".mllib") -> add_mllib_known basename (Some phys_dir)
- | (basename,".mlpack") -> add_mlpack_known basename (Some phys_dir)
+ (fun n -> safe_hash_add compare_file clash_v vKnown (n,file)) paths
+ | (basename,".vo") when not(!option_boot) ->
+ 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
| _ -> ()
(* Visits all the directories under [dir], including [dir],
@@ -456,11 +487,18 @@ let rec add_directory recur add_file phys_dir log_dir =
done
with End_of_file -> closedir dirh
+(** -Q semantic: go in subdirs but only full logical paths are known. *)
let add_dir add_file phys_dir log_dir =
- try add_directory false add_file phys_dir log_dir with Unix_error _ -> ()
+ try add_directory true (add_file false) phys_dir log_dir with Unix_error _ -> ()
+(** -R semantic: go in subdirs and suffixes of logical paths are known. *)
let add_rec_dir add_file phys_dir log_dir =
- handle_unix_error (add_directory true add_file phys_dir) log_dir
+ handle_unix_error (add_directory true (add_file true) phys_dir) log_dir
+
+(** -I semantic: do not go in subdirs. *)
+let add_caml_dir phys_dir =
+ handle_unix_error (add_directory true add_caml_known phys_dir) []
+
let rec treat_file old_dirname old_name =
let name = Filename.basename old_name
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-12 18:02:20 +0000