From: Ferruccio Guidi Date: Fri, 25 Mar 2016 18:48:24 +0000 (+0000) Subject: - probe: now includes source character count (was: mac) X-Git-Tag: make_still_working~624 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9722a8d7b63e62f2b5b00de008304485371f7bf6;p=helm.git - probe: now includes source character count (was: mac) - lambdadelta: summaries are generated using the updated probe --- 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/lexer.mll b/matita/components/binaries/mac/lexer.mll deleted file mode 100644 index c6e56176e..000000000 --- a/matita/components/binaries/mac/lexer.mll +++ /dev/null @@ -1,43 +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_______________________________________________________________ *) - -{ - module O = Options - - let out s = if !O.debug_lexer then prerr_endline s -} - -let OL = "(*" -let CL = "*)" -let UNI = ['\x80'-'\xBF']+ -let SPC = ['\r' '\n' '\t' ' ']+ -let WRD = ['0'-'9' 'A'-'Z' 'a'-'z' '_']+ -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 } - | eof { out "EOF" } -and str = parse - | QT { 2 } - | "\\\"" { succ (str lexbuf) } - | UNI { succ (str lexbuf) } - | WRD { succ (str lexbuf) } - | _ { succ (str lexbuf) } -and block = parse - | CL { () } - | OL { block lexbuf; block lexbuf } - | QT { let _ = str lexbuf in block lexbuf } - | _ { block lexbuf } diff --git a/matita/components/binaries/mac/mac.ml b/matita/components/binaries/mac/mac.ml deleted file mode 100644 index 18bba1746..000000000 --- a/matita/components/binaries/mac/mac.ml +++ /dev/null @@ -1,59 +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_______________________________________________________________ *) - -module A = Arg -module P = Printf - -module O = Options -module L = Lexer - -let help = "Usage: mac [ -LXQV | -p ]* [ ]*" -let help_L = " Activate lexer debugging" -let help_Q = " Read data from standard input" -let help_V = " Show version information" -let help_X = " Reset options and counters" -let help_p = " Assume characters per page (default: 5120)" - -let active = ref false - -let process_channel ich = - let lexbuf = Lexing.from_channel ich in - L.token lexbuf; active := true - -let output_version () = - P.printf "mac 0.1.1 M - July 2013\n" - -let process_stdin () = - process_channel stdin - -let process_file fname = - let ich = open_in fname in - process_channel ich; close_in ich - -let set_page i = - if i > 0 then O.page := i - -let output_count () = - if !active then - let pages = !O.count / !O.page in - let pages = if !O.count mod !O.page = 0 then pages else succ pages in - P.printf "%u %u\n" !O.count pages - -let main () = - A.parse [ - "-L", A.Set O.debug_lexer, help_L; - "-Q", Arg.Unit process_stdin, help_Q; - "-V", Arg.Unit output_version, help_V; - "-X", A.Unit O.clear, help_X; - ] process_file help; - output_count () - -let _ = main () 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/probe/mac.etc b/matita/components/binaries/probe/mac.etc new file mode 100644 index 000000000..18bba1746 --- /dev/null +++ b/matita/components/binaries/probe/mac.etc @@ -0,0 +1,59 @@ +(* + ||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_______________________________________________________________ *) + +module A = Arg +module P = Printf + +module O = Options +module L = Lexer + +let help = "Usage: mac [ -LXQV | -p ]* [ ]*" +let help_L = " Activate lexer debugging" +let help_Q = " Read data from standard input" +let help_V = " Show version information" +let help_X = " Reset options and counters" +let help_p = " Assume characters per page (default: 5120)" + +let active = ref false + +let process_channel ich = + let lexbuf = Lexing.from_channel ich in + L.token lexbuf; active := true + +let output_version () = + P.printf "mac 0.1.1 M - July 2013\n" + +let process_stdin () = + process_channel stdin + +let process_file fname = + let ich = open_in fname in + process_channel ich; close_in ich + +let set_page i = + if i > 0 then O.page := i + +let output_count () = + if !active then + let pages = !O.count / !O.page in + let pages = if !O.count mod !O.page = 0 then pages else succ pages in + P.printf "%u %u\n" !O.count pages + +let main () = + A.parse [ + "-L", A.Set O.debug_lexer, help_L; + "-Q", Arg.Unit process_stdin, help_Q; + "-V", Arg.Unit output_version, help_V; + "-X", A.Unit O.clear, help_X; + ] process_file help; + output_count () + +let _ = main () diff --git a/matita/components/binaries/probe/macLexer.mll b/matita/components/binaries/probe/macLexer.mll new file mode 100644 index 000000000..5e4c01d3d --- /dev/null +++ b/matita/components/binaries/probe/macLexer.mll @@ -0,0 +1,43 @@ +(* + ||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_______________________________________________________________ *) + +{ + module O = Options + + let out s = if !O.debug_lexer then prerr_endline s +} + +let OL = "(*" +let CL = "*)" +let UNI = ['\x80'-'\xBF']+ +let SPC = ['\r' '\n' '\t' ' ']+ +let WRD = ['0'-'9' 'A'-'Z' 'a'-'z' '_']+ +let QT = '"' + +rule token = parse + | OL { out "COM"; block lexbuf; 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 } + | "\\\"" { succ (str lexbuf) } + | UNI { succ (str lexbuf) } + | WRD { succ (str lexbuf) } + | _ { succ (str lexbuf) } +and block = parse + | CL { () } + | OL { block lexbuf; block lexbuf } + | QT { let _ = str lexbuf in block lexbuf } + | _ { block lexbuf } 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' >> $$@