helm/ocaml/metadata/test.ml

   1
   2 module DB = Dbi_mysql
   3
   4 let _ = Helm_registry.set "getter.mode" "remote";
   5 let _ = Helm_registry.set "getter.url" "http://mowgli.cs.unibo.it:58081/" in
   6 let dbh = new DB.connection ~host:"mowgli.cs.unibo.it" ~user:"helm" "matita" in
   7 let owner =
   8   try
   9     Sys.argv.(2)
  10   with Invalid_argument _ -> "matita_test"
  11 in
  12 if Sys.argv.(1) = "clean" then
  13   MetadataDb.clean ~dbh ~owner
  14 else
  15   let uri_str = Sys.argv.(1) in
  16   let uri = UriManager.uri_of_string uri_str in
  17   match CicEnvironment.get_obj uri with
  18   | Cic.Constant (_, body, ty, _) ->
  19       MetadataDb.index_constant ~body ~ty ~uri ~owner ~dbh
  20   | Cic.InductiveDefinition (types, _, _) ->
  21       MetadataDb.index_inductive_def ~dbh ~owner ~uri ~types
  22   | _ -> assert false
  23