From e299c8aad16752ea008cbb8a673996652b548e30 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 14 Apr 2008 14:59:12 +0000 Subject: [PATCH] objects are typechecked to ensure there is a graph before doing all the stuff... read: much more memory is required --- helm/software/components/ng_kernel/check.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml index 513612f9b..6e2074db0 100644 --- a/helm/software/components/ng_kernel/check.ml +++ b/helm/software/components/ng_kernel/check.ml @@ -38,7 +38,7 @@ let _ = (fun u -> try Some (UriManager.uri_of_string u) with _ -> None) alluris in (* brutal *) - prerr_endline "loading graphs..."; + 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 = @@ -59,6 +59,13 @@ let _ = 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); + ignore(CicTypeChecker.typecheck u); + ) alluris; + prerr_endline "loading..."; List.iter (fun u -> prerr_endline (" - "^UriManager.string_of_uri u); -- 2.39.2