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) *)
* 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 ***********************************************************************)
-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
-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
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "Base-2/ext/tactics.ma".
+
+include "Base-2/ext/arith.ma".
+
+include "Base-2/types/props.ma".
+
+include "Base-2/blt/props.ma".
+
+include "Base-2/plist/props.ma".
+
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-(* This file was automatically generated: do not edit *********************)
-
-include "Base-2/ext/tactics.ma".
-
-include "Base-2/ext/arith.ma".
-
-include "Base-2/types/props.ma".
-
-include "Base-2/blt/props.ma".
-
-include "Base-2/plist/props.ma".
-
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
$(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
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
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
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
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
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 ->
(* 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
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:
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
projects / helm.git / commitdiff