diff options
| -rw-r--r-- | CHANGES | 6 | ||||
| -rw-r--r-- | lib/coqProject_file.ml4 | 87 | ||||
| -rw-r--r-- | lib/coqProject_file.mli | 42 | ||||
| -rw-r--r-- | man/coqdep.1 | 3 | ||||
| -rw-r--r-- | tools/CoqMakefile.in | 9 | ||||
| -rw-r--r-- | tools/coq_makefile.ml | 71 | ||||
| -rw-r--r-- | tools/coqdep.ml | 19 |
7 files changed, 157 insertions, 80 deletions
@@ -109,6 +109,12 @@ CoqIDE - Find and Replace All report the number of occurrences found; Find indicates when it wraps. +coqdep + +- Learned to read -I, -Q, -R and filenames from _CoqProject files. + This is used by coq_makefile when generating dependencies for .v + files (but not other files). + Documentation - The Coq FAQ, formerly located at https://coq.inria.fr/faq, has been diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4 index 40945939f..d6c340f69 100644 --- a/lib/coqProject_file.ml4 +++ b/lib/coqProject_file.ml4 @@ -8,27 +8,32 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +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; + 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; @@ -114,6 +119,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 @@ -143,17 +149,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 @@ -178,20 +184,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" -> { proj with v_files = proj.v_files @ [f] } - | ".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] } + | ".v" -> + { 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 @@ -215,16 +222,34 @@ 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 } = - 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 5a4dd3659..5780bb5d7 100644 --- a/lib/coqProject_file.mli +++ b/lib/coqProject_file.mli @@ -10,29 +10,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; - + extra_targets : extra_target sourced list; + subdirs : string sourced list; } and extra_target = { target : string; @@ -52,3 +55,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/man/coqdep.1 b/man/coqdep.1 index ed727db7c..c417402c2 100644 --- a/man/coqdep.1 +++ b/man/coqdep.1 @@ -80,6 +80,9 @@ Prints the dependencies of Caml modules. \" of each Coq file given as argument and complete (if needed) \" the list of Caml modules. The new command is printed on \" the standard output. No dependency is computed with this option. +.TP +.BI \-f \ file +Read filenames and options -I, -R and -Q from a _CoqProject FILE. .TP .BI \-I/\-Q/\-R \ options Have the same effects on load path and modules names as for other 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 |