From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- tools/coqdep_common.ml | 114 ++++++++++++++++++++++++++++++++----------------- 1 file changed, 76 insertions(+), 38 deletions(-) (limited to 'tools/coqdep_common.ml') 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 *) -(* 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 -- cgit v1.2.3