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. --- tools/CoqMakefile.in | 13 ++++++++++++- tools/coq_makefile.ml | 3 ++- tools/coqdep.ml | 7 +++++++ 3 files changed, 21 insertions(+), 2 deletions(-) (limited to 'tools') diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 727fd3ec3..e9ac8f55d 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 1e1862220..d495cde2f 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 ca14b11bc..4569994b4 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 -- 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 ++++++++++++--------- tools/coq_makefile.ml | 59 +++++++++++++++++---------------- tools/coqdep.ml | 2 +- 4 files changed, 102 insertions(+), 82 deletions(-) (limited to 'tools') diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4 index f1ec4b455..238e26c42 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 8702da1f4..68bc5dfe4 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 diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index d495cde2f..ae29c95f4 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -11,6 +11,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 "" @@ -173,21 +175,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" @@ -217,10 +220,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; cmdline_vfiles } + { 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)); @@ -228,7 +231,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)); - fprintf oc "COQMF_CMDLINE_VFILES = %s\n" (S.concat " " (map quote cmdline_vfiles)); + 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 @@ -245,12 +249,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"; @@ -263,9 +267,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"; @@ -283,10 +287,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 @@ -296,10 +300,11 @@ 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 @@ -310,15 +315,15 @@ let warn_install_at_root_directory 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 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 ;; @@ -327,10 +332,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 @@ -353,7 +358,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 @@ -363,10 +368,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 4569994b4..26a2b2696 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -464,7 +464,7 @@ 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 + List.iter (fun f -> treat_file None f.thing) project.v_files let rec parse = function | "-c" :: ll -> option_c := true; parse ll -- 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 ++++++ tools/CoqMakefile.in | 14 +++++--------- tools/coq_makefile.ml | 13 +++++++------ tools/coqdep.ml | 16 ++++++++++++---- 5 files changed, 38 insertions(+), 19 deletions(-) (limited to 'tools') 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 -- cgit v1.2.3