From: Ferruccio Guidi Date: Sat, 29 May 2021 12:18:10 +0000 (+0200) Subject: probe X-Git-Tag: make_still_working~146 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=ea99a55173ebdcfe60f3b3d6f6c979f5d7785d48 probe + improved error handling --- diff --git a/matita/components/binaries/probe/engine.ml b/matita/components/binaries/probe/engine.ml index 8a8a74ac5..345f065fe 100644 --- a/matita/components/binaries/probe/engine.ml +++ b/matita/components/binaries/probe/engine.ml @@ -19,47 +19,38 @@ module B = Librarian module H = HExtlib module M = MacLexer - -let unsupported protocol = - failwith (P.sprintf "probe: unsupported protocol: %s" protocol) - -let missing path = - failwith (P.sprintf "probe: missing path: %s" path) - -let unrooted path roots = - failwith (P.sprintf "probe: missing root: %s (found roots: %u)" path (L.length roots)) +module X = Error let out_int i = P.printf "%u\n" i let out_length uris = out_int (US.cardinal uris) let out_uris uris = - let map uri = P.printf "%S\n" (U.string_of_uri uri) in - US.iter map uris + let map uri = P.printf "%S\n" (U.string_of_uri uri) in + US.iter map uris let is_registry str = - F.check_suffix str ".conf.xml" + F.check_suffix str ".conf.xml" let get_uri str = let str = H.normalize_path str in let dir, file = - 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 - F.concat bdir file, F.concat buri file - | roots -> - if bdir = F.current_dir_name || bdir = F.dir_sep then unrooted dir roots else - aux (F.dirname bdir) (F.concat (F.basename bdir) file) - in - aux dir file + 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 X.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 + F.concat bdir file, F.concat buri file + | roots -> + if bdir = F.current_dir_name || bdir = F.dir_sep then X.unrooted dir roots else + 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 - + 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 5aed03961..432af34c7 100644 --- a/matita/components/binaries/probe/engine.mli +++ b/matita/components/binaries/probe/engine.mli @@ -20,7 +20,3 @@ val mac: string -> unit val is_registry: string -> bool val get_uri: string -> string * string - -val unsupported: string -> 'a - -val missing: string -> 'a diff --git a/matita/components/binaries/probe/error.ml b/matita/components/binaries/probe/error.ml new file mode 100644 index 000000000..598edb19e --- /dev/null +++ b/matita/components/binaries/probe/error.ml @@ -0,0 +1,30 @@ +(* + ||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 L = List +module P = Printf + +exception Error of string + +let error s = + raise (Error s) + +let unsupported protocol = + error (P.sprintf "unsupported protocol: %s" protocol) + +let missing path = + error (P.sprintf "missing path: %s" path) + +let unrooted path roots = + error (P.sprintf "missing root: %s (found roots: %u)" path (L.length roots)) + +let malformed () = + error "malformed term" diff --git a/matita/components/binaries/probe/error.mli b/matita/components/binaries/probe/error.mli new file mode 100644 index 000000000..35bdf830a --- /dev/null +++ b/matita/components/binaries/probe/error.mli @@ -0,0 +1,20 @@ +(* + ||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_______________________________________________________________ *) + +exception Error of string + +val unsupported: string -> 'a + +val missing: string -> 'a + +val unrooted: string -> 'b list -> 'a + +val malformed: unit -> 'a diff --git a/matita/components/binaries/probe/matitaList.ml b/matita/components/binaries/probe/matitaList.ml index d4ea3e584..95250b26c 100644 --- a/matita/components/binaries/probe/matitaList.ml +++ b/matita/components/binaries/probe/matitaList.ml @@ -21,6 +21,7 @@ module H = HExtlib module O = Options module E = Engine +module X = Error let chop_extension file = try F.chop_extension file @@ -88,8 +89,8 @@ let from_uri base devel uri = 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 + else X.missing path + else X.unsupported protocol let from_string base devel 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 5b0a10605..736baafbc 100644 --- a/matita/components/binaries/probe/nCicScan.ml +++ b/matita/components/binaries/probe/nCicScan.ml @@ -19,6 +19,7 @@ module P = NCicPp module E = NCicEnvironment module O = Options +module X = Error type status = { (* current complexity *) @@ -29,9 +30,6 @@ type status = { let status = new P.status -let malformed () = - failwith "probe: malformed term" - let add_name str = let u = U.uri_of_string str in if US.mem u !O.names then Printf.eprintf "probe: name clash: %S\n" str; @@ -86,7 +84,7 @@ let rec scan_term st = function | (_, 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.Appl []) :: tl -> X.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 -> diff --git a/matita/components/binaries/probe/probe.ml b/matita/components/binaries/probe/probe.ml index d118fdab2..897148e97 100644 --- a/matita/components/binaries/probe/probe.ml +++ b/matita/components/binaries/probe/probe.ml @@ -22,27 +22,32 @@ module M = MatitaList module D = MatitaRemove module S = NCicScan module E = Engine +module X = Error let trusted _ = true let no_log _ _ = () let init registry = - R.load_from registry; - if !O.no_init then begin - B.init (); - C.set_trust trusted; - H.set_log_callback no_log; - O.no_init := false; - end + R.load_from registry; + if !O.no_init then begin + B.init (); + C.set_trust trusted; + H.set_log_callback no_log; + O.no_init := false; + end let scan_uri devel str = - M.from_string (R.get "matita.basedir") devel str; - S.scan () + try + M.from_string (R.get "matita.basedir") devel str; + S.scan () + with + | X.Error s -> + Printf.eprintf "probe: %s\n%!" s let scan_from devel = - let devel, uri = E.get_uri devel in - scan_uri devel uri + let devel, uri = E.get_uri devel in + scan_uri devel uri let set_g () = O.exclude := `Generated :: !O.exclude @@ -71,45 +76,45 @@ 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 + if L.is_uri s then scan_uri "" s + else if E.is_registry s then init s + else scan_from s let clear () = - D.objects (); O.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 - let help_nn = " Print the number of names" in - let help_ns = " Print the list of names" 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 [ - "-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; - "-nn", A.Unit out_nn, help_nn; - "-ns", A.Unit out_ns, help_ns; - "-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; - "-sc", A.Unit out_sc, help_sc; - "-sn", A.Unit out_sn, help_sn; - "-ss", A.Unit out_ss, help_ss; - ] process help; - D.objects () + 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 + let help_nn = " Print the number of names" in + let help_ns = " Print the list of names" 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 [ + "-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; + "-nn", A.Unit out_nn, help_nn; + "-ns", A.Unit out_ns, help_ns; + "-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; + "-sc", A.Unit out_sc, help_sc; + "-sn", A.Unit out_sn, help_sn; + "-ss", A.Unit out_ss, help_ss; + ] process help; + D.objects () diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index 8d6f2ccd2..dc13cc156 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -186,7 +186,7 @@ define SUMMARY_TEMPLATE $$(SUM_$(1)): S2 = $$(word 2, $$(C0)) $$(SUM_$(1)): S3 = $$(word 3, $$(C0)) $$(SUM_$(1)): S4 = $$(word 4, $$(C0)) - $$(SUM_$(1)): S5 = $$(shell printf "%.1f" `echo "scale=2;$$(S4)/$$(S2)"|bc`) + $$(SUM_$(1)): S5 = $$(shell printf "%.1f" `echo "scale=2;if($$(S2)!=0)$$(S4)/$$(S2) else 0"|bc`) $$(SUM_$(1)): C1 = $$(word 5, $$(C0)) $$(SUM_$(1)): C2 = $$(word 7, $$(C0)) $$(SUM_$(1)): C3 = $$(shell echo "$$(C1)+$$(C2)"|bc)