From 9722a8d7b63e62f2b5b00de008304485371f7bf6 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 25 Mar 2016 18:48:24 +0000 Subject: [PATCH] - probe: now includes source character count (was: mac) - lambdadelta: summaries are generated using the updated probe --- matita/components/binaries/mac/Makefile | 6 ---- matita/components/binaries/mac/options.ml | 27 ---------------- matita/components/binaries/mac/options.mli | 18 ----------- matita/components/binaries/probe/engine.ml | 8 +++++ matita/components/binaries/probe/engine.mli | 2 ++ .../binaries/{mac/mac.ml => probe/mac.etc} | 0 .../{mac/lexer.mll => probe/macLexer.mll} | 10 +++--- .../components/binaries/probe/matitaList.ml | 7 ++-- matita/components/binaries/probe/options.ml | 9 ++++++ matita/components/binaries/probe/options.mli | 4 +++ matita/components/binaries/probe/probe.ml | 32 +++++++++++-------- matita/matita/contribs/lambdadelta/Makefile | 29 +++++++++-------- 12 files changed, 67 insertions(+), 85 deletions(-) delete mode 100644 matita/components/binaries/mac/Makefile delete mode 100644 matita/components/binaries/mac/options.ml delete mode 100644 matita/components/binaries/mac/options.mli rename matita/components/binaries/{mac/mac.ml => probe/mac.etc} (100%) rename matita/components/binaries/{mac/lexer.mll => probe/macLexer.mll} (84%) diff --git a/matita/components/binaries/mac/Makefile b/matita/components/binaries/mac/Makefile deleted file mode 100644 index 2a738628f..000000000 --- a/matita/components/binaries/mac/Makefile +++ /dev/null @@ -1,6 +0,0 @@ -EXEC = mac -VERSION=0.1.0 - -REQUIRES = - -include ../Makefile.common diff --git a/matita/components/binaries/mac/options.ml b/matita/components/binaries/mac/options.ml deleted file mode 100644 index ad48d2ebb..000000000 --- a/matita/components/binaries/mac/options.ml +++ /dev/null @@ -1,27 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -let debug_lexer_default = false - -let count_default = 0 - -let page_default = 5120 - -let debug_lexer = ref debug_lexer_default - -let count = ref count_default - -let page = ref page_default - -let clear () = - debug_lexer := debug_lexer_default; - count := count_default; - page := page_default diff --git a/matita/components/binaries/mac/options.mli b/matita/components/binaries/mac/options.mli deleted file mode 100644 index 1816f3d15..000000000 --- a/matita/components/binaries/mac/options.mli +++ /dev/null @@ -1,18 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -val debug_lexer: bool ref - -val count: int ref - -val page: int ref - -val clear: unit -> unit diff --git a/matita/components/binaries/probe/engine.ml b/matita/components/binaries/probe/engine.ml index c959e648c..c25201508 100644 --- a/matita/components/binaries/probe/engine.ml +++ b/matita/components/binaries/probe/engine.ml @@ -18,6 +18,8 @@ module US = U.UriSet module B = Librarian module H = HExtlib +module M = MacLexer + let unsupported protocol = failwith (P.sprintf "probe: unsupported protocol: %s" protocol) @@ -55,3 +57,9 @@ let get_uri str = aux (F.dirname bdir) (F.concat (F.basename bdir) file) in aux dir file + +let mac fname = + let ich = open_in fname in + let lexbuf = Lexing.from_channel ich in + M.token lexbuf; close_in ich + diff --git a/matita/components/binaries/probe/engine.mli b/matita/components/binaries/probe/engine.mli index 808315971..df8a69ff3 100644 --- a/matita/components/binaries/probe/engine.mli +++ b/matita/components/binaries/probe/engine.mli @@ -15,6 +15,8 @@ val out_length: NUri.UriSet.t -> unit val out_uris: NUri.UriSet.t -> unit +val mac: string -> unit + val is_registry: string -> bool val get_uri: string -> string * string diff --git a/matita/components/binaries/mac/mac.ml b/matita/components/binaries/probe/mac.etc similarity index 100% rename from matita/components/binaries/mac/mac.ml rename to matita/components/binaries/probe/mac.etc diff --git a/matita/components/binaries/mac/lexer.mll b/matita/components/binaries/probe/macLexer.mll similarity index 84% rename from matita/components/binaries/mac/lexer.mll rename to matita/components/binaries/probe/macLexer.mll index c6e56176e..5e4c01d3d 100644 --- a/matita/components/binaries/mac/lexer.mll +++ b/matita/components/binaries/probe/macLexer.mll @@ -24,11 +24,11 @@ let QT = '"' rule token = parse | OL { out "COM"; block lexbuf; token lexbuf } - | QT { out "STR"; O.count := !O.count + str lexbuf; token lexbuf } - | SPC { out "SPC"; incr O.count; token lexbuf } - | UNI { out "UNI"; incr O.count; token lexbuf } - | WRD { out "WRD"; incr O.count; token lexbuf } - | _ { out "CHR"; incr O.count; token lexbuf } + | QT { out "STR"; O.chars := !O.chars + str lexbuf; token lexbuf } + | SPC { out "SPC"; incr O.chars; token lexbuf } + | UNI { out "UNI"; incr O.chars; token lexbuf } + | WRD { out "WRD"; incr O.chars; token lexbuf } + | _ { out "CHR"; incr O.chars; token lexbuf } | eof { out "EOF" } and str = parse | QT { 2 } diff --git a/matita/components/binaries/probe/matitaList.ml b/matita/components/binaries/probe/matitaList.ml index 22b2f91b5..ee6cb417a 100644 --- a/matita/components/binaries/probe/matitaList.ml +++ b/matita/components/binaries/probe/matitaList.ml @@ -26,6 +26,8 @@ let chop_extension file = try F.chop_extension file with Invalid_argument("Filename.chop_extension") -> file +let script devel = chop_extension devel ^ ".ma" + let src_exists path = !O.no_devel || Y.file_exists path let is_obj base path = @@ -43,7 +45,7 @@ let is_dir base path = H.is_dir (F.concat base path) let is_script devel = - src_exists (chop_extension devel ^ ".ma") + src_exists (script devel) let mk_file path = if F.check_suffix path "/" then S.sub path 0 (pred (S.length path)) @@ -57,7 +59,8 @@ let add_obj path = 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 + 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 diff --git a/matita/components/binaries/probe/options.ml b/matita/components/binaries/probe/options.ml index 655539d14..d84d2b3e1 100644 --- a/matita/components/binaries/probe/options.ml +++ b/matita/components/binaries/probe/options.ml @@ -30,6 +30,10 @@ let default_exclude = [] let default_net = 0 +let default_chars = 0 + +let default_debug_lexer = false + let default_no_devel = true let default_no_init = true @@ -48,6 +52,10 @@ let exclude = ref default_exclude let net = ref default_net +let chars = ref default_chars + +let debug_lexer = ref default_debug_lexer + let no_devel = ref default_no_devel let no_init = ref default_no_init @@ -74,4 +82,5 @@ 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 diff --git a/matita/components/binaries/probe/options.mli b/matita/components/binaries/probe/options.mli index 7b99bf535..1158a84c8 100644 --- a/matita/components/binaries/probe/options.mli +++ b/matita/components/binaries/probe/options.mli @@ -27,6 +27,10 @@ val exclude: NCic.source list ref val net: int ref +val chars: int ref + +val debug_lexer: bool ref + val no_devel: bool ref val no_init: bool ref diff --git a/matita/components/binaries/probe/probe.ml b/matita/components/binaries/probe/probe.ml index e3d8f6cc9..16a2ce9e2 100644 --- a/matita/components/binaries/probe/probe.ml +++ b/matita/components/binaries/probe/probe.ml @@ -50,15 +50,17 @@ let set_i () = O.exclude := `Implied :: !O.exclude let set_p () = O.exclude := `Provided :: !O.exclude -let out_c () = E.out_int !O.net - let out_f () = O.iter_xflavours E.out_int +let out_oc () = E.out_int !O.net + let out_on () = E.out_length !O.objs let out_os () = E.out_uris !O.objs -let out_sn () = E.out_length !O.srcs +let out_sc () = E.out_int !O.chars + +let out_sn () = E.out_length !O.srcs let out_ss () = E.out_uris !O.srcs @@ -71,26 +73,30 @@ let clear () = D.objects (); O.clear () let _ = - let help = "Usage: probe [ -X | | -gip | HELM (base)uri | -cf | -on | os | -sn | -ss ]*" in + 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_c = " Print the total intrinsic complexity" in - let help_g = " Exclude generated objects" 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 - let help_p = " Exclude provided objects" in + let help_oc = " Print the total intrinsic complexity (objects)" in let help_on = " Print the number of objects" in let help_os = " Print the list of objects" in + let help_p = " Exclude provided objects" in + let help_sc = " Print the total extrinsic complexity (sources)" in let help_sn = " Print the number of sources" in let help_ss = " Print the list of sources" in A.parse [ - "-X" , A.Unit clear, help_X; - "-c" , A.Unit out_c, help_c; - "-f" , A.Unit out_f, help_f; - "-g" , A.Unit set_g, help_g; - "-i" , A.Unit set_i, help_i; + "-L" , A.Set O.debug_lexer, help_L; + "-X" , A.Unit clear , help_X; + "-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; ] process help; diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index f3d8b3232..6aa7ffbf8 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -52,7 +52,7 @@ define MAS_TEMPLATE $(1)/$(1)_probe.txt: $$(MAS_$(1)) @echo " PROBE $(1)" - $$(H)$$(PRB_DIR)/$$(PRB) $$(PRB_OPTS) $(1) -sn -on -c > $$@ + $$(H)$$(PRB_DIR)/$$(PRB) $$(PRB_OPTS) $(1) -sn -sc -on -oc -f > $$@ $(1)/$(1)_mac.txt: $$(MAS_$(1)) @echo " MAC $(1)" @@ -192,16 +192,17 @@ define SUMMARY_TEMPLATE SUMS += $$(SUM_$(1)) $$(SUM_$(1)): S0 = $$(shell cat $(1)/$(1)_probe.txt) - $$(SUM_$(1)): S1 = $$(shell cat $(1)/$(1)_mac.txt) - $$(SUM_$(1)): S4 = $$(shell ls $$(MAS_$(1)) | wc -l) - $$(SUM_$(1)): C1 = $$(shell grep "^inductive \|^record " $$(MAS_$(1)) | wc -l) - $$(SUM_$(1)): C2 = $$(shell grep "^definition \|^let rec " $$(MAS_$(1)) | wc -l) - $$(SUM_$(1)): C3 = $$(shell grep "^inductive \|^record \|^definition \|^let rec " $$(MAS_$(1)) | wc -l) - $$(SUM_$(1)): P1 = $$(shell grep "^theorem " $$(MAS_$(1)) | wc -l) - $$(SUM_$(1)): P2 = $$(shell grep "^lemma " $$(MAS_$(1)) | wc -l) - $$(SUM_$(1)): P3 = $$(shell grep "^lemma \|^theorem " $$(MAS_$(1)) | wc -l) - - $$(SUM_$(1)): $$(MAS_$(1)) $(1)/$(1)_probe.txt $(1)/$(1)_mac.txt + $$(SUM_$(1)): S1 = $$(word 1, $$(S0)) + $$(SUM_$(1)): S2 = $$(word 2, $$(S0)) + $$(SUM_$(1)): S4 = $$(word 4, $$(S0)) + $$(SUM_$(1)): C1 = $$(word 5, $$(S0)) + $$(SUM_$(1)): C2 = $$(word 7, $$(S0)) + $$(SUM_$(1)): C3 = $$(shell echo "$$(C1)+$$(C2)"|bc) + $$(SUM_$(1)): P1 = $$(word 10, $$(S0)) + $$(SUM_$(1)): P2 = $$(word 9, $$(S0)) + $$(SUM_$(1)): P3 = $$(shell echo "$$(P1)+$$(P2)"|bc) + + $$(SUM_$(1)): $$(MAS_$(1)) $(1)/$(1)_probe.txt @printf ' SUMMARY $(1)\n' @printf 'name "$$(basename $$(@F))"\n\n' > $$@ @printf 'table {\n' >> $$@ @@ -209,9 +210,9 @@ define SUMMARY_TEMPLATE @printf ' [ "objects" * ]\n' >> $$@ @printf ' ]\n' >> $$@ @printf ' class "cyan" [ "sizes"\n' >> $$@ - @printf ' [ "files" "$$(S4)" ]\n' >> $$@ - @printf ' [ "characters" "$$(word 1, $$(S1))" ]\n' >> $$@ - @printf ' [ "nodes" "$$(word 3, $$(S0))" ]\n' >> $$@ + @printf ' [ "files" "$$(S1)" ]\n' >> $$@ + @printf ' [ "characters" "$$(S2)" ]\n' >> $$@ + @printf ' [ "nodes" "$$(S4)" ]\n' >> $$@ @printf ' ]\n' >> $$@ @printf ' class "green" [ "propositions"\n' >> $$@ @printf ' [ "theorems" "$$(P1)" ]\n' >> $$@ -- 2.39.2