diff options
| -rw-r--r-- | lib/coqProject_file.ml4 | 8 | ||||
| -rw-r--r-- | lib/coqProject_file.mli | 6 | ||||
| -rw-r--r-- | tools/CoqMakefile.in | 14 | ||||
| -rw-r--r-- | tools/coq_makefile.ml | 13 | ||||
| -rw-r--r-- | tools/coqdep.ml | 16 |
5 files changed, 38 insertions, 19 deletions
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4 index 238e26c42..aeae99b21 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 68bc5dfe4..97367b600 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 diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index e9ac8f55d..e9f64542c 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -31,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) @@ -726,18 +727,13 @@ $(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack $(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 +# 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 $(COQDEP_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 ae29c95f4..67dc60e3e 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -203,7 +203,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 = @@ -308,17 +312,14 @@ let ensure_root_dir ;; 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 {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 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"; diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 26a2b2696..1317426f6 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -444,7 +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 " -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? *) @@ -461,10 +461,18 @@ 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 - List.iter (fun f -> treat_file None f.thing) project.v_files + 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 @@ -476,8 +484,8 @@ let rec parse = function | "-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 |