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