diff options
Diffstat (limited to 'tools/coqdep.ml')
| -rw-r--r-- | tools/coqdep.ml | 63 |
1 files changed, 46 insertions, 17 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml index a7c32e1d..12b5cab0 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Printf @@ -320,19 +322,25 @@ let treat_coq_file chan = List.fold_left (fun accu v -> mark_v_done from accu v) acc strl | Declare sl -> let declare suff dir s = - let base = file_name s dir in - let opt = if !option_natdynlk then " " ^ base ^ ".cmxs" else "" in - (escape base, suff ^ opt) + let base = escape (file_name s dir) in + match !option_dynlink with + | No -> [] + | Byte -> [base,suff] + | Opt -> [base,".cmxs"] + | Both -> [base,suff; base,".cmxs"] + | Variable -> + if suff=".cmo" then [base,"$(DYNOBJ)"] + else [base,"$(DYNLIB)"] in let decl acc str = let s = basename_noext str in if not (StrSet.mem s !deja_vu_ml) then let () = deja_vu_ml := StrSet.add s !deja_vu_ml in match search_mllib_known s with - | Some mldir -> (declare ".cma" mldir s) :: acc + | Some mldir -> (declare ".cma" mldir s) @ acc | None -> match search_ml_known s with - | Some mldir -> (declare ".cmo" mldir s) :: acc + | Some mldir -> (declare ".cmo" mldir s) @ acc | None -> acc else acc in @@ -435,9 +443,10 @@ let usage () = 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 " -boot : For coq developers, 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 " -f file : read -I, -Q, -R and filenames from _CoqProject-formatted FILE."; 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? *) @@ -449,10 +458,24 @@ let usage () = eprintf " -coqlib dir : set the coq standard library directory\n"; eprintf " -suffix s : \n"; eprintf " -slash : deprecated, no effect\n"; + eprintf " -dyndep (opt|byte|both|no|var) : set how dependencies over ML modules are printed\n"; exit 1 let split_period = Str.split (Str.regexp (Str.quote ".")) +let add_q_include path l = add_rec_dir_no_import add_known path (split_period l) + +let add_r_include path l = add_rec_dir_import add_known path (split_period l) + +let treat_coqproject f = + let open CoqProject_file in + let iter_sourced f = List.iter (fun {thing} -> f thing) in + let project = read_project_file f in + iter_sourced (fun { path } -> add_caml_dir path) project.ml_includes; + iter_sourced (fun ({ path }, l) -> add_q_include path l) project.q_includes; + iter_sourced (fun ({ path }, l) -> add_r_include path l) project.r_includes; + iter_sourced (fun f -> treat_file None f) (all_files project) + let rec parse = function | "-c" :: ll -> option_c := true; parse ll | "-D" :: ll -> option_D := true; parse ll @@ -460,10 +483,11 @@ 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 + | "-f" :: f :: ll -> treat_coqproject f; parse ll | "-I" :: r :: ll -> add_caml_dir r; parse ll | "-I" :: [] -> usage () - | "-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" :: r :: ln :: ll -> add_r_include r ln; parse ll + | "-Q" :: r :: ln :: ll -> add_q_include r 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,17 +500,22 @@ let rec parse = function | "-slash" :: ll -> Printf.eprintf "warning: option -slash has no effect and is deprecated.\n"; parse ll + | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll + | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll + | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll + | "-dyndep" :: "both" :: ll -> option_dynlink := Both; parse ll + | "-dyndep" :: "var" :: ll -> option_dynlink := Variable; parse ll | ("-h"|"--help"|"-help") :: _ -> usage () | f :: ll -> treat_file None f; parse ll | [] -> () let coqdep () = if Array.length Sys.argv < 2 then usage (); + if not Coq_config.has_natdynlink then option_dynlink := No; 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_import add_known "theories" ["Coq"]; @@ -495,14 +524,14 @@ let coqdep () = 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:CErrors.error; + Envars.set_coqlib ~fail:(fun msg -> CErrors.user_err Pp.(str msg)); let coqlib = Envars.coqlib () in 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_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 -> Feedback.msg_warning (Pp.str x))); + (Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (Pp.str x))); 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; @@ -526,5 +555,5 @@ let _ = try coqdep () with CErrors.UserError(s,p) -> - let pp = if s <> "_" then Pp.(str s ++ str ": " ++ p) else p in - Feedback.msg_error pp + let pp = (match s with | None -> p | Some s -> Pp.(str s ++ str ": " ++ p)) in + Format.eprintf "%a@\n%!" Pp.pp_with pp |