test_instance.ma

[helm.git] / helm / ocaml / metadata / test.ml

diff --git a/helm/ocaml/metadata/test.ml b/helm/ocaml/metadata/test.ml
index 21274a585e37020c4652a1f865439191e8f3b9ed..a7040e6598c14d9cc643f8229fda0ba8da3bbcd5 100644 (file)
--- a/helm/ocaml/metadata/test.ml
+++ b/helm/ocaml/metadata/test.ml
@@ -1,6 +1,16 @@
 
-let _ = Helm_registry.set "getter.mode" "remote";
-let _ = Helm_registry.set "getter.url" "http://mowgli.cs.unibo.it:58081/" in
+
+let _ = Helm_registry.set "getter.mode" "local" in
+
+let _ = Helm_registry.set "getter.servers"
+            "file:///projects/helm/library/coq_contribs" in
+let _ = Helm_registry.set "getter.cache_dir" "." in
+let _ = Helm_registry.set "getter.maps_dir" "." in
+let _ = Helm_registry.set "getter.dtd_dir" "/projects/helm/xml/dtd" in
+
+let _ = Http_getter.init () in
+(* let _ = Http_getter.update () in *)
+
 let dbd =
   Mysql.quick_connect ~host:"mowgli.cs.unibo.it" ~user:"helm" ~database:"matita"
     ()
@@ -8,7 +18,7 @@ in
 let owner =
   try
     Sys.argv.(2)
-  with Invalid_argument _ -> "matita_test"
+  with Invalid_argument _ -> "matita_test2"
 in
 let _ = MetadataTypes.ownerize_tables owner in
 if Sys.argv.(1) = "clean" then begin
@@ -24,14 +34,12 @@ end else
       incr n;
       Printf.printf "%d\t%s\n" !n line; flush stdout;
       let uri = UriManager.uri_of_string line in
-      (match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
-      | Cic.Constant (_, body, ty, _, _), _ ->
-          MetadataDb.index_constant ~body ~ty ~uri ~dbd
-      | Cic.Variable (_, body, ty, _, _), _ ->
-          MetadataDb.index_constant ~body ~ty ~uri ~dbd
-      | Cic.InductiveDefinition (types, _, _, _), _ ->
-          MetadataDb.index_inductive_def ~dbd ~uri ~types
-      | _ -> assert false)
+      MetadataDb.index_obj ~dbd ~uri
     done
-  with End_of_file -> close_in ic
+  with 
+  | _ -> 
+    prerr_endline 
+      ("total persing time " ^ 
+         (string_of_float !CicEnvironment.total_parsing_time)); 
+    close_in ic