From a2257181cddf84a3b831c50398f5b13e2b79ac3a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 22 Feb 2008 22:25:27 +0000 Subject: [PATCH] - added some options to matitadep: -stdout and -exclude - LAMBDA-TYPES: improved Makefile, Base-2/theory.mma is no longer needed --- helm/software/components/library/librarian.ml | 18 +++---- .../software/components/library/librarian.mli | 2 +- .../contribs/LAMBDA-TYPES/Base-2/.depend | 1 - .../contribs/LAMBDA-TYPES/Base-2/depends | 1 - .../Base-2/{theory.mma => theory.ma} | 0 .../matita/contribs/LAMBDA-TYPES/Makefile | 26 ++++++++-- .../matita/contribs/LAMBDA-TYPES/depends | 3 +- helm/software/matita/matitaclean.ml | 8 ++- helm/software/matita/matitadep.ml | 49 +++++++++++++------ 9 files changed, 71 insertions(+), 37 deletions(-) rename helm/software/matita/contribs/LAMBDA-TYPES/Base-2/{theory.mma => theory.ma} (100%) diff --git a/helm/software/components/library/librarian.ml b/helm/software/components/library/librarian.ml index aa6b2e81d..f9831545d 100644 --- a/helm/software/components/library/librarian.ml +++ b/helm/software/components/library/librarian.ml @@ -366,15 +366,15 @@ module Make = functor (F:Format) -> struct end -let write_deps_file root deps = - let oc = open_out (root ^ "/depends") in - List.iter - (fun (t,d) -> output_string oc (t^" "^String.concat " " d^"\n")) - deps; - close_out oc; - HLog.message ("Generated: " ^ root ^ "/depends") -;; - +let write_deps_file where deps = match where with + | Some root -> + let oc = open_out (root ^ "/depends") in + let map (t, d) = output_string oc (t^" "^String.concat " " d^"\n") in + List.iter map deps; close_out oc; + HLog.message ("Generated: " ^ root ^ "/depends") + | None -> + print_endline (String.concat " " (List.flatten (List.map snd deps))) + (* FG ***********************************************************************) (* scheme uri part as defined in URI Generic Syntax (RFC 3986) *) diff --git a/helm/software/components/library/librarian.mli b/helm/software/components/library/librarian.mli index e7b6df521..25ab0853e 100644 --- a/helm/software/components/library/librarian.mli +++ b/helm/software/components/library/librarian.mli @@ -91,7 +91,7 @@ module Make : * state that plus.ma needs nat and equality *) val load_deps_file: string -> (string * string list) list -val write_deps_file: string -> (string * string list) list -> unit +val write_deps_file: string option -> (string * string list) list -> unit (* FG ***********************************************************************) diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/.depend b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/.depend index 800096bb8..52fc20094 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/.depend +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/.depend @@ -1,4 +1,3 @@ -Base-2/theory.ma: Base-2/theory.mma Base-2/ext/tactics.ma Base-2/ext/arith.ma Base-2/types/props.ma Base-2/blt/props.ma Base-2/plist/props.ma Base-2/ext/tactics.ma: Base-2/ext/tactics.mma Base-2/preamble.ma Base-2/ext/arith.ma: Base-2/ext/arith.mma Base-2/preamble.ma Base-2/types/defs.ma: Base-2/types/defs.mma Base-2/preamble.ma diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/depends b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/depends index 7f10402a2..fd98f272c 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/depends +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/depends @@ -1,4 +1,3 @@ -Base-2/theory.mma Base-2/preamble.ma Base-1/theory.ma Base-2/ext/tactics.mma Base-2/preamble.ma Base-1/ext/tactics.ma Base-2/ext/arith.mma Base-2/preamble.ma Base-1/ext/arith.ma Base-2/types/defs.mma Base-2/preamble.ma Base-1/types/defs.ma diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory.ma similarity index 100% rename from helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory.mma rename to helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory.ma diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile index 99d22a93a..a2a3b8eec 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile @@ -6,15 +6,18 @@ DIR=$(shell basename $$PWD) MMAS = $(shell find Base-2 -name "*.mma") MAS = $(MMAS:%.mma=%.ma) +XMAS = Base-2/theory.ma pippo -%.ma: %.mma - $(H)../../matitac.opt $(MATITAOPTIONS) $< 2> /dev/null +%.ma: %.mma + $(H)../../matitac.opt $(MATITAOPTIONS) `../../matitadep.opt -stdout $<` 2> /dev/null $(H)../../matitac.opt $(MATITAOPTIONS) -dump $@ $< 2> /dev/null $(H)$(MAKE) --no-print-directory depend.opt $(DIR) all: $(MAS) + $(H)$(MAKE) --no-print-directory depend.full $(H)../../matitac $(MATITAOPTIONS) 2> /dev/null $(DIR).opt opt all.opt: $(MAS) + $(H)$(MAKE) --no-print-directory depend.full.opt $(H)../../matitac.opt $(MATITAOPTIONS) 2> /dev/null clean: $(H)../../matitaclean @@ -24,11 +27,26 @@ clean.opt: $(H)../../matitaclean.opt $(H)rm -f $(MAS) $(H)$(MAKE) --no-print-directory depend.opt +clean.ma: + $(H)../../matitaclean.opt $(MAS) + $(H)rm -f $(MAS) + $(H)$(MAKE) --no-print-directory depend.opt + depend: - $(H)../../matitadep + @echo matitadep + $(H)../../matitadep $(foreach FILE,$(XMAS),-exclude $(FILE)) $(H)cat Base-2/depends >> depends depend.opt: - $(H)../../matitadep.opt + @echo matitadep.opt + $(H)../../matitadep.opt $(foreach FILE,$(XMAS),-exclude $(FILE)) + $(H)cat Base-2/depends >> depends +depend.full: + @echo matitadep + $(H)../../matitadep + $(H)cat Base-2/depends >> depends +depend.full.opt: + @echo matitadep.opt + $(H)../../matitadep.opt $(H)cat Base-2/depends >> depends include Base-2/.depend diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/depends b/helm/software/matita/contribs/LAMBDA-TYPES/depends index 6c7aab739..a4314a81c 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/depends +++ b/helm/software/matita/contribs/LAMBDA-TYPES/depends @@ -224,7 +224,7 @@ Base-2/types/defs.ma Base-2/preamble.ma Base-2/types/props.ma Base-2/types/defs.ma Base-2/plist/defs.ma Base-2/preamble.ma Base-2/plist/props.ma Base-2/plist/defs.ma -Base-2/ext/arith.ma +Base-2/ext/arith.ma Base-2/preamble.ma Base-2/ext/tactics.ma Base-2/preamble.ma Base-2/blt/defs.ma Base-2/preamble.ma Base-2/blt/props.ma Base-2/blt/defs.ma @@ -234,7 +234,6 @@ NPlus/monoid.ma coq.ma datatypes/Bool.ma logic/equality.ma -Base-2/theory.mma Base-2/preamble.ma Base-1/theory.ma Base-2/ext/tactics.mma Base-2/preamble.ma Base-1/ext/tactics.ma Base-2/ext/arith.mma Base-2/preamble.ma Base-1/ext/arith.ma Base-2/types/defs.mma Base-2/preamble.ma Base-1/types/defs.ma diff --git a/helm/software/matita/matitaclean.ml b/helm/software/matita/matitaclean.ml index d9f603652..ffc253d69 100644 --- a/helm/software/matita/matitaclean.ml +++ b/helm/software/matita/matitaclean.ml @@ -111,12 +111,10 @@ let main () = UM.buri_of_uri (UM.uri_of_string suri) with UM.IllFormedUri _ -> let _,u,_,_ = Librarian.baseuri_of_script ~include_paths:[] suri in - if String.length u < 5 || String.sub u 0 5 <> "cic:/" then begin - HLog.error (sprintf "File %s defines a bad baseuri: %s" - suri u); + if Librarian.is_uri u then u else begin + HLog.error (sprintf "File %s defines a bad baseuri: %s" suri u); exit 1 - end else - u + end in uri::uris_to_remove) [] files in diff --git a/helm/software/matita/matitadep.ml b/helm/software/matita/matitadep.ml index ae95f8cf0..fc50a74fb 100644 --- a/helm/software/matita/matitadep.ml +++ b/helm/software/matita/matitadep.ml @@ -29,8 +29,23 @@ open Printf module GA = GrafiteAst module U = UriManager - +module HR = Helm_registry + +let fix_name f = + let f = + if Pcre.pmatch ~pat:"^\\./" f then String.sub f 2 (String.length f - 2) + else f + in + HExtlib.normalize_path f + +let exclude excluded_files files = + let map file = not (List.mem (fix_name file) excluded_files) in + List.filter map files + let main () = + let include_paths = ref [] in + let excluded_files = ref [] in + let use_stdout = ref false in (* all are maps from "file" to "something" *) let include_deps = Hashtbl.create 13 in let baseuri_of = Hashtbl.create 13 in @@ -38,8 +53,8 @@ let main () = let dot_name = "depends" in let dot_file = ref "" in let set_dot_file () = dot_file := dot_name^".dot" in + let set_excluded_file name = excluded_files := name :: !excluded_files in (* helpers *) - let include_paths = ref [] in let baseuri_of_script s = try Hashtbl.find baseuri_of s with Not_found -> @@ -66,9 +81,20 @@ let main () = (* initialization *) MatitaInit.add_cmdline_spec ["-dot", Arg.Unit set_dot_file, - "Save dependency graph in dot format and generate a png";]; + "Save dependency graph in dot format and generate a png"; + "-exclude", Arg.String set_excluded_file, + "Exclude a file from the dependences"; + "-stdout", Arg.Set use_stdout, + "Print dependences on stdout" + ]; MatitaInit.parse_cmdline_and_configuration_file (); MatitaInit.initialize_environment (); + if not (Helm_registry.get_bool "matita.verbose") then MatitaMisc.shutup (); + let cmdline_args = HR.get_list HR.string "matita.args" in + let files = fun () -> match cmdline_args with + | [] -> HExtlib.find ~test:(fun x -> Filename.check_suffix x ".ma") "." + | _ -> cmdline_args + in let args = let roots = Librarian.find_roots_in_dir (Sys.getcwd ()) in match roots with @@ -81,21 +107,15 @@ let main () = include_paths := (try Str.split (Str.regexp " ") (List.assoc "include_paths" opts) with Not_found -> []) @ - (Helm_registry.get_list Helm_registry.string "matita.includes"); - HExtlib.find ~test:(fun x -> Filename.check_suffix x ".ma") "." + (HR.get_list HR.string "matita.includes"); + files () | _ -> let roots = List.map (HExtlib.chop_prefix (Sys.getcwd()^"/")) roots in prerr_endline ("Too many roots found:\n\t"^String.concat "\n\t" roots); prerr_endline ("\nEnter one of these directories and retry"); exit 1 in - let fix_name f = - let f = - if Pcre.pmatch ~pat:"^\\./" f then String.sub f 2 (String.length f - 2) - else f - in - HExtlib.normalize_path f - in + let args = exclude !excluded_files args in let ma_files = args in (* here we go *) (* fills: @@ -145,11 +165,12 @@ let main () = acc d) [] deps in - Librarian.write_deps_file (Sys.getcwd()) + let where = if !use_stdout then None else Some (Sys.getcwd()) in + Librarian.write_deps_file where (deps@HExtlib.list_uniq (List.sort Pervasives.compare (List.map (fun x -> x,[]) extern))); (* dot generation *) - if !dot_file <> "" then + if !dot_file <> "" then begin let oc = open_out !dot_file in let fmt = Format.formatter_of_out_channel oc in -- 2.39.2