From 8f2b388ed93eca7de9a9fe70eaf2e0ab2588e6b7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 7 Apr 2008 16:18:52 +0000 Subject: [PATCH] added comparison with old kernel --- helm/software/components/ng_kernel/check.ml | 46 ++++++++++++++++----- 1 file changed, 35 insertions(+), 11 deletions(-) diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml index 68c9ff1ae..4bcff60d4 100644 --- a/helm/software/components/ng_kernel/check.ml +++ b/helm/software/components/ng_kernel/check.ml @@ -1,10 +1,11 @@ let _ = NCicTypeChecker.set_logger (function - | `Start_type_checking s -> - prerr_endline ("Start: " ^ NUri.string_of_uri s) - | `Type_checking_completed s -> - prerr_endline ("End: " ^ NUri.string_of_uri s)); + | `Start_type_checking s -> () +(* prerr_endline ("Start: " ^ NUri.string_of_uri s) *) + | `Type_checking_completed s -> () +(* prerr_endline ("End: " ^ NUri.string_of_uri s) *) + ); NCicPp.set_ppterm NCicPp.trivial_pp_term; Helm_registry.load_from "conf.xml"; let alluris = @@ -27,14 +28,18 @@ let _ = try while true do r := input_line ic :: !r; done; [] with _ -> List.rev !r in + let alluris = + HExtlib.filter_map + (fun u -> try Some (NUri.nuri_of_ouri (UriManager.uri_of_string u)) with _ + -> None) alluris + in + prerr_endline "caching objects"; List.iter (fun uu -> - if uu.[0] = '#' then prerr_endline "SKIP" else begin - prerr_endline ("************* INIZIO **************** " ^ uu); - let u = UriManager.uri_of_string uu in - let _,o = NCicEnvironment.get_obj (NUri.nuri_of_ouri u) in +(* prerr_endline ("************* INIZIO **************** " ^ uu); *) + let _,o = NCicEnvironment.get_obj uu in try NCicTypeChecker.typecheck_obj o; - prerr_endline ("************* FINE ****************" ^ uu); +(* prerr_endline ("************* FINE ****************" ^ uu); *) with | NCicTypeChecker.AssertFailure s | NCicTypeChecker.TypeCheckerFailure s as e -> @@ -42,6 +47,25 @@ let _ = prerr_endline (Lazy.force s); raise e | CicEnvironment.Object_not_found s -> prerr_endline ("Obj not found: " ^ UriManager.string_of_uri s); - end) - alluris + ) + alluris; + NCicEnvironment.invalidate (); + Gc.compact (); + let prima = Unix.gettimeofday () in + List.iter + (fun u -> NCicTypeChecker.typecheck_obj (snd (NCicEnvironment.get_obj u))) + alluris; + let dopo = Unix.gettimeofday () in + Gc.compact (); + let dopo2 = Unix.gettimeofday () in + Printf.eprintf "NEW typing: %3.2f, gc: %3.2f\n" (dopo -. prima) (dopo2 -. dopo); + CicEnvironment.invalidate (); + let alluris = List.map NUri.ouri_of_nuri alluris in + Gc.compact (); + let prima = Unix.gettimeofday () in + List.iter (fun u -> ignore (CicTypeChecker.typecheck u)) alluris; + let dopo = Unix.gettimeofday () in + Gc.compact (); + let dopo2 = Unix.gettimeofday () in + Printf.eprintf "OLD typing: %3.2f, gc: %3.2f\n" (dopo -. prima) (dopo2 -. dopo) ;; -- 2.39.2