diff options
| -rw-r--r-- | tools/coqdep.ml | 25 | ||||
| -rw-r--r-- | tools/coqdep_boot.ml | 13 | ||||
| -rw-r--r-- | tools/coqdep_common.ml | 34 | ||||
| -rw-r--r-- | tools/coqdep_common.mli | 9 |
4 files changed, 55 insertions, 26 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml index febde9b69..a44f159b4 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -36,11 +36,11 @@ let warning_mult suf iter = in iter check -let add_coqlib_known phys_dir log_dir f = +let add_coqlib_known recur phys_dir log_dir f = match get_extension f [".vo"] with | (basename,".vo") -> let name = log_dir@[basename] in - let paths = suffixes name in + let paths = if recur then suffixes name else [name] in List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths | _ -> () @@ -445,16 +445,19 @@ let rec parse = function | "-c" :: ll -> option_c := true; parse ll | "-D" :: ll -> option_D := true; parse ll | "-w" :: ll -> option_w := true; parse ll - | "-boot" :: ll -> Flags.boot := true; parse ll + | "-boot" :: ll -> option_boot := true; parse ll | "-sort" :: ll -> option_sort := true; parse ll | ("-noglob" | "-no-glob") :: ll -> option_noglob := true; parse ll - | "-I" :: r :: "-as" :: ln :: ll -> add_dir add_known r (split_period ln); parse ll + | "-I" :: r :: "-as" :: ln :: ll -> add_dir add_known r []; + add_dir add_known r (split_period ln); + parse ll | "-I" :: r :: "-as" :: [] -> usage () - | "-I" :: r :: ll -> add_dir add_known r []; parse ll + | "-I" :: r :: ll -> add_caml_dir r; parse ll | "-I" :: [] -> usage () | "-R" :: r :: "-as" :: ln :: ll -> add_rec_dir add_known r (split_period ln); parse ll | "-R" :: r :: "-as" :: [] -> usage () | "-R" :: r :: ln :: ll -> add_rec_dir add_known r (split_period ln); parse ll + | "-Q" :: r :: ln :: ll -> add_dir add_known r (split_period ln); parse ll | "-R" :: ([] | [_]) -> usage () | "-dumpgraph" :: f :: ll -> option_dump := Some (false, f); parse ll | "-dumpgraphbox" :: f :: ll -> option_dump := Some (true, f); parse ll @@ -476,19 +479,21 @@ let coqdep () = parse (List.tl (Array.to_list Sys.argv)); if not Coq_config.has_natdynlink then option_natdynlk := false; (* NOTE: These directories are searched from last to first *) - if !Flags.boot then begin + if !option_boot then begin add_rec_dir add_known "theories" ["Coq"]; - add_rec_dir add_known "plugins" ["Coq"] + add_rec_dir add_known "plugins" ["Coq"]; + add_rec_dir (fun _ -> add_caml_known) "theories" ["Coq"]; + add_rec_dir (fun _ -> add_caml_known) "plugins" ["Coq"]; end else begin Envars.set_coqlib ~fail:Errors.error; let coqlib = Envars.coqlib () in add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"]; add_rec_dir add_coqlib_known (coqlib//"plugins") ["Coq"]; let user = coqlib//"user-contrib" in - if Sys.file_exists user then add_rec_dir add_coqlib_known user []; - List.iter (fun s -> add_rec_dir add_coqlib_known s []) + if Sys.file_exists user then add_dir add_coqlib_known user []; + List.iter (fun s -> add_dir add_coqlib_known s []) (Envars.xdg_dirs (fun x -> Pp.msg_warning (Pp.str x))); - List.iter (fun s -> add_rec_dir add_coqlib_known s []) Envars.coqpath; + List.iter (fun s -> add_dir add_coqlib_known s []) Envars.coqpath; end; List.iter (fun (f,d) -> add_mli_known f d) !mliAccu; List.iter (fun (f,d) -> add_mllib_known f d) !mllibAccu; diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml index f42c8dc75..a80a713ed 100644 --- a/tools/coqdep_boot.ml +++ b/tools/coqdep_boot.ml @@ -24,21 +24,26 @@ let rec parse = function | "-I" :: r :: ll -> (* To solve conflict (e.g. same filename in kernel and checker) we allow to state an explicit order *) - add_dir add_known r []; + add_caml_dir r; norec_dirs:=r::!norec_dirs; parse ll | f :: ll -> treat_file None f; parse ll | [] -> () let coqdep_boot () = + let () = option_boot := true in if Array.length Sys.argv < 2 then exit 1; parse (List.tl (Array.to_list Sys.argv)); - if !option_c then - add_rec_dir add_known "." [] + if !option_c then begin + add_rec_dir add_known "." []; + add_rec_dir (fun _ -> add_caml_known) "." ["Coq"]; + end else begin add_rec_dir add_known "theories" ["Coq"]; add_rec_dir add_known "plugins" ["Coq"]; - add_dir add_known "tactics" []; + add_caml_dir "tactics"; + add_rec_dir (fun _ -> add_caml_known) "theories" ["Coq"]; + add_rec_dir (fun _ -> add_caml_known) "plugins" ["Coq"]; end; if !option_c then mL_dependencies (); coq_dependencies () diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 1845351cd..c965fb098 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -23,6 +23,7 @@ let stdout = Pervasives.stdout let option_c = ref false let option_noglob = ref false let option_natdynlk = ref true +let option_boot = ref false let option_mldep = ref None let norec_dirs = ref ([] : string list) @@ -426,18 +427,26 @@ 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 = + match get_extension f [".ml";".mli";".ml4";".mllib";".mlpack"] with + | (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) + | _ -> () + +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) + | (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], @@ -464,11 +473,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 diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 3e4ffe500..3c1cd4fbe 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -8,6 +8,7 @@ val option_c : bool ref val option_noglob : bool ref +val option_boot : bool ref val option_natdynlk : bool ref val option_mldep : string option ref val norec_dirs : string list ref @@ -38,13 +39,15 @@ val canonize : string -> string val mL_dependencies : unit -> unit val coq_dependencies : unit -> unit val suffixes : 'a list -> 'a list list -val add_known : string -> string list -> string -> unit +val add_known : bool -> string -> string list -> string -> unit +val add_caml_known : string -> string list -> string -> unit val add_directory : bool -> (string -> string list -> string -> unit) -> string -> string list -> unit +val add_caml_dir : string -> unit val add_dir : - (string -> string list -> string -> unit) -> string -> string list -> unit + (bool -> string -> string list -> string -> unit) -> string -> string list -> unit val add_rec_dir : - (string -> string list -> string -> unit) -> string -> string list -> unit + (bool -> string -> string list -> string -> unit) -> string -> string list -> unit val treat_file : dir -> string -> unit val error_cannot_parse : string -> int * int -> 'a |