From ed98716036e9d47efb2ba66cf0336fc45e03f793 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 1 Mar 2018 13:48:47 +0100 Subject: Closes #6830: coqdep reads options and files from _CoqProject. Note that we don't look inside -arg for eg -coqlib. --- tools/CoqMakefile.in | 14 +++++--------- tools/coq_makefile.ml | 13 +++++++------ tools/coqdep.ml | 16 ++++++++++++---- 3 files changed, 24 insertions(+), 19 deletions(-) (limited to 'tools') diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index e9ac8f55d..e9f64542c 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -31,6 +31,7 @@ OCAMLLIBS := $(COQMF_OCAMLLIBS) SRC_SUBDIRS := $(COQMF_SRC_SUBDIRS) COQLIBS := $(COQMF_COQLIBS) COQLIBS_NOML := $(COQMF_COQLIBS_NOML) +CMDLINE_COQLIBS := $(COQMF_CMDLINE_COQLIBS) LOCAL := $(COQMF_LOCAL) COQLIB := $(COQMF_COQLIB) DOCDIR := $(COQMF_DOCDIR) @@ -726,18 +727,13 @@ $(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok) # If this makefile is created using a _CoqProject we have coqdep get -# the list of files from it. This avoids argument length limits for -# pathological projects. Note that extra files might be on the command -# line. -ifeq (,@PROJECT_FILE@) -COQDEP_VFILES:=$(CMDLINE_VFILES) -else -COQDEP_VFILES:=-f @PROJECT_FILE@ $(CMDLINE_VFILES) -endif +# options from it. This avoids argument length limits for pathological +# projects. Note that extra options might be on the command line. +VDFILE_FLAGS:=$(if @PROJECT_FILE@,-f @PROJECT_FILE@,) $(CMDLINE_COQLIBS) $(CMDLINE_VFILES) $(VDFILE).d: $(VFILES) $(SHOW)'COQDEP VFILES' - $(HIDE)$(COQDEP) $(COQLIBS) -dyndep var -c $(COQDEP_VFILES) $(redir_if_ok) + $(HIDE)$(COQDEP) -dyndep var $(VDFILE_FLAGS) $(redir_if_ok) # Misc ######################################################################## diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index ae29c95f4..67dc60e3e 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -203,7 +203,11 @@ let generate_conf_includes oc { ml_includes; r_includes; q_includes } = (S.concat " " (map (fun ({ path },l) -> dash2 "R" path l) r_includes)); fprintf oc "COQMF_COQLIBS_NOML = %s %s\n" (S.concat " " (map (fun ({ path },l) -> dash2 "Q" path l) q_includes)) - (S.concat " " (map (fun ({ path },l) -> dash2 "R" path l) r_includes)) + (S.concat " " (map (fun ({ path },l) -> dash2 "R" path l) r_includes)); + fprintf oc "COQMF_CMDLINE_COQLIBS = %s %s %s\n" + (S.concat " " (map_cmdline (fun { path } -> dash1 "I" path) ml_includes)) + (S.concat " " (map_cmdline (fun ({ path },l) -> dash2 "Q" path l) q_includes)) + (S.concat " " (map_cmdline (fun ({ path },l) -> dash2 "R" path l) r_includes)); ;; let windrive s = @@ -308,17 +312,14 @@ let ensure_root_dir ;; let warn_install_at_root_directory - { q_includes; r_includes; - v_files; ml_files; mli_files; ml4_files; - mllib_files; mlpack_files } + ({ q_includes; r_includes; } as project) = let open CList in let inc_top_p = map_filter (fun {thing=({ path } ,ldir)} -> if ldir = "" then Some path else None) (r_includes @ q_includes) in - let files = - v_files @ mli_files @ ml4_files @ ml_files @ mllib_files @ mlpack_files in + let files = all_files project in let bad = filter (fun f -> mem (Filename.dirname f.thing) inc_top_p) files in if bad <> [] then begin eprintf "Warning: No file should be installed at the root of Coq's library.\n"; diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 26a2b2696..1317426f6 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -444,7 +444,7 @@ let usage () = 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 : use filenames found in the _CoqProject file FILE .v files only, options and other files are ignored)"; + 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? *) @@ -461,10 +461,18 @@ let usage () = 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 - List.iter (fun f -> treat_file None f.thing) project.v_files + 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 @@ -476,8 +484,8 @@ let rec parse = function | "-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 -- cgit v1.2.3