- 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 ()))
+ let host_mangled = Pcre.replace ~pat:"[/ .]" ~templ:"_" host in
+ let find_db _ =
+ let base = "matita.db." ^ username ^ "." ^ host_mangled ^ "." in
+ let root = "/dev/shm/" in
+ let files = HExtlib.find ~test:(Pcre.pmatch ~pat:(base^"[0-9]+")) root in
+ let rec aux = function
+ | [] ->
+ debug_print ("HSqlite3: no valid db files found in memory");
+ let name = root ^ base ^ string_of_int (Unix.getpid ()) in
+ debug_print ("HSqlite3: memory db file name: "^name);
+ name, true
+ | x::tl ->
+ debug_print ("HSqlite3: found a .db in memory: " ^ x);
+ match Array.to_list (Pcre.extract ~pat:"\\.([0-9]+)$" x) with
+ | [] | _::_::_::_ -> assert false
+ | [_;p] when HExtlib.is_dir ("/proc/" ^ p) ->
+ debug_print ("HSqlite3: found valid db file: " ^ x);
+ x, false
+ | _ ->
+ HLog.warn ("HSqlite3: dead process db file found: " ^ x);
+ HLog.warn ("HSqlite3: removing: " ^ x);
+ ignore (Sys.command ("rm " ^ x));
+ aux tl
+ in
+ aux files