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(-) 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