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.

2 files changed, 11 insertions, 1 deletions

diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4
index e6f1d7e06..f1ec4b455 100644
--- a/lib/coqProject_file.ml4
+++ b/lib/coqProject_file.ml4
@@ -27,6 +27,8 @@ type project = {
   
   extra_targets : extra_target list;
   subdirs : string list;
+
+  cmdline_vfiles : string list;
 }
 and extra_target = {
   target : string;
@@ -61,6 +63,7 @@ let mk_project project_file makefile install_kind use_ocamlopt = {
   q_includes = [];
   extra_args = [];
   defs = [];
+  cmdline_vfiles = [];
 }
 
 (********************* utils ********************************************)
@@ -184,7 +187,13 @@ let process_cmd_line orig_dir proj args =
       let proj =
         if exists_dir f then { proj with subdirs = proj.subdirs @ [f] }
         else match CUnix.get_extension f with
-        | ".v" -> { proj with v_files = proj.v_files @ [f] }
+          | ".v" ->
+            let { cmdline_vfiles } = proj in
+            let cmdline_vfiles = if !parsing_project_file
+              then cmdline_vfiles
+              else cmdline_vfiles @ [f]
+            in
+            { proj with v_files = proj.v_files @ [f]; cmdline_vfiles }
         | ".ml" -> { proj with ml_files = proj.ml_files @ [f] }
         | ".ml4" -> { proj with ml4_files = proj.ml4_files @ [f] }
         | ".mli" -> { proj with mli_files = proj.mli_files @ [f] }
diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli
index 810189450..8702da1f4 100644
--- a/lib/coqProject_file.mli
+++ b/lib/coqProject_file.mli
@@ -31,6 +31,7 @@ type project = {
   extra_targets : extra_target list;
   subdirs : string list;
 
+  cmdline_vfiles : string list; (** The subset of [v_files] not from the [project_file].*)
 }
 and extra_target = {
   target : string;