Closes #6830: coqdep reads options and files from _CoqProject.

Note that we don't look inside -arg for eg -coqlib.

5 files changed, 38 insertions, 19 deletions

diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4
index 238e26c42..aeae99b21 100644
--- a/lib/coqProject_file.ml4
+++ b/lib/coqProject_file.ml4
@@ -220,9 +220,17 @@ let rec find_project_file ~from ~projfile_name =
     else find_project_file ~from:newdir ~projfile_name
 ;;
 
+let all_files { v_files; ml_files; mli_files; ml4_files;
+                mllib_files; mlpack_files } =
+  v_files @ mli_files @ ml4_files @ ml_files @ mllib_files @ mlpack_files
+
 let map_sourced_list f l = List.map (fun x -> f x.thing) l
 ;;
 
+let map_cmdline f l = CList.map_filter (function
+    | {thing=x; source=CmdLine} -> Some (f x)
+    | {source=ProjectFile} -> None) l
+
 let coqtop_args_from_project
   { ml_includes; r_includes; q_includes; extra_args }
 =
diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli
index 68bc5dfe4..97367b600 100644
--- a/lib/coqProject_file.mli
+++ b/lib/coqProject_file.mli
@@ -53,8 +53,14 @@ val read_project_file : string -> project
 val coqtop_args_from_project : project -> string list
 val find_project_file : from:string -> projfile_name:string -> string option
 
+val all_files : project -> string sourced list
+
 val map_sourced_list : ('a -> 'b) -> 'a sourced list -> 'b list
 
+(** Only uses the elements with source=CmdLine *)
+val map_cmdline : ('a -> 'b) -> 'a sourced list -> 'b list
+
+(** Only uses the elements with source=CmdLine *)
 val filter_cmdline : 'a sourced list -> 'a list
 
 val forget_source : 'a sourced -> 'a
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