X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2Fcheck.ml;h=28aeb16c8da1b338fd93bcd3e5b66dc80c227eff;hb=c622da7bd4b14f5953424e09f32c14f74d681a3f;hp=c9c0bd37b7973a65d1dee0cbc82fd44d8b967c1c;hpb=fcdc755773839176c7206b579b6dd1ff665ed8f5;p=helm.git diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml index c9c0bd37b..28aeb16c8 100644 --- a/helm/software/components/ng_kernel/check.ml +++ b/helm/software/components/ng_kernel/check.ml @@ -1,16 +1,47 @@ -let _ = - let indent = ref 0 in -(* let do_indent () = String.make !indent ' ' in *) - NCicTypeChecker.set_logger +let debug = true +let ignore_exc = false +let rank_all_dependencies = true +let trust_environment = false + +let indent = ref 0;; + +let load_graph, get_graph = + let oldg = ref CicUniv.empty_ugraph in + (function uri -> + let _,g = CicEnvironment.get_obj !oldg uri in + oldg := g), + (function _ -> !oldg) +;; + +let logger = + let do_indent () = String.make !indent ' ' in (function - | `Start_type_checking s -> (); -(* prerr_endline (do_indent () ^ "Start: " ^ NUri.string_of_uri s); *) - incr indent + | `Start_type_checking s -> + if debug then + prerr_endline (do_indent () ^ "Start: " ^ NUri.string_of_uri s); + incr indent + | `Type_checking_completed s -> + decr indent; + if debug then + prerr_endline (do_indent () ^ "End: " ^ NUri.string_of_uri s) + | `Type_checking_interrupted s -> + decr indent; + if debug then + prerr_endline (do_indent () ^ "Break: " ^ NUri.string_of_uri s) + | `Type_checking_failed s -> + decr indent; + if debug then + prerr_endline (do_indent () ^ "Fail: " ^ NUri.string_of_uri s)) +;; - | `Type_checking_completed s -> (); - decr indent; -(* prerr_endline (do_indent () ^ "End: " ^ NUri.string_of_uri s) *) - ); +let _ = + let do_old_logging = ref true in + HelmLogger.register_log_callback + (fun ?append_NL html_msg -> + if !do_old_logging then + prerr_endline (HelmLogger.string_of_html_msg html_msg)); + CicParser.impredicative_set := false; + NCicTypeChecker.set_logger logger; NCicPp.set_ppterm NCicPp.trivial_pp_term; Helm_registry.load_from "conf.xml"; let alluris = @@ -39,75 +70,79 @@ let _ = in (* brutal *) prerr_endline "computing graphs to load..."; - let dbd = HSql.quick_connect (LibraryDb.parse_dbd_conf ()) in - MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); - let uniq l = - HExtlib.list_uniq (List.sort UriManager.compare l) - in - let who_uses u = - uniq (List.map fst (MetadataDeps.inverse_deps ~dbd u)) - in let roots_alluris = - let rec fix acc l = - let acc, todo = - List.fold_left (fun (acc,todo) x -> - let w = who_uses x in - if w = [] then (x::acc,todo) else (acc,uniq (todo@w))) - (acc,[]) l - in - if todo = [] then uniq acc else fix acc todo - in - (fix [] alluris) + if not rank_all_dependencies then + alluris + else ( + let dbd = HSql.quick_connect (LibraryDb.parse_dbd_conf ()) in + MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); + let uniq l = + HExtlib.list_uniq (List.sort UriManager.compare l) in + let who_uses u = + uniq (List.map (fun (uri,_) -> UriManager.strip_xpointer uri) + (MetadataDeps.inverse_deps ~dbd u)) in + let rec fix acc l = + let acc, todo = + List.fold_left (fun (acc,todo) x -> + let w = who_uses x in + if w = [] then (x::acc,todo) else (acc,uniq (todo@w))) + (acc,[]) l + in + if todo = [] then uniq acc else fix acc todo + in + fix [] alluris) in prerr_endline "generating Coq graphs..."; - CicEnvironment.set_trust (fun _ -> false); - List.iter (fun u -> - prerr_endline (" - " ^ UriManager.string_of_uri u); - try - ignore(CicTypeChecker.typecheck u); - with - | CicTypeChecker.AssertFailure s - | CicTypeChecker.TypeCheckerFailure s -> prerr_endline (Lazy.force s) + CicEnvironment.set_trust (fun _ -> trust_environment); + List.iter + (fun u -> + prerr_endline (" - " ^ UriManager.string_of_uri u); + try + ignore(CicTypeChecker.typecheck u); + with + | CicTypeChecker.AssertFailure s + | CicTypeChecker.TypeCheckerFailure s -> + prerr_endline (Lazy.force s); + assert false ) roots_alluris; prerr_endline "loading..."; List.iter (fun u -> prerr_endline (" - "^UriManager.string_of_uri u); - try NCicEnvironment.load_graph u with exn -> ()) + try load_graph u with exn -> ()) roots_alluris; prerr_endline "finished...."; - CicUniv.do_rank (NCicEnvironment.get_graph ()); - prerr_endline "ranked...."; + CicUniv.do_rank (get_graph ()); prerr_endline "caching objects"; + prerr_endline "ranked...."; HExtlib.profiling_enabled := false; List.iter (fun uu -> - let uu= NUri.nuri_of_ouri uu in - indent := 0; -(* prerr_endline ("************* INIZIO **************** " ^ NUri.string_of_uri uu); *) - let _,o = NCicEnvironment.get_obj uu in -(* prerr_endline (NCicPp.ppobj o); *) + let uu= NUri.nuri_of_ouri uu in + indent := 0; + let o = NCicLibrary.get_obj uu in try - NCicTypeChecker.typecheck_obj o; -(* prerr_endline ("************* FINE ****************" ^ NUri.string_of_uri uu); *) + NCicTypeChecker.typecheck_obj o with | NCicTypeChecker.AssertFailure s | NCicTypeChecker.TypeCheckerFailure s as e -> -(* prerr_endline ("Obj: " ^ NCicPp.ppobj o); *) - prerr_endline ("######### " ^ Lazy.force s); raise e + prerr_endline ("######### " ^ Lazy.force s); + if not ignore_exc then raise e | CicEnvironment.Object_not_found s -> - prerr_endline ("Obj not found: " ^ UriManager.string_of_uri s); + prerr_endline ("Obj not found: " ^ UriManager.string_of_uri s) ) alluris; NCicEnvironment.invalidate (); Gc.compact (); HExtlib.profiling_enabled := true; + NCicTypeChecker.set_logger (fun _ -> ()); + do_old_logging := false; prerr_endline "typechecking, first with the new and then with the old kernel"; let prima = Unix.gettimeofday () in List.iter (fun u -> let u= NUri.nuri_of_ouri u in indent := 0; - NCicTypeChecker.typecheck_obj (snd (NCicEnvironment.get_obj u))) + NCicTypeChecker.typecheck_obj (NCicLibrary.get_obj u)) alluris; let dopo = Unix.gettimeofday () in Gc.compact ();