More options can now be set at the beginning of the file.

diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml
index 5205274733494cda2585cbd6c59aafca03900c70..132ce5b7f350ea0ef660f9b8448ca7bdcfdda5e4 100644 (file)
--- a/helm/software/components/ng_kernel/check.ml
+++ b/helm/software/components/ng_kernel/check.ml
@@ -1,5 +1,7 @@
-let debug = false
+let debug = true
 let ignore_exc = false
+let rank_all_dependencies = true
+let trust_environment = false
 
 let indent = ref 0;;
 
@@ -18,6 +20,9 @@ let logger =
 ;;
 
 let _ =
+  HelmLogger.register_log_callback
+   (fun ?append_NL html_msg ->
+     prerr_endline (HelmLogger.string_of_html_msg html_msg));
   CicParser.impredicative_set := false;
   NCicTypeChecker.set_logger logger;
   NCicPp.set_ppterm NCicPp.trivial_pp_term;
@@ -48,41 +53,40 @@ 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 (fun (uri,_) -> UriManager.strip_xpointer uri)
-     (MetadataDeps.inverse_deps ~dbd u)) in
   let roots_alluris = 
-   let rec fix acc l = 
-    let acc, todo = 
-     List.fold_left (fun (acc,todo) x ->
+   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
+      (acc,[]) l
+     in
+     if todo = [] then uniq acc else fix acc todo
     in
-    if todo = [] then uniq acc else fix acc todo
-   in
-   (fix [] alluris)
+     fix [] alluris)
   in
-(*
- BARO!
-  let roots_alluris = alluris in *)
   prerr_endline "generating Coq graphs...";
-  (* per barare *)
-   let roots_alluris = alluris in
-  (* /per barare *)
-  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