From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 14 Apr 2008 14:59:12 +0000 (+0000)
Subject: objects are typechecked to ensure there is a graph before doing all the stuff...... 
X-Git-Tag: make_still_working~5339
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e299c8aad16752ea008cbb8a673996652b548e30;p=helm.git

objects are typechecked to ensure there is a graph before doing all the stuff... read: much more memory is required
---

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);