diff options
| -rw-r--r-- | lib/coqProject_file.ml4 | 11 | ||||
| -rw-r--r-- | lib/coqProject_file.mli | 1 | ||||
| -rw-r--r-- | tools/CoqMakefile.in | 13 | ||||
| -rw-r--r-- | tools/coq_makefile.ml | 3 | ||||
| -rw-r--r-- | tools/coqdep.ml | 7 |
5 files changed, 32 insertions, 3 deletions
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; diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 727fd3ec37..e9ac8f55d8 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 1e1862220b..d495cde2fb 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 ca14b11bc1..4569994b42 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 |