From 2b53a3735b2a6130726e0a0451993cd679fd5935 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 18 Sep 2008 14:36:52 +0000 Subject: [PATCH] librarian: improved error detection, bug fix in time comparison functions: now the object files are considered in the correct compilation order even if they mtime is the same :) Procedural: improved error detection --- .../acic_procedural/acic2Procedural.ml | 18 ++-- .../acic_procedural/acic2Procedural.mli | 2 + .../acic_procedural/proceduralHelpers.ml | 11 --- .../acic_procedural/proceduralHelpers.mli | 2 - .../acic_procedural/proceduralOptimizer.ml | 7 +- helm/software/components/library/librarian.ml | 84 ++++++++++++------- .../software/components/library/librarian.mli | 4 + 7 files changed, 74 insertions(+), 54 deletions(-) diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index ce6316de1..071377c63 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -39,6 +39,7 @@ module PEH = ProofEngineHelpers module HEL = HExtlib module DTI = DoubleTypeInference module NU = CicNotationUtil +module L = Librarian module Cl = ProceduralClassify module T = ProceduralTypes @@ -54,7 +55,7 @@ type status = { case: int list } -let debug = false +let debug = ref false (* helpers ******************************************************************) @@ -194,7 +195,7 @@ let mk_convert st ?name sty ety note = let e = Cn.hole "" in let csty, cety = H.cic sty, H.cic ety in let script = - if debug then + if !debug then let sname = match name with None -> "" | Some (id, _) -> id in let note = Printf.sprintf "%s: %s\nSINTH: %s\nEXP: %s" note sname (Pp.ppterm csty) (Pp.ppterm cety) @@ -218,7 +219,7 @@ let mk_convert st ?name sty ety note = let convert st ?name v = match get_inner_types st v with | None -> - if debug then [T.Note "NORMAL: NO INNER TYPES"] else [] + if !debug then [T.Note "NORMAL: NO INNER TYPES"] else [] | Some (sty, ety) -> mk_convert st ?name sty ety "NORMAL" let convert_elim st ?name t v pattern = @@ -341,7 +342,10 @@ and proc_const st what = and proc_appl st what hd tl = let proceed, dtext = test_depth st in let script = if proceed then - let ty = get_type "TC2" st hd in + let ty = match get_inner_types st hd with + | Some (ity, _) -> H.cic ity + | None -> get_type "TC2" st hd + in let classes, rc = Cl.classify st.context ty in let goal_arity, goal = match get_inner_types st what with | None -> 0, None @@ -489,13 +493,13 @@ let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types ?depth context = []; case = [] } in - H.print_times "LEVEL 2"; + L.time_stamp "P : LEVEL 2 "; HLog.debug "Procedural: level 2 transformation"; let steps = proc_obj st ?flavour anobj in - H.print_times "RENDERING"; + L.time_stamp "P : RENDERING"; HLog.debug "Procedural: grafite rendering"; let r = List.rev (T.render_steps [] steps) in - H.print_times "DONE "; r + L.time_stamp "P : DONE "; r let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix context annterm = diff --git a/helm/software/components/acic_procedural/acic2Procedural.mli b/helm/software/components/acic_procedural/acic2Procedural.mli index f0016cce2..852bc05a5 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.mli +++ b/helm/software/components/acic_procedural/acic2Procedural.mli @@ -38,3 +38,5 @@ val procedural_of_acic_term: (Cic.annterm, Cic.annterm, Cic.annterm GrafiteAst.reduction, Cic.annterm CicNotationPt.obj, string) GrafiteAst.statement list + +val debug: bool ref diff --git a/helm/software/components/acic_procedural/proceduralHelpers.ml b/helm/software/components/acic_procedural/proceduralHelpers.ml index 54b115aa2..91f7016cd 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.ml +++ b/helm/software/components/acic_procedural/proceduralHelpers.ml @@ -35,17 +35,6 @@ module D = Deannotate module PER = ProofEngineReduction module Ut = CicUtil -(* time stamping ************************************************************) - -let print_times = - let old = ref 0.0 in - fun msg -> - let times = Unix.times () in - let stamp = times.Unix.tms_utime +. times.Unix.tms_utime in - let lap = stamp -. !old in - Printf.eprintf "TIME STAMP: %s: %f\n" msg lap; flush stdout; - old := stamp - (* raw cic prettyprinter ****************************************************) let xiter out so ss sc map l = diff --git a/helm/software/components/acic_procedural/proceduralHelpers.mli b/helm/software/components/acic_procedural/proceduralHelpers.mli index 239c789c2..6b90e815c 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.mli +++ b/helm/software/components/acic_procedural/proceduralHelpers.mli @@ -23,8 +23,6 @@ * http://cs.unibo.it/helm/. *) -val print_times: - string -> unit val pp_term: (string -> unit) -> Cic.metasenv -> Cic.context -> Cic.term -> unit val mk_fresh_name: diff --git a/helm/software/components/acic_procedural/proceduralOptimizer.ml b/helm/software/components/acic_procedural/proceduralOptimizer.ml index c5958575a..3ac567095 100644 --- a/helm/software/components/acic_procedural/proceduralOptimizer.ml +++ b/helm/software/components/acic_procedural/proceduralOptimizer.ml @@ -34,6 +34,7 @@ module HEL = HExtlib module PEH = ProofEngineHelpers module TC = CicTypeChecker module Un = CicUniv +module L = Librarian module H = ProceduralHelpers module Cl = ProceduralClassify @@ -285,11 +286,11 @@ let optimize_obj = function prerr_string "H.pp_term : "; H.pp_term prerr_string [] [] bo; prerr_newline () end; - let _ = H.get_type "opt" [] (C.Cast (bo, ty)) in - H.print_times ("OPTIMIZED: " ^ name); +(* let _ = H.get_type "opt" [] (C.Cast (bo, ty)) in *) + L.time_stamp ("PO: DONE " ^ name); C.Constant (name, Some bo, ty, pars, attrs) in - H.print_times ("BEGIN : " ^ name); + L.time_stamp ("PO: OPTIMIZING " ^ name); if !debug then Printf.eprintf "BEGIN: %s\nPre Nodes : %u\n" name (I.count_nodes 0 bo); diff --git a/helm/software/components/library/librarian.ml b/helm/software/components/library/librarian.ml index 32b6de48b..b0c601f1f 100644 --- a/helm/software/components/library/librarian.ml +++ b/helm/software/components/library/librarian.ml @@ -23,14 +23,18 @@ * http://helm.cs.unibo.it/ *) -let debug = false;; - -let timestamp msg = - if debug then - let times = Unix.times () in - let utime = times.Unix.tms_utime in - let msg = Printf.sprintf "UTIMESTAMP (%s): %f" msg utime in - prerr_endline msg +let debug = ref true + +let time_stamp = + let old = ref 0.0 in + fun msg -> + if !debug then begin + let times = Unix.times () in + let stamp = times.Unix.tms_utime +. times.Unix.tms_stime in + let lap = stamp -. !old in + Printf.eprintf "TIME STAMP (%s): %f\n" msg lap; flush stderr; + old := stamp + end exception NoRootFor of string @@ -198,13 +202,15 @@ module Make = functor (F:Format) -> struct type status = Done of bool | Ready of bool - let say s = if debug then prerr_endline ("make: "^s);; + let say s = if !debug then prerr_endline ("make: "^s);; let unopt_or_call x f y = match x with Some _ -> x | None -> f y;; let fst4 = function (x,_,_,_) -> x;; let modified_before_s_t (_,cs, ct, _, _) a b = + prerr_endline ("L s_t: a " ^ F.string_of_source_object a); + prerr_endline ("L s_t: b " ^ F.string_of_target_object b); let a = try Hashtbl.find cs a with Not_found -> assert false in let b = try @@ -218,20 +224,24 @@ module Make = functor (F:Format) -> struct | x -> x with Not_found -> assert false in - match a, b with - | Some a, Some b -> a < b - | _ -> false - ;; + let r = match a, b with + | Some a, Some b -> a <= b + | _ -> false + in + prerr_endline ("L s_t: " ^ string_of_bool r); r let modified_before_t_t (_,_,ct, _, _) a b = - let a = +(* + prerr_endline ("L t_t: a " ^ F.string_of_target_object a); + prerr_endline ("L t_t: b " ^ F.string_of_target_object b); +*) let a = try match Hashtbl.find ct a with | Some _ as x -> x | None -> - match F.mtime_of_target_object a with + match F.mtime_of_target_object a with | Some t as x -> - Hashtbl.remove ct a; + Hashtbl.remove ct a; Hashtbl.add ct a x; x | x -> x with Not_found -> assert false @@ -243,15 +253,21 @@ module Make = functor (F:Format) -> struct | None -> match F.mtime_of_target_object b with | Some t as x -> - Hashtbl.remove ct b; + Hashtbl.remove ct b; Hashtbl.add ct b x; x | x -> x with Not_found -> assert false in - match a, b with - | Some a, Some b -> a < b + let r = match a, b with + | Some a, Some b -> +(* + prerr_endline ("tt: a " ^ string_of_float a); + prerr_endline ("tt: b " ^ string_of_float b); +*) + a <= b | _ -> false - ;; + in + prerr_endline ("L t_t: " ^ string_of_bool r); r let rec purge_unwanted_roots wanted deps = let roots, rest = @@ -317,13 +333,13 @@ module Make = functor (F:Format) -> struct aux [] [] l let rec make_aux root (lo,_,ct, cc, _ as opts) ok deps = - timestamp "filter get_status: begin"; + time_stamp "filter get_status: begin"; let map what = match get_status opts what with | Done _ -> None | Ready b -> Some b in let todo, deps = list_partition_filter_rev map deps in - timestamp "filter get_status: end"; + time_stamp "filter get_status: end"; let todo = let local, remote = List.partition (fun (_,_,froot,_) -> froot = Some root) todo @@ -343,9 +359,9 @@ module Make = functor (F:Format) -> struct | Some froot when froot = root -> Hashtbl.remove ct tgt; Hashtbl.add ct tgt None; - timestamp "building"; + time_stamp "building"; let r = F.build lo file in - timestamp "done"; r + time_stamp "done"; r | Some froot -> make froot [file] | None -> HLog.error ("No root for: "^F.string_of_source_object file); @@ -369,26 +385,31 @@ module Make = functor (F:Format) -> struct and make_one root opts ok what = let lo, _, ct, cc, cd = opts in let t, deps, froot, tgt = what in + let str = F.string_of_source_object t in let map (okd, okt) d = let (_, _, _, tgtd) as whatd = (Hashtbl.find cd d) in - make_one root opts okd whatd, okt && modified_before_t_t opts tgtd tgt + let r = make_one root opts okd whatd in + r, okt && modified_before_t_t opts tgtd tgt in - try ok && Hashtbl.find cc t + prerr_endline ("L : processing " ^ str); + try + let r = Hashtbl.find cc t in + prerr_endline ("L : " ^ string_of_bool r ^ " " ^ str); + ok && r (* say "already built" *) with Not_found -> let okd, okt = List.fold_left map (true, modified_before_s_t opts t tgt) deps in let res = if okd then if okt then true else - let str = F.string_of_source_object t in match froot with | Some froot when froot = root -> if is_not_ro opts what then begin Hashtbl.remove ct tgt; Hashtbl.add ct tgt None; - timestamp "building"; + time_stamp ("L : BUILDING " ^ str); let res = F.build lo t in - timestamp "done"; res + time_stamp ("L : DONE " ^ str); res end else begin HLog.warn("Read only baseuri for: "^ str); false end @@ -397,12 +418,13 @@ module Make = functor (F:Format) -> struct HLog.error ("No root for: " ^ str); false else false in + prerr_endline ("L : " ^ string_of_bool res ^ " " ^ str); Hashtbl.add cc t res; ok && res (****************************************************************************) and make root targets = - timestamp "entering"; + time_stamp "L : ENTERING"; HLog.debug ("Entering directory '"^root^"'"); let old_root = Sys.getcwd () in Sys.chdir root; @@ -433,7 +455,7 @@ module Make = functor (F:Format) -> struct in HLog.debug ("Leaving directory '"^root^"'"); Sys.chdir old_root; - timestamp "leaving"; + time_stamp "L : LEAVING"; ok ;; diff --git a/helm/software/components/library/librarian.mli b/helm/software/components/library/librarian.mli index 0c74f3ea5..f448e52b5 100644 --- a/helm/software/components/library/librarian.mli +++ b/helm/software/components/library/librarian.mli @@ -96,3 +96,7 @@ val write_deps_file: string option -> (string * string list) list -> unit (* true if the argunent starts with a uri scheme prefix *) val is_uri: string -> bool + +val debug: bool ref + +val time_stamp: string -> unit -- 2.39.2