-module DB = Dbi_mysql
-
let _ = Helm_registry.set "getter.mode" "remote";
let _ = Helm_registry.set "getter.url" "http://mowgli.cs.unibo.it:58081/" in
-let dbh = new DB.connection ~host:"mowgli.cs.unibo.it" ~user:"helm" "matita" in
+let dbd =
+ Mysql.quick_connect ~host:"mowgli.cs.unibo.it" ~user:"helm" ~database:"matita"
+ ()
+in
let owner =
try
Sys.argv.(2)
with Invalid_argument _ -> "matita_test"
in
-if Sys.argv.(1) = "clean" then
- MetadataDb.clean ~dbh ~owner
-else
- let uri_str = Sys.argv.(1) in
- let uri = UriManager.uri_of_string uri_str in
- match CicEnvironment.get_obj uri with
- | Cic.Constant (_, body, ty, _) ->
- MetadataDb.index_constant ~body ~ty ~uri ~owner ~dbh
- | Cic.InductiveDefinition (types, _, _) ->
- MetadataDb.index_inductive_def ~dbh ~owner ~uri ~types
- | _ -> assert false
+let _ = MetadataTypes.ownerize_tables owner in
+if Sys.argv.(1) = "clean" then begin
+ prerr_endline "foo";
+ ignore (MetadataDb.clean ~dbd)
+end else
+ let fname = Sys.argv.(1) in
+ let n = ref 0 in
+ let ic = open_in fname in
+ try
+ while true do
+ let line = input_line ic in
+ 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)
+ done
+ with End_of_file -> close_in ic