let _ =
- NCicTypeChecker.set_logger
+ let indent = ref 0 in
+(* let do_indent () = String.make !indent ' ' in *)
+ 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 (do_indent () ^ "Start: " ^ NUri.string_of_uri s);
+ incr indent
+*)
+ | `Type_checking_completed s -> ();
+(*
+ decr indent;
+ prerr_endline (do_indent () ^ "End: " ^ NUri.string_of_uri s)
+*)
+ );
NCicPp.set_ppterm NCicPp.trivial_pp_term;
Helm_registry.load_from "conf.xml";
let alluris =
let s = Sys.argv.(1) in
if s = "-alluris" then
begin
- let uri_re = Str.regexp ".*\\(ind\\|var\\|con\\)$" in
+ let uri_re = Str.regexp ".*\\(ind\\|con\\)$" in
let uris = Http_getter.getalluris () in
let alluris = List.filter (fun u -> Str.string_match uri_re u 0) uris in
let oc = open_out "alluris.txt" in
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";
+ HExtlib.profiling_enabled := false;
List.iter (fun uu ->
- prerr_endline ("************* INIZIO **************** " ^ uu);
- let u = UriManager.uri_of_string uu in
- let _,o = NCicEnvironment.get_obj (NUri.nuri_of_ouri u) in
+ indent := 0;
+(* prerr_endline ("************* INIZIO **************** " ^ NUri.string_of_uri uu); *)
+ let _,o = NCicEnvironment.get_obj uu in
try
NCicTypeChecker.typecheck_obj o;
- prerr_endline ("************* FINE ****************" ^ uu);
+(* prerr_endline ("************* FINE ****************" ^ NUri.string_of_uri uu); *)
with
| NCicTypeChecker.AssertFailure s
| NCicTypeChecker.TypeCheckerFailure s as e ->
- prerr_endline (Lazy.force s); raise e
+(* prerr_endline ("Obj: " ^ NCicPp.ppobj o); *)
+ prerr_endline ("######### " ^ Lazy.force s); raise e
| CicEnvironment.Object_not_found s ->
- prerr_endline ("Obj not found: " ^ UriManager.string_of_uri s))
- alluris
+ prerr_endline ("Obj not found: " ^ UriManager.string_of_uri s);
+ )
+ alluris;
+ NCicEnvironment.invalidate ();
+ Gc.compact ();
+ HExtlib.profiling_enabled := true;
+ prerr_endline "typechecking, first with the new and then with the old kernel";
+ let prima = Unix.gettimeofday () in
+ List.iter
+ (fun u ->
+ indent := 0;
+ 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)
;;