let profiler = HExtlib.profile "Sqlite3"
-let quick_connect ?host ?(database = "sqlite") ?port ?password ?user () =
+let quick_connect
+ is_library
+ ?(host = Helm_registry.get "matita.basedir")
+ ?(database = "sqlite") ?port ?password ?user ()
+=
let username = Helm_registry.get "user.name" in
- let tmp_db_name =
- if HExtlib.is_dir "/dev/shm/" && HExtlib.writable_dir "/dev/shm/" then
- ((*HLog.debug "using /dev/shm to store the working copy of the db";*)
- "/dev/shm/matita.db." ^ username ^ "." ^ string_of_int (Unix.getpid ()))
- else
- ((*HLog.debug "/dev/shm not available";*)
- Helm_registry.get "matita.basedir" ^ "/matita.db." ^ username ^ "." ^
- string_of_int (Unix.getpid ()))
- in
- let db_name = Helm_registry.get "matita.basedir" ^ "/" ^ database ^ ".db" in
- let standard_db_name =
- Helm_registry.get "matita.rt_base_dir" ^ "/metadata.db"
+ let host_mangled = Pcre.replace ~pat:"[/ .]" ~templ:"_" host in
+ let tmp_db_name =
+ "/dev/shm/matita.db." ^ username ^ "." ^ host_mangled ^ "." ^
+ string_of_int (Unix.getpid ())
in
- let cp_to_ram_cmd =
- if HExtlib.is_regular db_name then
- "cp " ^ db_name ^ " " ^ tmp_db_name
+ let db_name = host ^ "/" ^ database in
+ let db_to_open =
+ if HExtlib.is_dir "/dev/shm/" && HExtlib.writable_dir "/dev/shm/"
+ && (not is_library)
+ then
+ (let cp_to_ram_cmd = "cp " ^ db_name ^ " " ^ tmp_db_name in
+ ignore (Sys.command cp_to_ram_cmd);
+ let mv_to_disk_cmd _ =
+ ignore (Sys.command ("mv " ^ tmp_db_name ^ " " ^ db_name))
+ in
+ at_exit mv_to_disk_cmd;
+ tmp_db_name)
else
- (* we start from the standard library *)
- "cp " ^ standard_db_name ^ " " ^ tmp_db_name
- in
- ignore (Sys.command cp_to_ram_cmd);
- let mv_to_disk_cmd _ =
- ignore (Sys.command ("mv " ^ tmp_db_name ^ " " ^ db_name))
+ db_name
in
- at_exit mv_to_disk_cmd;
- let db = Sqlite3.db_open tmp_db_name in
+ let db = Sqlite3.db_open db_to_open in
(* attach the REGEX function *)
- Sqlite3.create_fun_2 db "REGEXP"
+ Sqlite3.create_fun2 db "REGEXP"
(fun s rex ->
match rex, s with
| Sqlite3.Data.TEXT rex, Sqlite3.Data.BLOB s
let pp_rc rc = prerr_endline (string_of_rc rc);;
-let exec db s =
+let exec s db =
prerr_endline s;
let stored_result = ref [] in
let store row =