From 195c03f798141dc816e97def7275bbdd1aa623a2 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 28 Feb 2018 11:55:14 +0100
Subject: 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.
---
 lib/coqProject_file.ml4 | 11 ++++++++++-
 lib/coqProject_file.mli |  1 +
 2 files changed, 11 insertions(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4
index e6f1d7e063..f1ec4b4552 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 810189450f..8702da1f49 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;
-- 
cgit v1.2.3


From 7e0eeba3e91cd5da029aaa6b9c86f7a13f505b88 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 28 Feb 2018 16:39:26 +0100
Subject: Add source (project file / command line) to project fields.

---
 lib/coqProject_file.ml4 | 86 +++++++++++++++++++++++++++----------------------
 lib/coqProject_file.mli | 37 ++++++++++++---------
 2 files changed, 69 insertions(+), 54 deletions(-)

(limited to 'lib')

diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4
index f1ec4b4552..238e26c429 100644
--- a/lib/coqProject_file.ml4
+++ b/lib/coqProject_file.ml4
@@ -6,29 +6,32 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+type arg_source = CmdLine | ProjectFile
+
+type 'a sourced = { thing : 'a; source : arg_source }
+
 type project = {
   project_file  : string option;
   makefile : string option;
   install_kind  : install option;
   use_ocamlopt : bool;
 
-  v_files : string list;
-  mli_files : string list;
-  ml4_files : string list;
-  ml_files : string list;
-  mllib_files : string list;
-  mlpack_files : string list;
-
-  ml_includes : path list;
-  r_includes  : (path * logic_path) list;
-  q_includes  : (path * logic_path) list;
-  extra_args : string list;
-  defs : (string * string) list;
-  
-  extra_targets : extra_target list;
-  subdirs : string list;
-
-  cmdline_vfiles : string list;
+  v_files : string sourced list;
+  mli_files : string sourced list;
+  ml4_files : string sourced list;
+  ml_files : string sourced list;
+  mllib_files : string sourced list;
+  mlpack_files : string sourced list;
+
+  ml_includes : path sourced list;
+  r_includes  : (path * logic_path) sourced list;
+  q_includes  : (path * logic_path) sourced list;
+  extra_args : string sourced list;
+  defs : (string * string) sourced list;
+
+  (* deprecated in favor of a Makefile.local using :: rules *)
+  extra_targets : extra_target sourced list;
+  subdirs : string sourced list;
 }
 and extra_target = {
   target : string;
@@ -63,7 +66,6 @@ let mk_project project_file makefile install_kind use_ocamlopt = {
   q_includes = [];
   extra_args = [];
   defs = [];
-  cmdline_vfiles = [];
 }
 
 (********************* utils ********************************************)
@@ -115,6 +117,7 @@ let exists_dir dir =
 
 let process_cmd_line orig_dir proj args =
   let parsing_project_file = ref (proj.project_file <> None) in
+  let sourced x = { thing = x; source = if !parsing_project_file then ProjectFile else CmdLine } in
   let orig_dir = (* avoids turning foo.v in ./foo.v *)
     if orig_dir = "." then "" else orig_dir in
   let error s = Format.eprintf "@[%a]@@\n%!" Pp.pp_with Pp.(str (s^".")); exit 1 in
@@ -144,17 +147,17 @@ let process_cmd_line orig_dir proj args =
     aux { proj with install_kind = Some install } r
   | "-extra" :: target :: dependencies :: command :: r ->
     let tgt = { target; dependencies; phony = false; command } in
-    aux { proj with extra_targets = proj.extra_targets @ [tgt] } r
+    aux { proj with extra_targets = proj.extra_targets @ [sourced tgt] } r
   | "-extra-phony" :: target :: dependencies :: command :: r ->
     let tgt = { target; dependencies; phony = true; command } in
-    aux { proj with extra_targets = proj.extra_targets @ [tgt] } r
+    aux { proj with extra_targets = proj.extra_targets @ [sourced tgt] } r
 
   | "-Q" :: d :: lp :: r ->
-    aux { proj with q_includes = proj.q_includes @ [mk_path d,lp] } r
+    aux { proj with q_includes = proj.q_includes @ [sourced (mk_path d,lp)] } r
   | "-I" :: d :: r ->
-    aux { proj with ml_includes = proj.ml_includes @ [mk_path d] } r
+    aux { proj with ml_includes = proj.ml_includes @ [sourced (mk_path d)] } r
   | "-R" :: d :: lp :: r ->
-    aux { proj with r_includes = proj.r_includes @ [mk_path d,lp] } r
+    aux { proj with r_includes = proj.r_includes @ [sourced (mk_path d,lp)] } r
 
   | "-f" :: file :: r ->
     if !parsing_project_file then
@@ -179,26 +182,21 @@ let process_cmd_line orig_dir proj args =
       error "Option -o given more than once";
     aux { proj with makefile = Some file } r  
   | v :: "=" :: def :: r ->
-    aux { proj with defs = proj.defs @ [v,def] } r
+    aux { proj with defs = proj.defs @ [sourced (v,def)] } r
   | "-arg" :: a :: r ->
-    aux { proj with extra_args = proj.extra_args @ [a] } r
+    aux { proj with extra_args = proj.extra_args @ [sourced a] } r
   | f :: r ->
       let f = CUnix.correct_path f orig_dir in
       let proj =
-        if exists_dir f then { proj with subdirs = proj.subdirs @ [f] }
+        if exists_dir f then { proj with subdirs = proj.subdirs @ [sourced f] }
         else match CUnix.get_extension f with
           | ".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] }
-        | ".mllib" -> { proj with mllib_files = proj.mllib_files @ [f] }
-        | ".mlpack" -> { proj with mlpack_files = proj.mlpack_files @ [f] }
+            { proj with v_files = proj.v_files @ [sourced f] }
+        | ".ml" -> { proj with ml_files = proj.ml_files @ [sourced f] }
+        | ".ml4" -> { proj with ml4_files = proj.ml4_files @ [sourced f] }
+        | ".mli" -> { proj with mli_files = proj.mli_files @ [sourced f] }
+        | ".mllib" -> { proj with mllib_files = proj.mllib_files @ [sourced f] }
+        | ".mlpack" -> { proj with mlpack_files = proj.mlpack_files @ [sourced f] }
         | _ -> raise (Parsing_error ("Unknown option "^f)) in
       aux proj r
  in
@@ -222,16 +220,26 @@ let rec find_project_file ~from ~projfile_name =
     else find_project_file ~from:newdir ~projfile_name
 ;;
 
+let map_sourced_list f l = List.map (fun x -> f x.thing) l
+;;
+
 let coqtop_args_from_project
   { ml_includes; r_includes; q_includes; extra_args }
 =
-  let map = List.map in
+  let map = map_sourced_list  in
   let args =
     map (fun { canonical_path = i } -> ["-I"; i]) ml_includes @
     map (fun ({ canonical_path = i }, l) -> ["-Q"; i; l]) q_includes @
     map (fun ({ canonical_path = p }, l) -> ["-R"; p; l]) r_includes @
-    [extra_args] in
+    [map (fun x -> x) extra_args] in
   List.flatten args
 ;;
 
+let filter_cmdline l = CList.map_filter
+    (function {thing; source=CmdLine} -> Some thing | {source=ProjectFile} -> None)
+    l
+;;
+
+let forget_source {thing} = thing
+
 (* vim:set ft=ocaml: *)
diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli
index 8702da1f49..68bc5dfe4d 100644
--- a/lib/coqProject_file.mli
+++ b/lib/coqProject_file.mli
@@ -8,30 +8,32 @@
 
 exception Parsing_error of string
 
+type arg_source = CmdLine | ProjectFile
+
+type 'a sourced = { thing : 'a; source : arg_source }
+
 type project = {
   project_file  : string option;
   makefile : string option;
   install_kind  : install option;
   use_ocamlopt : bool;
 
-  v_files : string list;
-  mli_files : string list;
-  ml4_files : string list;
-  ml_files : string list;
-  mllib_files : string list;
-  mlpack_files : string list;
+  v_files : string sourced list;
+  mli_files : string sourced list;
+  ml4_files : string sourced list;
+  ml_files : string sourced list;
+  mllib_files : string sourced list;
+  mlpack_files : string sourced list;
 
-  ml_includes : path list;
-  r_includes  : (path * logic_path) list;
-  q_includes  : (path * logic_path) list;
-  extra_args : string list;
-  defs : (string * string) list;
+  ml_includes : path sourced list;
+  r_includes  : (path * logic_path) sourced list;
+  q_includes  : (path * logic_path) sourced list;
+  extra_args : string sourced list;
+  defs : (string * string) sourced list;
 
   (* deprecated in favor of a Makefile.local using :: rules *)
-  extra_targets : extra_target list;
-  subdirs : string list;
-
-  cmdline_vfiles : string list; (** The subset of [v_files] not from the [project_file].*)
+  extra_targets : extra_target sourced list;
+  subdirs : string sourced list;
 }
 and extra_target = {
   target : string;
@@ -51,3 +53,8 @@ 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 map_sourced_list : ('a -> 'b) -> 'a sourced list -> 'b list
+
+val filter_cmdline : 'a sourced list -> 'a list
+
+val forget_source : 'a sourced -> 'a
-- 
cgit v1.2.3


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.
---
 lib/coqProject_file.ml4 | 8 ++++++++
 lib/coqProject_file.mli | 6 ++++++
 2 files changed, 14 insertions(+)

(limited to 'lib')

diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4
index 238e26c429..aeae99b21b 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 68bc5dfe4d..97367b6000 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
-- 
cgit v1.2.3