From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- tools/coqdep_common.ml | 95 ++++++++++++++++++++------------------------------ 1 file changed, 38 insertions(+), 57 deletions(-) (limited to 'tools/coqdep_common.ml') diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 58c8e884..0064aebd 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -9,10 +9,11 @@ open Printf open Coqdep_lexer open Unix +open Minisys (** [coqdep_boot] is a stripped-down version of [coqdep], whose behavior is the one of [coqdep -boot]. Its only dependencies - are [Coqdep_lexer] and [Unix], and it should stay so. + are [Coqdep_lexer], [Unix] and [Minisys], and it should stay so. If it need someday some additional information, pass it via options (see for instance [option_natdynlk] below). *) @@ -32,26 +33,11 @@ let option_boot = ref false let option_mldep = ref None let norec_dirs = ref StrSet.empty -let norec_dirnames = ref (List.fold_right StrSet.add ["CVS"; "_darcs"] StrSet.empty) let suffixe = ref ".vo" type dir = string option -(* 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 the extension. When no extension match, [(f,"")] is returned *) @@ -179,11 +165,6 @@ let warning_module_notfound f s = eprintf "*** Warning: in file %s, library %s is required and has not been found in the loadpath!\n%!" f (String.concat "." s) -let warning_notfound f s = - eprintf "*** Warning: in file %s, the file " f; - eprintf "%s.v is required and has not been found!\n" s; - flush stderr - let warning_declare f s = eprintf "*** Warning: in file %s, declared ML module " f; eprintf "%s has not been found!\n" s; @@ -203,6 +184,10 @@ let warning_clash file dir = eprintf "%s and %s; used the latter)\n" d2 d1 | _ -> assert false +let warning_cannot_open_dir dir = + eprintf "*** Warning: cannot open %s\n" dir; + flush stderr + let safe_assoc from verbose file k = if verbose && StrListMap.mem k !clash_v then warning_clash file k; match search_v_known ?from k with @@ -460,7 +445,7 @@ let mL_dependencies () = let efullname = escape fullname in printf "%s_MLLIB_DEPENDENCIES:=%s\n" efullname dep; printf "%s.cma:$(addsuffix .cmo,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname; - printf "%s.cmxa %s.cmxs:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname efullname; + printf "%s.cmxa:$(addsuffix .cmx,$(%s_MLLIB_DEPENDENCIES))\n" efullname efullname; flush stdout) (List.rev !mllibAccu); List.iter @@ -470,7 +455,7 @@ let mL_dependencies () = let efullname = escape fullname in printf "%s_MLPACK_DEPENDENCIES:=%s\n" efullname dep; printf "%s.cmo:$(addsuffix .cmo,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname; - printf "%s.cmx %s.cmxs:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname efullname; + printf "%s.cmx:$(addsuffix .cmx,$(%s_MLPACK_DEPENDENCIES))\n" efullname efullname; flush stdout) (List.rev !mlpackAccu) @@ -504,15 +489,15 @@ let add_caml_known phys_dir _ f = | _ -> () let add_coqlib_known recur phys_dir log_dir f = - match get_extension f [".vo"] with - | (basename,".vo") -> + match get_extension f [".vo"; ".vio"] with + | (basename, (".vo" | ".vio")) -> 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"] with + match get_extension f [".v"; ".vo"; ".vio"] with | (basename,".v") -> let name = log_dir@[basename] in let file = phys_dir//basename in @@ -521,37 +506,30 @@ let add_known recur phys_dir log_dir f = 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") when not(!option_boot) -> + | (basename, (".vo" | ".vio")) 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 | _ -> () -(** Visit directory [phys_dir] (recursively unless [recur=false]) and - apply function add_file to each regular file encountered. - [log_dir] is the logical name of the [phys_dir]. - [add_file] takes both directory names and the file. *) +(* Visits all the directories under [dir], including [dir] *) + +let is_not_seen_directory phys_f = + not (StrSet.mem phys_f !norec_dirs) + let rec add_directory recur add_file phys_dir log_dir = - let dirh = opendir phys_dir in register_dir_logpath phys_dir log_dir; - try - while true do - let f = readdir dirh in - (* we avoid all files and subdirs starting by '.' (e.g. .svn), - plus CVS and _darcs and any subdirs given via -exclude-dirs *) - if f.[0] <> '.' then - let phys_f = if phys_dir = "." then f else phys_dir//f in - match try (stat phys_f).st_kind with _ -> S_BLK with - | S_DIR when recur -> - if StrSet.mem f !norec_dirnames then () - else - if StrSet.mem phys_f !norec_dirs then () - else (* TODO: warn if already seen this physycal dir? *) - add_directory recur add_file phys_f (log_dir@[f]) - | S_REG -> add_file phys_dir log_dir f - | _ -> () - done - with End_of_file -> closedir dirh + let f = function + | FileDir (phys_f,f) -> + if is_not_seen_directory phys_f && recur then + add_directory true add_file phys_f (log_dir @ [f]) + | FileRegular f -> + add_file phys_dir log_dir f + in + if exists_dir phys_dir then + process_directory f phys_dir + else + warning_cannot_open_dir phys_dir (** Simply add this directory and imports it, no subdirs. This is used by the implicit adding of the current path (which is not recursive). *) @@ -564,12 +542,18 @@ let add_rec_dir_no_import add_file phys_dir log_dir = (** -R semantic: go in subdirs and suffixes of logical paths are known. *) let add_rec_dir_import add_file phys_dir log_dir = - handle_unix_error (add_directory true (add_file true) phys_dir) log_dir + add_directory true (add_file true) phys_dir log_dir + +(** -R semantic but only on immediate capitalized subdirs *) + +let add_rec_uppercase_subdirs add_file phys_dir log_dir = + process_subdirectories (fun phys_dir f -> + add_directory true (add_file true) phys_dir (log_dir@[String.capitalize f])) + phys_dir (** -I semantic: do not go in subdirs. *) let add_caml_dir phys_dir = - handle_unix_error (add_directory false add_caml_known phys_dir) [] - + add_directory false add_caml_known phys_dir [] let rec treat_file old_dirname old_name = let name = Filename.basename old_name @@ -584,15 +568,12 @@ let rec treat_file old_dirname old_name = match try (stat complete_name).st_kind with _ -> S_BLK with | S_DIR -> (if name.[0] <> '.' then - let dir=opendir complete_name in let newdirname = match dirname with | None -> name | Some d -> d//name in - try - while true do treat_file (Some newdirname) (readdir dir) done - with End_of_file -> closedir dir) + Array.iter (treat_file (Some newdirname)) (Sys.readdir complete_name)) | S_REG -> (match get_extension name [".v";".ml";".mli";".ml4";".mllib";".mlpack"] with | (base,".v") -> -- cgit v1.2.3