Fix #6830: coqdep VDFILE uses too many arguments for fiat-crypto/OSX

We fix as suggested by @JasonGross by reading file names from the
_CoqProject when coq_makefile was invoked with one.

I made coqdep only look at the .v files from _CoqProject because it's
easier this way. Since we're going through the _CoqProject parser we
could have coqdep understand more of it but let's leave that to
another PR (and maybe someone else).

Some projects pass vfiles on the command line, we keep the list of
these files to pass them to coqdep via command line even when there is
a _CoqProject.

Multiple project files is probably broken.

3 files changed, 21 insertions, 2 deletions

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 727fd3ec3..e9ac8f55d 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -23,6 +23,7 @@ MLFILES           := $(COQMF_MLFILES)
 ML4FILES          := $(COQMF_ML4FILES)
 MLPACKFILES       := $(COQMF_MLPACKFILES)
 MLLIBFILES        := $(COQMF_MLLIBFILES)
+CMDLINE_VFILES    := $(COQMF_CMDLINE_VFILES)
 INSTALLCOQDOCROOT := $(COQMF_INSTALLCOQDOCROOT)
 OTHERFLAGS        := $(COQMF_OTHERFLAGS)
 COQ_SRC_SUBDIRS   := $(COQMF_COQ_SRC_SUBDIRS)
@@ -724,9 +725,19 @@ $(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack
 	$(SHOW)'COQDEP $<'
 	$(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
+
 $(VDFILE).d: $(VFILES)
 	$(SHOW)'COQDEP VFILES'
-	$(HIDE)$(COQDEP) $(COQLIBS) -dyndep var -c $(VFILES) $(redir_if_ok)
+	$(HIDE)$(COQDEP) $(COQLIBS) -dyndep var -c $(COQDEP_VFILES) $(redir_if_ok)
 
 # Misc ########################################################################
 
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 1e1862220..d495cde2f 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -217,7 +217,7 @@ let generate_conf_coq_config oc args =
 ;;
 
 let generate_conf_files oc
-  { v_files; mli_files; ml4_files; ml_files; mllib_files; mlpack_files }
+  { v_files; mli_files; ml4_files; ml_files; mllib_files; mlpack_files; cmdline_vfiles }
 =
   let module S = String in
   let open List in
@@ -228,6 +228,7 @@ let generate_conf_files oc
   fprintf oc "COQMF_ML4FILES = %s\n"    (S.concat " " (map quote ml4_files));
   fprintf oc "COQMF_MLPACKFILES = %s\n" (S.concat " " (map quote mlpack_files));
   fprintf oc "COQMF_MLLIBFILES = %s\n"  (S.concat " " (map quote mllib_files));
+  fprintf oc "COQMF_CMDLINE_VFILES = %s\n" (S.concat " " (map quote cmdline_vfiles));
 ;;
 
 let rec all_start_with prefix = function
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index ca14b11bc..4569994b4 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -444,6 +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 "  -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? *)
@@ -460,6 +461,11 @@ let usage () =
 
 let split_period = Str.split (Str.regexp (Str.quote "."))
 
+let treat_coqproject f =
+  let open CoqProject_file in
+  let project = read_project_file f in
+  List.iter (treat_file None) project.v_files
+
 let rec parse = function
   | "-c" :: ll -> option_c := true; parse ll
   | "-D" :: ll -> option_D := true; parse ll
@@ -467,6 +473,7 @@ 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