2 let _ = Helm_registry.set "getter.mode" "remote";
3 let _ = Helm_registry.set "getter.url" "http://mowgli.cs.unibo.it:58081/" in
5 Mysql.quick_connect ~host:"mowgli.cs.unibo.it" ~user:"helm" ~database:"matita"
11 with Invalid_argument _ -> "matita_test"
13 let _ = MetadataTypes.ownerize_tables owner in
14 if Sys.argv.(1) = "clean" then begin
16 ignore (MetadataDb.clean ~dbd)
18 let fname = Sys.argv.(1) in
20 let ic = open_in fname in
23 let line = input_line ic in
25 Printf.printf "%d\t%s\n" !n line; flush stdout;
26 let uri = UriManager.uri_of_string line in
27 (match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
28 | Cic.Constant (_, body, ty, _, _), _ ->
29 MetadataDb.index_constant ~body ~ty ~uri ~dbd
30 | Cic.Variable (_, body, ty, _, _), _ ->
31 MetadataDb.index_constant ~body ~ty ~uri ~dbd
32 | Cic.InductiveDefinition (types, _, _, _), _ ->
33 MetadataDb.index_inductive_def ~dbd ~uri ~types
36 with End_of_file -> close_in ic