diff options
Diffstat (limited to 'tools/coqdep.ml')
| -rw-r--r-- | tools/coqdep.ml | 61 |
1 files changed, 41 insertions, 20 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 110d3060..79662a5d 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -426,11 +426,28 @@ let coq_dependencies_dump chan dumpboxes = end let usage () = - eprintf " usage: coqdep [-w] [-c] [-D] [-I dir] [-R dir coqdir] <filename>+\n"; - eprintf " extra options:\n"; - eprintf " -coqlib dir : set the coq standard library directory\n"; - eprintf " -exclude-dir f : skip subdirectories named 'f' during -R search\n"; + eprintf " usage: coqdep [options] <filename>+\n"; + eprintf " options:\n"; + eprintf " -c : Also print the dependencies of caml modules (=ocamldep).\n"; + (* Does not work anymore *) + (* eprintf " -w : Print informations on missing or wrong \"Declare + ML Module\" commands in coq files.\n"; *) + (* Does not work anymore: *) + (* eprintf " -D : Prints the missing ocmal module names. No dependency computed.\n"; *) + eprintf " -boot : For coq developpers, prints dependencies over coq library files (omitted by default).\n"; + eprintf " -sort : output the given file name ordered by dependencies\n"; + eprintf " -noglob | -no-glob : \n"; + eprintf " -I dir -as logname : add (non recursively) dir to coq load path under logical name logname\n"; + eprintf " -I dir : add (non recursively) dir to ocaml path\n"; + eprintf " -R dir -as logname : add and import dir recursively to coq load path under logical name logname\n"; (* deprecate? *) + eprintf " -R dir logname : add and import dir recursively to coq load path under logical name logname\n"; + eprintf " -Q dir logname : add (recusively) and open (non recursively) dir to coq load path under logical name logname\n"; eprintf " -dumpgraph f : print a dot dependency graph in file 'f'\n"; + eprintf " -dumpgraphbox f : print a dot dependency graph box in file 'f'\n"; + eprintf " -exclude-dir dir : skip subdirectories named 'dir' during -R/-Q search\n"; + eprintf " -coqlib dir : set the coq standard library directory\n"; + eprintf " -suffix s : \n"; + eprintf " -slash : deprecated, no effect\n"; exit 1 let split_period = Str.split (Str.regexp (Str.quote ".")) @@ -442,16 +459,17 @@ let rec parse = function | "-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 []; - add_dir add_known r (split_period ln); - parse ll + | "-I" :: r :: "-as" :: ln :: ll -> + add_rec_dir_no_import add_known r []; + add_rec_dir_no_import add_known r (split_period ln); + parse ll | "-I" :: r :: "-as" :: [] -> usage () | "-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" :: ln :: ll -> add_rec_dir_import 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" :: r :: ln :: ll -> add_rec_dir_import add_known r (split_period ln); parse ll + | "-Q" :: r :: ln :: ll -> add_rec_dir_no_import 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 @@ -471,23 +489,26 @@ let rec parse = function let coqdep () = if Array.length Sys.argv < 2 then usage (); parse (List.tl (Array.to_list Sys.argv)); + (* Add current dir with empty logical path if not set by options above. *) + (try ignore (Coqdep_common.find_dir_logpath (Sys.getcwd())) + with Not_found -> add_norec_dir_import add_known "." []); if not Coq_config.has_natdynlink then option_natdynlk := false; (* NOTE: These directories are searched from last to first *) if !option_boot then begin - add_rec_dir add_known "theories" ["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"]; + add_rec_dir_import add_known "theories" ["Coq"]; + add_rec_dir_import add_known "plugins" ["Coq"]; + add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"]; + add_rec_dir_import (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"]; + add_rec_dir_import add_coqlib_known (coqlib//"theories") ["Coq"]; + add_rec_dir_import add_coqlib_known (coqlib//"plugins") ["Coq"]; let user = coqlib//"user-contrib" in - if Sys.file_exists user then add_dir add_coqlib_known user []; - List.iter (fun s -> add_dir add_coqlib_known s []) + if Sys.file_exists user then add_rec_dir_no_import add_coqlib_known user []; + List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) (Envars.xdg_dirs (fun x -> Pp.msg_warning (Pp.str x))); - List.iter (fun s -> add_dir add_coqlib_known s []) Envars.coqpath; + List.iter (fun s -> add_rec_dir_no_import add_coqlib_known s []) Envars.coqpath; end; List.iter (fun (f,d) -> add_mli_known f d ".mli") !mliAccu; List.iter (fun (f,d) -> add_mllib_known f d ".mllib") !mllibAccu; |