From 42e4ab5293078dd99a89933971403fa652d26b09 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 8 Sep 2007 17:22:34 +0000 Subject: [PATCH] matita can now safely start a matitac that will put metadata in the right db. --- helm/software/components/hmysql/hSqlite3.ml | 39 +++++++++++++++++---- 1 file changed, 32 insertions(+), 7 deletions(-) diff --git a/helm/software/components/hmysql/hSqlite3.ml b/helm/software/components/hmysql/hSqlite3.ml index d5c5f0fcc..0038c650f 100644 --- a/helm/software/components/hmysql/hSqlite3.ml +++ b/helm/software/components/hmysql/hSqlite3.ml @@ -54,19 +54,44 @@ let quick_connect = let username = Helm_registry.get "user.name" in 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 ()) + 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 + | [] -> + HLog.debug ("HSqlite3: no valid db files found in memory"); + let name = root ^ base ^ string_of_int (Unix.getpid ()) in + HLog.debug ("HSqlite3: memory db file name: "^name); + name, true + | x::tl -> + HLog.debug ("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) -> + HLog.debug ("HSqlite3: found valid db file: " ^ x); + x, false + | _ -> + HLog.warn ("HSqlite3: dead process db file found: " ^ x); + HLog.warn ("HSqlite3: ignoring: " ^ x); + aux tl + in + aux files in 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); + then ( + let tmp_db_name, first_time = find_db () in + let cp_to_ram_cmd = "cp " ^ db_name ^ " " ^ tmp_db_name in + if first_time then + if HExtlib.is_regular db_name then ignore (Sys.command cp_to_ram_cmd) + else HLog.debug ("HSqlite3: no initial db: " ^ db_name) + else HLog.debug "HSqlite3: not copying the db, already in memory"; let mv_to_disk_cmd _ = - ignore (Sys.command ("mv " ^ tmp_db_name ^ " " ^ db_name)) + if first_time then ignore (Sys.command ("mv "^tmp_db_name^" "^db_name)) + else HLog.debug "HSqlite3: not copying back the db" in at_exit mv_to_disk_cmd; tmp_db_name) -- 2.39.2