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

3 files changed, 64 insertions, 35 deletions

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 727fd3ec3..e9f64542c 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)
@@ -30,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)
@@ -724,9 +726,14 @@ $(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
+# 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 $(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 ef4428755..6cd520d60 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -13,6 +13,8 @@
 open CoqProject_file
 open Printf
 
+let (>) f g = fun x -> g (f x)
+
 let output_channel = ref stdout
 let makefile_name = ref "Makefile"
 let make_name = ref ""
@@ -175,21 +177,22 @@ let generate_conf_extra_target oc sps =
   in
     if sps <> [] then
       section oc "Extra targets. (-extra and -extra-phony, DEPRECATED)";
-    List.iter pr_path sps
+    List.iter (forget_source > pr_path) sps
 
 let generate_conf_subdirs oc sds =
   if sds <> [] then section oc "Subdirectories. (DEPRECATED)";
-  List.iter (fprintf oc ".PHONY:%s\n") sds;
-  List.iter (fprintf oc "post-all::\n\tcd \"%s\" && $(MAKE) all\n") sds;
-  List.iter (fprintf oc "clean::\n\tcd \"%s\" && $(MAKE) clean\n") sds;
-  List.iter (fprintf oc "archclean::\n\tcd \"%s\" && $(MAKE) archclean\n") sds;
-  List.iter (fprintf oc "install-extra::\n\tcd \"%s\" && $(MAKE) install\n") sds
+  let iter f = List.iter (forget_source > f) in
+  iter (fprintf oc ".PHONY:%s\n") sds;
+  iter (fprintf oc "post-all::\n\tcd \"%s\" && $(MAKE) all\n") sds;
+  iter (fprintf oc "clean::\n\tcd \"%s\" && $(MAKE) clean\n") sds;
+  iter (fprintf oc "archclean::\n\tcd \"%s\" && $(MAKE) archclean\n") sds;
+  iter (fprintf oc "install-extra::\n\tcd \"%s\" && $(MAKE) install\n") sds
    
 
 let generate_conf_includes oc { ml_includes; r_includes; q_includes } =
   section oc "Path directives (-I, -R, -Q).";
   let module S = String in
-  let open List in
+  let map = map_sourced_list in
   let dash1 opt v = sprintf "-%s %s" opt (quote v) in
   let dash2 opt v1 v2 = sprintf "-%s %s %s" opt (quote v1) (quote v2) in
   fprintf oc "COQMF_OCAMLLIBS = %s\n"
@@ -202,7 +205,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 =
@@ -219,10 +226,10 @@ 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; }
 =
   let module S = String in
-  let open List in
+  let map = map_sourced_list in
   section oc "Project files.";
   fprintf oc "COQMF_VFILES = %s\n"      (S.concat " " (map quote v_files));
   fprintf oc "COQMF_MLIFILES = %s\n"    (S.concat " " (map quote mli_files));
@@ -230,6 +237,8 @@ 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));
+  let cmdline_vfiles = filter_cmdline v_files in
+  fprintf oc "COQMF_CMDLINE_VFILES = %s\n" (S.concat " " (List.map quote cmdline_vfiles));
 ;;
 
 let rec all_start_with prefix = function
@@ -246,12 +255,12 @@ let rec logic_gcd acc = function
       else acc
 
 let generate_conf_doc oc { defs; q_includes; r_includes } =
-  let includes = List.map snd (q_includes @ r_includes) in
+  let includes = List.map (forget_source > snd) (q_includes @ r_includes) in
   let logpaths = List.map (CString.split '.') includes in
   let gcd = logic_gcd [] logpaths in
   let root =
     if gcd = [] then
-      if not (List.mem_assoc "INSTALLDEFAULTROOT" defs) then begin
+      if not (List.exists (fun x -> fst x.thing = "INSTALLDEFAULTROOT") defs) then begin
          let destination = "orphan_" ^ (String.concat "_" includes) in
          eprintf "Warning: no common logical root\n";
          eprintf "Warning: in such case INSTALLDEFAULTROOT must be defined\n";
@@ -264,9 +273,9 @@ let generate_conf_doc oc { defs; q_includes; r_includes } =
 
 let generate_conf_defs oc { defs; extra_args } =
   section oc "Extra variables.";
-  List.iter (fun (k,v) -> Printf.fprintf oc "%s = %s\n" k v) defs;
+  List.iter (forget_source > (fun (k,v) -> Printf.fprintf oc "%s = %s\n" k v)) defs;
   Printf.fprintf oc "COQMF_OTHERFLAGS = %s\n"
-    (String.concat " " extra_args)
+    (String.concat " " (List.map forget_source extra_args))
 
 let generate_conf oc project args  =
   fprintf oc "# This configuration file was generated by running:\n";
@@ -284,10 +293,10 @@ let ensure_root_dir
   ({ ml_includes; r_includes; q_includes;
      v_files; ml_files; mli_files; ml4_files;
      mllib_files; mlpack_files } as project)
-=
-  let open List in
+  =
+  let exists f = List.exists (forget_source > f) in
   let here = Sys.getcwd () in
-  let not_tops = List.for_all (fun s -> s <> Filename.basename s) in
+  let not_tops = List.for_all (fun s -> s.thing <> Filename.basename s.thing) in
   if exists (fun { canonical_path = x } -> x = here) ml_includes
   || exists (fun ({ canonical_path = x },_) -> is_prefix x here) r_includes
   || exists (fun ({ canonical_path = x },_) -> is_prefix x here) q_includes
@@ -297,29 +306,27 @@ let ensure_root_dir
   then
     project
   else
+    let source x = {thing=x; source=CmdLine} in
     let here_path = { path = "."; canonical_path = here } in
     { project with
-        ml_includes = here_path :: ml_includes;
-        r_includes = (here_path, "Top") :: r_includes }
+        ml_includes = source here_path :: ml_includes;
+        r_includes = source (here_path, "Top") :: r_includes }
 ;;
 
 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 ({ path } ,ldir) -> if ldir = "" then Some path else None)
+      (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 bad = filter (fun f -> mem (Filename.dirname f) inc_top_p) 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";
     eprintf "Warning: No logical path (-R, -Q) applies to these files:\n";
-    List.iter (fun x -> eprintf "Warning:  %s\n" x) bad;
+    List.iter (fun x -> eprintf "Warning:  %s\n" x.thing) bad;
     eprintf "\n";
   end
 ;;
@@ -328,10 +335,10 @@ let check_overlapping_include { q_includes; r_includes } =
   let pwd = Sys.getcwd () in
   let aux = function
     | [] -> ()
-    | ({ path; canonical_path }, _) :: l ->
+    | {thing = { path; canonical_path }, _} :: l ->
 	if not (is_prefix pwd canonical_path) then
 	  eprintf "Warning: %s (used in -R or -Q) is not a subdirectory of the current directory\n\n" path;
-	List.iter (fun ({ path = p; canonical_path = cp }, _) ->
+        List.iter (fun {thing={ path = p; canonical_path = cp }, _} ->
 	  if is_prefix canonical_path cp  || is_prefix cp canonical_path then
 	    eprintf "Warning: %s and %s overlap (used in -R or -Q)\n\n"
               path p) l
@@ -354,7 +361,7 @@ let destination_of { ml_includes; q_includes; r_includes; } file =
     clean_path (physical_dir_of_logical_dir logic ^ "/" ^
                 chop_prefix canonical_path file_dir ^ "/") in
   let candidates =
-    CList.map_filter (fun ({ canonical_path }, logic) ->
+    CList.map_filter (fun {thing={ canonical_path }, logic} ->
       if is_prefix canonical_path file_dir then
         Some(mk_destination logic canonical_path)
       else None) includes
@@ -364,10 +371,10 @@ let destination_of { ml_includes; q_includes; r_includes; } file =
      (* BACKWARD COMPATIBILITY: -I into the only logical root *)
      begin match
         r_includes,
-        List.find (fun { canonical_path = p } -> is_prefix p file_dir)
+        List.find (fun {thing={ canonical_path = p }} -> is_prefix p file_dir)
           ml_includes
      with
-        | [{ canonical_path }, logic], { canonical_path = p } ->
+        | [{thing={ canonical_path }, logic}], {thing={ canonical_path = p }} ->
             let destination =
               clean_path (physical_dir_of_logical_dir logic ^ "/" ^
                           chop_prefix p file_dir ^ "/") in
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index f4f143b3b..12b5cab0a 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -446,6 +446,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 : 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? *)
@@ -462,6 +463,19 @@ 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
+  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
   | "-D" :: ll -> option_D := true; parse ll
@@ -469,10 +483,11 @@ 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
-  | "-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