helm/software/components/ng_kernel/check.ml

   1 let debug = true
   2 let ignore_exc = false
   3 let rank_all_dependencies = true
   4 let trust_environment = false
   5
   6 let indent = ref 0;;
   7
   8 let logger =
   9     let do_indent () = String.make !indent ' ' in
  10     (function
  11     | `Start_type_checking s -> ();
  12         if debug then
  13          prerr_endline (do_indent () ^ "Start: " ^ NUri.string_of_uri s);
  14         incr indent
  15
  16     | `Type_checking_completed s ->  ();
  17         decr indent;
  18         if debug then
  19          prerr_endline (do_indent () ^ "End: " ^ NUri.string_of_uri s))
  20 ;;
  21
  22 let _ =
  23   HelmLogger.register_log_callback
  24    (fun ?append_NL html_msg ->
  25      prerr_endline (HelmLogger.string_of_html_msg html_msg));
  26   CicParser.impredicative_set := false;
  27   NCicTypeChecker.set_logger logger;
  28   NCicPp.set_ppterm NCicPp.trivial_pp_term;
  29   Helm_registry.load_from "conf.xml";
  30   let alluris =
  31     try
  32       let s = Sys.argv.(1) in
  33       if s = "-alluris" then
  34        begin
  35         let uri_re = Str.regexp ".*\\(ind\\|con\\)$" in
  36         let uris = Http_getter.getalluris () in
  37         let alluris = List.filter (fun u -> Str.string_match uri_re u 0) uris in
  38         let oc = open_out "alluris.txt" in
  39         List.iter (fun s -> output_string oc (s^"\n")) alluris;
  40         close_out oc;
  41         []
  42        end
  43       else [s]
  44     with Invalid_argument _ ->
  45       let r = ref [] in
  46       let ic = open_in "alluris.txt" in
  47       try while true do r := input_line ic :: !r; done; []
  48       with _ -> List.rev !r
  49   in
  50   let alluris =
  51     HExtlib.filter_map
  52       (fun u -> try Some (UriManager.uri_of_string u) with _ -> None) alluris
  53   in
  54   (* brutal *)
  55   prerr_endline "computing graphs to load...";
  56   let roots_alluris =
  57    if not rank_all_dependencies then
  58     alluris
  59    else (
  60     let dbd = HSql.quick_connect (LibraryDb.parse_dbd_conf ()) in
  61      MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
  62     let uniq l =
  63      HExtlib.list_uniq (List.sort UriManager.compare l) in
  64     let who_uses u =
  65      uniq (List.map (fun (uri,_) -> UriManager.strip_xpointer uri)
  66       (MetadataDeps.inverse_deps ~dbd u)) in
  67     let rec fix acc l =
  68      let acc, todo =
  69       List.fold_left (fun (acc,todo) x ->
  70         let w = who_uses x in
  71         if w = [] then (x::acc,todo) else (acc,uniq (todo@w)))
  72       (acc,[]) l
  73      in
  74      if todo = [] then uniq acc else fix acc todo
  75     in
  76      fix [] alluris)
  77   in
  78   prerr_endline "generating Coq graphs...";
  79   CicEnvironment.set_trust (fun _ -> trust_environment);
  80   List.iter
  81    (fun u ->
  82      prerr_endline (" - " ^ UriManager.string_of_uri u);
  83      try
  84        ignore(CicTypeChecker.typecheck u);
  85      with
  86      | CicTypeChecker.AssertFailure s
  87      | CicTypeChecker.TypeCheckerFailure s ->
  88         prerr_endline (Lazy.force s);
  89         assert false
  90     ) roots_alluris;
  91   prerr_endline "loading...";
  92   List.iter
  93     (fun u ->
  94        prerr_endline ("  - "^UriManager.string_of_uri u);
  95        try NCicEnvironment.load_graph u with exn -> ())
  96     roots_alluris;
  97   prerr_endline "finished....";
  98   CicUniv.do_rank (NCicEnvironment.get_graph ());
  99   prerr_endline "caching objects";
 100   prerr_endline "ranked....";
 101   HExtlib.profiling_enabled := false;
 102   List.iter (fun uu ->
 103      let uu= NUri.nuri_of_ouri uu in
 104      indent := 0;
 105      logger (`Start_type_checking uu);
 106     let _,o = NCicEnvironment.get_obj uu in
 107     try
 108       NCicTypeChecker.typecheck_obj o;
 109       logger (`Type_checking_completed uu);
 110     with
 111     | NCicTypeChecker.AssertFailure s
 112     | NCicTypeChecker.TypeCheckerFailure s as e ->
 113        prerr_endline ("######### " ^ Lazy.force s);
 114        if not ignore_exc then raise e
 115     | CicEnvironment.Object_not_found s ->
 116        prerr_endline ("Obj not found: " ^ UriManager.string_of_uri s)
 117     )
 118     alluris;
 119   NCicEnvironment.invalidate ();
 120   Gc.compact ();
 121   HExtlib.profiling_enabled := true;
 122   NCicTypeChecker.set_logger (fun _ -> ());
 123   prerr_endline "typechecking, first with the new and then with the old kernel";
 124   let prima = Unix.gettimeofday () in
 125   List.iter
 126     (fun u ->
 127        let u= NUri.nuri_of_ouri u in
 128       indent := 0;
 129       NCicTypeChecker.typecheck_obj (snd (NCicEnvironment.get_obj u)))
 130     alluris;
 131   let dopo = Unix.gettimeofday () in
 132   Gc.compact ();
 133   let dopo2 = Unix.gettimeofday () in
 134   Printf.eprintf "NEW typing: %3.2f, gc: %3.2f\n%!" (dopo -. prima) (dopo2 -.  dopo);
 135   CicEnvironment.invalidate ();
 136   Gc.compact ();
 137   let prima = Unix.gettimeofday () in
 138   List.iter (fun u -> ignore (CicTypeChecker.typecheck u)) alluris;
 139   let dopo = Unix.gettimeofday () in
 140   Gc.compact ();
 141   let dopo2 = Unix.gettimeofday () in
 142   Printf.eprintf "OLD typing: %3.2f, gc: %3.2f\n%!" (dopo -. prima) (dopo2 -. dopo)
 143 ;;