From 2f19651bcec24abfb1bf15ff7e1387daad1f6638 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 9 Nov 2019 18:27:55 +0100 Subject: [PATCH] updated probe and matitadep + matitadep: bug fixed in loop display + new options -b and -i to output backward dependences --- matita/components/binaries/matitadep/Makefile | 2 +- .../binaries/matitadep/matitadep.ml | 127 +++++++++----- matita/components/binaries/probe/engine.ml | 6 +- .../components/binaries/probe/matitaList.ml | 86 +++++----- matita/components/binaries/probe/nCicScan.ml | 161 ++++++++++-------- matita/components/binaries/probe/options.ml | 50 ++++-- matita/components/binaries/probe/options.mli | 4 + matita/components/binaries/probe/probe.ml | 12 +- matita/matita/contribs/lambdadelta/Makefile | 9 +- 9 files changed, 274 insertions(+), 183 deletions(-) diff --git a/matita/components/binaries/matitadep/Makefile b/matita/components/binaries/matitadep/Makefile index 7695ab288..2fe33e60b 100644 --- a/matita/components/binaries/matitadep/Makefile +++ b/matita/components/binaries/matitadep/Makefile @@ -1,6 +1,6 @@ EXEC = matitadep VERSION=0.1.0 -REQUIRES = +REQUIRES = helm-ng_library include ../Makefile.common diff --git a/matita/components/binaries/matitadep/matitadep.ml b/matita/components/binaries/matitadep/matitadep.ml index d21af12a3..426ab6926 100644 --- a/matita/components/binaries/matitadep/matitadep.ml +++ b/matita/components/binaries/matitadep/matitadep.ml @@ -5,6 +5,12 @@ type file = { rdeps: StringSet.t option (* recursive dependences *) } +let show_check = ref false +let show_top = ref false +let show_leaf = ref false +let show_back = ref "" +let iset = ref StringSet.empty + let graph = Hashtbl.create 503 let debug = ref 0 @@ -24,36 +30,41 @@ let add_ddep fname dname = Hashtbl.replace graph fname {file with ddeps = dname :: file.ddeps} let init fname dname = - if !debug land 1 > 0 then Printf.eprintf "init: %s: %s.\n" fname dname; + if !debug land 1 > 0 then Printf.printf "init: %s: %s.\n" fname dname; add fname; add dname; add_ddep fname dname (* vdeps: visited dependences for loop detection *) let rec compute_from_file vdeps fname file = match file.rdeps with | Some rdeps -> rdeps | None -> - if !debug land 2 > 0 then Printf.eprintf " compute file: %s\n" fname; - let vdeps = fname :: vdeps in - List.iter (redundant vdeps fname file.ddeps) file.ddeps; - let rdeps = compute_from_ddeps vdeps file.ddeps in - Hashtbl.replace graph fname {file with rdeps = Some rdeps}; - rdeps + if !debug land 2 > 0 then Printf.printf " (%u) compute object: %s\n%!" (List.length vdeps) fname; + if !debug land 2 > 0 then Printf.printf " ddeps: %s\n%!" (String.concat " " file.ddeps); + if !debug land 8 > 0 then Printf.printf " vdeps: %s\n%!" (String.concat " " vdeps); + if List.mem fname vdeps then begin + if !show_check then Printf.printf "circular: %s\n%!" (String.concat " " vdeps); + StringSet.empty + end else begin + let vdeps = fname :: vdeps in + List.iter (redundant vdeps fname file.ddeps) file.ddeps; + let rdeps = compute_from_ddeps vdeps file.ddeps in + Hashtbl.replace graph fname {file with rdeps = Some rdeps}; + rdeps + end and compute_from_dname vdeps rdeps dname = - if List.mem dname vdeps then begin - let loop = purge dname (List.rev vdeps) in - Printf.printf "circular: %s\n" (String.concat " " loop); - StringSet.add dname rdeps - end else - let file = Hashtbl.find graph dname in - StringSet.add dname (StringSet.union (compute_from_file vdeps dname file) rdeps) + if !debug land 4 > 0 then Printf.printf " (%u) compute dep: %s\n%!" (List.length vdeps) dname; + if !debug land 8 > 0 then Printf.printf " vdeps: %s\n%!" (String.concat " " vdeps); + let file = Hashtbl.find graph dname in + let rdeps = StringSet.add dname rdeps in + StringSet.union (compute_from_file vdeps dname file) rdeps and compute_from_ddeps vdeps ddeps = List.fold_left (compute_from_dname vdeps) StringSet.empty ddeps and redundant vdeps fname ddeps dname = let rdeps = compute_from_ddeps vdeps (purge dname ddeps) in - if StringSet.mem dname rdeps then - Printf.printf "%s: redundant %s\n" fname dname + if !show_check && StringSet.mem dname rdeps then + Printf.printf "%S: redundant %S\n%!" fname dname let check () = let iter fname file = ignore (compute_from_file [] fname file) in @@ -82,52 +93,90 @@ let leaf () = let fnames = get_leafs () in StringSet.iter iter fnames -let back fname = - Printf.printf "backward: %s\n" fname; - try match (Hashtbl.find graph fname).rdeps with +let rec file_iter map ich = + let line = input_line ich in + if line <> "" then map line; + file_iter map ich + +let back name = + Printf.printf "\"%s\":\n" name; + try match (Hashtbl.find graph name).rdeps with | None -> () | Some rdeps -> - let iter fname = Printf.printf "%s\n" fname in - StringSet.iter iter rdeps - with Not_found -> () + let rdeps = + if !iset = StringSet.empty then rdeps + else StringSet.inter rdeps !iset + in + let iter name = Printf.printf " \"%s\"\n" name in + StringSet.iter iter rdeps; + Printf.printf "\n" + with Not_found -> Printf.printf "* not found\n\n" -let rec read ich = +let back fname = + if Librarian.is_uri fname then back fname else + let ich = open_in fname in + try file_iter back ich with End_of_file -> close_in ich + +let set_iset fname = + if Librarian.is_uri fname then iset := StringSet.singleton fname else + let map name = iset := StringSet.add name !iset in + let ich = open_in fname in + try file_iter map ich with End_of_file -> close_in ich + +let rec read_many ich s = let line = input_line ich in - begin try Scanf.sscanf line "%s@:include \"%s@\"." init - with Scanf.Scan_failure _ -> - begin try Scanf.sscanf line "./%s@:include \"%s@\"." init - with Scanf.Scan_failure _ -> + if line = "" then () else begin + begin try Scanf.sscanf line " %S" (init s) + with Scanf.Scan_failure _ | End_of_file -> + Printf.eprintf "unknown line: %s.\n" line + end; + read_many ich s + end + +let rec read_deps ich = + let line = input_line ich in + begin try Scanf.sscanf line "%s@:include %S." init + with Scanf.Scan_failure _ | End_of_file -> + begin try Scanf.sscanf line "./%s@:include %S." init + with Scanf.Scan_failure _ | End_of_file -> begin try Scanf.sscanf line "%s@:(*%s@*)" (fun _ _ -> ()) - with Scanf.Scan_failure _ -> - Printf.eprintf "unknown line: %s.\n" line + with Scanf.Scan_failure _ | End_of_file -> + begin try Scanf.sscanf line "%S:%!" (read_many ich) + with Scanf.Scan_failure _ | End_of_file -> + begin try Scanf.sscanf line "%S: %S" init + with Scanf.Scan_failure _ | End_of_file -> + Printf.eprintf "unknown line: %s.\n" line + end + end end end end; - read ich + read_deps ich let _ = - let show_check = ref false in - let show_top = ref false in - let show_leaf = ref false in - let show_back = ref "" in - let process_file name = () in + let process_file name = + let ich = open_in name in + try read_deps ich with End_of_file -> close_in ich + in let show () = - if !show_check then check (); + if !show_check || !show_back <> "" then check (); if !show_top then top (); if !show_leaf then leaf (); if !show_back <> "" then back !show_back in - let help = "matitadep [-clt | -d | -b ] < " in - let help_b = " Print the backward dependences of this node" in + let help = "matitadep [ -clt | -d | -bi [ | ] | ]*" in + let help_b = "| Print the backward dependences of these nodes" in let help_c = " Print the redundant and looping arcs of the dependences graph" in let help_d = " Set these debug options" in + let help_i = "| Intersect with these nodes" in let help_l = " Print the leaf nodes of the dependences graph" in let help_t = " Print the top nodes of the dependences graph" in Arg.parse [ "-b", Arg.String ((:=) show_back), help_b; "-c", Arg.Set show_check, help_c; "-d", Arg.Int ((:=) debug), help_d; + "-i", Arg.String set_iset, help_i; "-l", Arg.Set show_leaf, help_l; "-t", Arg.Set show_top, help_t; ] process_file help; - try read stdin with End_of_file -> show () + show () diff --git a/matita/components/binaries/probe/engine.ml b/matita/components/binaries/probe/engine.ml index c25201508..0fe7ace53 100644 --- a/matita/components/binaries/probe/engine.ml +++ b/matita/components/binaries/probe/engine.ml @@ -43,14 +43,14 @@ let is_registry str = let get_uri str = let str = H.normalize_path str in let dir, file = - if H.is_regular str && F.check_suffix str ".ma" + if H.is_regular str && F.check_suffix str ".ma" then F.dirname str, F.chop_extension (F.basename str) else if H.is_dir str then str, "" else missing str in let rec aux bdir file = match B.find_roots_in_dir bdir with - | [root] -> - let buri = L.assoc "baseuri" (B.load_root_file root) in + | [root] -> + let buri = L.assoc "baseuri" (B.load_root_file root) in F.concat bdir file, F.concat buri file | roots -> if bdir = F.current_dir_name || bdir = F.dir_sep then unrooted dir roots else diff --git a/matita/components/binaries/probe/matitaList.ml b/matita/components/binaries/probe/matitaList.ml index ee6cb417a..d6426e361 100644 --- a/matita/components/binaries/probe/matitaList.ml +++ b/matita/components/binaries/probe/matitaList.ml @@ -23,73 +23,73 @@ module O = Options module E = Engine let chop_extension file = - try F.chop_extension file - with Invalid_argument("Filename.chop_extension") -> file + try F.chop_extension file + with Invalid_argument _ -> file let script devel = chop_extension devel ^ ".ma" let src_exists path = !O.no_devel || Y.file_exists path -let is_obj base path = - if H.is_regular (F.concat base path) then - F.check_suffix path ".con.ng" || - F.check_suffix path ".ind.ng" || - F.check_suffix path ".var.ng" +let is_obj base path = + if H.is_regular (F.concat base path) then + F.check_suffix path ".con.ng" || + F.check_suffix path ".ind.ng" || + F.check_suffix path ".var.ng" else false -let is_src base path = - H.is_regular (F.concat base path) && - F.check_suffix path ".ng" +let is_src base path = + H.is_regular (F.concat base path) && + F.check_suffix path ".ng" let is_dir base path = - H.is_dir (F.concat base path) + H.is_dir (F.concat base path) let is_script devel = - src_exists (script devel) + src_exists (script devel) let mk_file path = - if F.check_suffix path "/" then S.sub path 0 (pred (S.length path)) - else path ^ ".ng" + if F.check_suffix path "/" then S.sub path 0 (pred (S.length path)) + else path ^ ".ng" let add_obj path = - let path = F.chop_extension path in - let str = F.concat "cic:" path in - O.objs := US.add (U.uri_of_string str) !O.objs + let path = F.chop_extension path in + let str = F.concat "cic:" path in + O.objs := US.add (U.uri_of_string str) !O.objs let add_src devel path = - let path = F.chop_extension path in - let str = F.concat "cic:" path ^ "/" in - O.srcs := US.add (U.uri_of_string str) !O.srcs; - E.mac (script devel) + let path = F.chop_extension path in + let str = F.concat "cic:" path ^ "/" in + O.srcs := US.add (U.uri_of_string str) !O.srcs; + E.mac (script devel) let add_remove base path = - O.remove := F.concat base path :: !O.remove + O.remove := F.concat base path :: !O.remove let rec scan_entry inner base devel path = -(* Printf.eprintf "%b %s %s%!\n" inner devel path; *) - if is_obj base path && inner then add_obj path else - if is_src base path && is_script devel then add_src devel path else - if is_dir base path && is_script devel then scan_dir true base devel path else - if is_dir base path && src_exists devel then scan_dir false base devel path else - add_remove base path +(* Printf.eprintf "%b %s %s%!\n" inner devel path; *) + if is_obj base path && inner then add_obj path else + if is_src base path && is_script devel then add_src devel path else + if is_dir base path && is_script devel then scan_dir true base devel path else + if is_dir base path && src_exists devel then scan_dir false base devel path else + add_remove base path and scan_dir inner base devel path = - let files = Y.readdir (F.concat base path) in - let map base file = scan_entry inner base (F.concat devel file) (F.concat path file) in - A.iter (map base) files + let files = Y.readdir (F.concat base path) in + let map base file = scan_entry inner base (F.concat devel file) (F.concat path file) in + A.iter (map base) files let from_uri base devel uri = - O.no_devel := devel = ""; - let str = U.string_of_uri uri in - let i = S.index str '/' in - let protocol = S.sub str 0 i in - if protocol = "cic:" then - let path = S.sub str (succ i) (S.length str - succ i) in - let file = mk_file path in - if Y.file_exists (F.concat base file) then - scan_entry (is_script devel) base devel file - else E.missing path - else E.unsupported protocol + O.no_devel := devel = ""; + let str = U.string_of_uri uri in + let i = S.index str '/' in + let protocol = S.sub str 0 i in + if protocol = "cic:" then + let path = S.sub str (succ i) (S.length str - succ i) in + let file = mk_file path in + if Y.file_exists (F.concat base file) then + scan_entry (is_script devel) base devel file + else E.missing path + else E.unsupported protocol let from_string base devel s = - from_uri base devel (U.uri_of_string s) + from_uri base devel (U.uri_of_string s) diff --git a/matita/components/binaries/probe/nCicScan.ml b/matita/components/binaries/probe/nCicScan.ml index fc6957292..f1c2772ec 100644 --- a/matita/components/binaries/probe/nCicScan.ml +++ b/matita/components/binaries/probe/nCicScan.ml @@ -20,88 +20,105 @@ module E = NCicEnvironment module O = Options +type status = { +(* current complexity *) + c: int; +(* current uri *) + u: U.uri; +} + let status = new P.status let malformed () = - failwith "probe: malformed term" + failwith "probe: malformed term" let add_attr n (_, xf, _) = O.add_xflavour n (xf:>O.def_xflavour) let add_ind n = O.add_xflavour n `Inductive let rec set_list c ts cts = - let map cts t = (c, t) :: cts in - L.fold_left map cts ts + let map cts t = (c, t) :: cts in + L.fold_left map cts ts let set_funs c rfs cts = - let map cts (_, _, _, t0, t1) = set_list c [t0; t1] cts in - L.fold_left map cts rfs + let map cts (_, _, _, t0, t1) = set_list c [t0; t1] cts in + L.fold_left map cts rfs let set_type c cts (_, _, t, css) = - let map cts (_, _, t) = (c, t) :: cts in - (c, t) :: L.fold_left map cts css - -let scan_lref a c i = - try match List.nth c (pred i) with - | _, C.Decl _ -> succ a - | _, C.Def _ -> a - with - | Failure _ -> succ a - -let scan_gref a = function - | R.Ref (_, R.Decl) - | R.Ref (_, R.Ind _) - | R.Ref (_, R.Con _) -> succ a - | R.Ref (u, R.Def _) - | R.Ref (u, R.Fix _) - | R.Ref (u, R.CoFix _) -> - if US.mem u !O.objs then a else succ a - -let rec scan_term a = function - | [] -> a - | (_, C.Meta _) :: tl - | (_, C.Implicit _) :: tl -> scan_term a tl - | (_, C.Sort _) :: tl -> scan_term (succ a) tl - | (c, C.Rel i) :: tl -> scan_term (scan_lref a c i) tl - | (_, C.Const p) :: tl -> scan_term (scan_gref a p) tl - | (_, C.Appl []) :: tl -> malformed () - | (c, C.Appl ts) :: tl -> - scan_term (L.length ts + pred a) (set_list c ts tl) - | (c, C.Match (_, t0, t1, ts)) :: tl -> - scan_term a (set_list c (t0::t1::ts) tl) - | (c, C.Prod (s, t0, t1)) :: tl - | (c, C.Lambda (s, t0, t1)) :: tl -> - scan_term (succ a) ((c, t0) :: ((s, C.Decl t0) :: c, t1) :: tl) - | (c, C.LetIn (s, t0, t1, t2)) :: tl -> - scan_term a ((c, t0) :: (c, t1) :: ((s, C.Def (t1, t0)) :: c, t2) :: tl) - -let scan_obj u a = - let _, _, _, _, obj = E.get_checked_obj status u in - match obj with - | C.Constant (_, _, None, t, m) -> - add_attr 1 m; - scan_term (succ a) [[], t] - | C.Constant (_, _, Some t0, t1, m) -> - add_attr 1 m; - scan_term (succ a) (set_list [] [t0; t1] []) - | C.Fixpoint (_, rfs, m) -> - add_attr (L.length rfs) m; - scan_term (a + L.length rfs) (set_funs [] rfs []) - | C.Inductive (_, _, its, _) -> - add_ind (L.length its); - let cts = L.fold_left (set_type []) [] its in - scan_term (a + L.length cts) cts - -let accept_obj u = - let _, _, _, _, obj = E.get_checked_obj status u in - let g = match obj with - | C.Constant (_, _, _, _, (g, _, _)) - | C.Fixpoint (_, _, (g, _, _)) - | C.Inductive (_, _, _, (g, _)) -> g - in - if L.mem g !O.exclude then false else true - -let scan () = - if !O.exclude <> [] then - O.objs := US.filter accept_obj !O.objs; - O.net := US.fold scan_obj !O.objs !O.net + let map cts (_, _, t) = (c, t) :: cts in + (c, t) :: L.fold_left map cts css + +let inc st = {st with c = succ st.c} + +let add st c = {st with c = st.c + c} + +let scan_lref st c i = + try match List.nth c (pred i) with + | _, C.Decl _ -> inc st + | _, C.Def _ -> st + with + | Failure _ -> inc st + +let scan_gref st = function + | R.Ref (u, R.Decl) + | R.Ref (u, R.Ind _) + | R.Ref (u, R.Con _) -> + O.add_dep st.u u; + inc st + | R.Ref (u, R.Def _) + | R.Ref (u, R.Fix _) + | R.Ref (u, R.CoFix _) -> + O.add_dep st.u u; + if US.mem u !O.objs then st else inc st + +let rec scan_term st = function + | [] -> st + | (_, C.Meta _) :: tl + | (_, C.Implicit _) :: tl -> scan_term st tl + | (_, C.Sort _) :: tl -> scan_term (inc st) tl + | (c, C.Rel i) :: tl -> scan_term (scan_lref st c i) tl + | (_, C.Const p) :: tl -> scan_term (scan_gref st p) tl + | (_, C.Appl []) :: tl -> malformed () + | (c, C.Appl ts) :: tl -> + scan_term (add st (pred (L.length ts))) (set_list c ts tl) + | (c, C.Match (_, t0, t1, ts)) :: tl -> + scan_term st (set_list c (t0::t1::ts) tl) + | (c, C.Prod (s, t0, t1)) :: tl + | (c, C.Lambda (s, t0, t1)) :: tl -> + scan_term (inc st) ((c, t0) :: ((s, C.Decl t0) :: c, t1) :: tl) + | (c, C.LetIn (s, t0, t1, t2)) :: tl -> + scan_term st ((c, t0) :: (c, t1) :: ((s, C.Def (t1, t0)) :: c, t2) :: tl) + +let scan_obj u c = + let st = {c; u} in + let _, _, _, _, obj = E.get_checked_obj status u in + let st = match obj with + | C.Constant (_, _, None, t, m) -> + add_attr 1 m; + scan_term (inc st) [[], t] + | C.Constant (_, _, Some t0, t1, m) -> + add_attr 1 m; + scan_term (inc st) (set_list [] [t0; t1] []) + | C.Fixpoint (_, rfs, m) -> + add_attr (L.length rfs) m; + scan_term (add st (L.length rfs)) (set_funs [] rfs []) + | C.Inductive (_, _, its, _) -> + add_ind (L.length its); + let cts = L.fold_left (set_type []) [] its in + scan_term (add st (L.length cts)) cts + in + st.c + +let accept_obj u = + let _, _, _, _, obj = E.get_checked_obj status u in + let g = match obj with + | C.Constant (_, _, _, _, (g, _, _)) + | C.Fixpoint (_, _, (g, _, _)) + | C.Inductive (_, _, _, (g, _)) -> g + in + if L.mem g !O.exclude then false else true + +let scan () = + if !O.exclude <> [] then + O.objs := US.filter accept_obj !O.objs; + O.net := US.fold scan_obj !O.objs !O.net diff --git a/matita/components/binaries/probe/options.ml b/matita/components/binaries/probe/options.ml index d84d2b3e1..981483e29 100644 --- a/matita/components/binaries/probe/options.ml +++ b/matita/components/binaries/probe/options.ml @@ -12,9 +12,11 @@ module A = Array module P = Printf -module C = NCic +module C = NCic module R = Helm_registry +module U = NUri module US = NUri.UriSet +module UH = NUri.UriHash type def_xflavour = [ C.def_flavour | `Inductive @@ -60,27 +62,41 @@ let no_devel = ref default_no_devel let no_init = ref default_no_init -let index_of_xflavour = function - | `Inductive -> 0 - | `Axiom -> 1 - | `Definition -> 2 - | `Fact -> 3 - | `Lemma -> 4 - | `Theorem -> 5 - | `Corollary -> 6 - | `Example -> 7 +let deps = UH.create 11 + +let index_of_xflavour = function + | `Inductive -> 0 + | `Axiom -> 1 + | `Definition -> 2 + | `Fact -> 3 + | `Lemma -> 4 + | `Theorem -> 5 + | `Corollary -> 6 + | `Example -> 7 let add_xflavour n xf = - let i = index_of_xflavour xf in - slot.(i) <- slot.(i) + n + let i = index_of_xflavour xf in + slot.(i) <- slot.(i) + n let clear_slot i _ = slot.(i) <- 0 let iter_xflavours map = A.iteri (fun _ -> map) slot +let add_dep c u = + UH.add deps c u + +let out_deps file = + let och = open_out file in + let map a b = + P.fprintf och "\"%s\": \"%s\"\n" (U.string_of_uri a) (U.string_of_uri b) + in + UH.iter map deps; + close_out och + let clear () = - R.clear (); A.iteri clear_slot slot; - objs := default_objs; srcs := default_srcs; remove := default_remove; - exclude := default_exclude; net := default_net; - chars := default_chars; debug_lexer := default_debug_lexer; - no_devel := default_no_devel; no_init := default_no_init + R.clear (); A.iteri clear_slot slot; + objs := default_objs; srcs := default_srcs; remove := default_remove; + exclude := default_exclude; net := default_net; + chars := default_chars; debug_lexer := default_debug_lexer; + no_devel := default_no_devel; no_init := default_no_init; + UH.reset deps diff --git a/matita/components/binaries/probe/options.mli b/matita/components/binaries/probe/options.mli index 1158a84c8..c36695ef5 100644 --- a/matita/components/binaries/probe/options.mli +++ b/matita/components/binaries/probe/options.mli @@ -35,4 +35,8 @@ val no_devel: bool ref val no_init: bool ref +val add_dep: NUri.uri -> NUri.uri -> unit + +val out_deps: string -> unit + val clear: unit -> unit diff --git a/matita/components/binaries/probe/probe.ml b/matita/components/binaries/probe/probe.ml index 16a2ce9e2..94c8707a7 100644 --- a/matita/components/binaries/probe/probe.ml +++ b/matita/components/binaries/probe/probe.ml @@ -28,9 +28,9 @@ let trusted _ = true let no_log _ _ = () let init registry = - R.load_from registry; + R.load_from registry; if !O.no_init then begin - B.init (); + B.init (); C.set_trust trusted; H.set_log_callback no_log; O.no_init := false; @@ -64,18 +64,21 @@ let out_sn () = E.out_length !O.srcs let out_ss () = E.out_uris !O.srcs +let out_b file = O.out_deps file + let process s = if L.is_uri s then scan_uri "" s else if E.is_registry s then init s else scan_from s -let clear () = +let clear () = D.objects (); O.clear () let _ = let help = "Usage: probe [ -LX | | -gip | | -f | -oc | -on | -os | -sc | -sn | -ss ]*" in let help_L = " Activate lexer debugging" in let help_X = " Clear configuration, options and counters" in + let help_b = " Print backward object dependences in this file" in let help_f = " Print the number of objects grouped by flavour" in let help_g = " Exclude generated objects" in let help_i = " Exclude implied objects" in @@ -89,13 +92,14 @@ let _ = A.parse [ "-L" , A.Set O.debug_lexer, help_L; "-X" , A.Unit clear , help_X; + "-b" , A.String out_b , help_b; "-f" , A.Unit out_f , help_f; "-g" , A.Unit set_g , help_g; "-i" , A.Unit set_i , help_i; "-oc", A.Unit out_oc, help_oc; "-on", A.Unit out_on, help_on; "-os", A.Unit out_os, help_os; - "-p" , A.Unit set_p , help_p; + "-p" , A.Unit set_p , help_p; "-sc", A.Unit out_sc, help_sc; "-sn", A.Unit out_sn, help_sn; "-ss", A.Unit out_ss, help_ss; diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index 59cf50f6e..dd955bcc2 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -50,7 +50,8 @@ define MAS_TEMPLATE $(1)/$(1)_probe.txt: $$(MAS_$(1)) @echo " PROBE $(1)" - $$(H)$$(PRB_DIR)/$$(PRB) $$(PRB_OPTS) $(1) -sn -sc -on -oc -f > $$@ + $$(H)$$(PRB_DIR)/$$(PRB) $$(PRB_OPTS) $(1) -sn -sc -on -oc -f -b $(1)/$(1)_deps.txt > $$@ + $$(H)sort < $(1)/$(1)_deps.txt | uniq > $(1)/$(1)_deps_uniq.txt endef $(foreach PKG, $(PACKAGES), $(eval $(call MAS_TEMPLATE,$(PKG)))) @@ -102,19 +103,19 @@ $(DEP_INPUT): $(MAS) Makefile deps: $(DEP_INPUT) @echo " MATITADEP -c" - $(H)$(DEP_DIR)/$(DEP) -c $(DEP_OPTS) < $< + $(H)$(DEP_DIR)/$(DEP) -c $(DEP_OPTS) $< # top ######################################################################## top: $(DEP_INPUT) @echo " MATITADEP -t" - $(H)$(DEP_DIR)/$(DEP) -t $(DEP_OPTS) < $< + $(H)$(DEP_DIR)/$(DEP) -t $(DEP_OPTS) $< # leaf ####################################################################### leaf: $(DEP_INPUT) @echo " MATITADEP -l" - $(H)$(DEP_DIR)/$(DEP) -l $(DEP_OPTS) < $< + $(H)$(DEP_DIR)/$(DEP) -l $(DEP_OPTS) $< # stats ###################################################################### -- 2.39.2