remove_obj is now much faster:

 1. the code was utterly messy, trying to remove from the DB files and
    to remove from disk #xpointer uris.
 2. LIKE substituted by =
 3. added QUICK and LOW_PRIORITY to the DELETE statement
 4. removed unuseful and unused debugging code that used to slow down every
    deletion

diff --git a/components/library/libraryDb.ml b/components/library/libraryDb.ml
index 858e4c4ff790e97dee62f215862bf5e55db939a0..d3e7e9831b39977da16e2ea1e40338d2b38fff6d 100644 (file)
--- a/components/library/libraryDb.ml
+++ b/components/library/libraryDb.ml
@@ -143,7 +143,7 @@ let remove_uri uri =
   let dbd = instance () in
   let suri = UriManager.string_of_uri uri in 
   let query table suri = sprintf 
-    "DELETE FROM %s WHERE source LIKE '%s%%'" table (HMysql.escape suri)
+    "DELETE QUICK LOW_PRIORITY FROM %s WHERE source='%s'" table (HMysql.escape suri)
   in
   List.iter (fun t -> 
     try 
@@ -152,19 +152,7 @@ let remove_uri uri =
       exn -> raise exn (* no errors should be accepted *)
     )
   [obj_tbl;sort_tbl;rel_tbl;name_tbl;(*conclno_tbl;conclno_hyp_tbl*)count_tbl];
-  (* and now the debug job *)  
-  let dbg_q = 
-    sprintf "SELECT source FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl
-    (HMysql.escape suri)
-  in
-  try 
-    let rc = HMysql.exec dbd dbg_q in
-    let l = ref [] in
-    HMysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l := a:: !l);
-    let l = List.sort Pervasives.compare !l in
-    HExtlib.list_uniq l
-  with
-    exn -> raise exn (* no errors should be accepted *)
+;;
 
 let xpointers_of_ind uri =
   let dbd = instance () in

diff --git a/components/library/libraryDb.mli b/components/library/libraryDb.mli
index 39aa7c07976af7c7cdcf29ae67adb9860e16d23a..fc3dc969a1e6b99e1313b502851a60bb534176ee 100644 (file)
--- a/components/library/libraryDb.mli
+++ b/components/library/libraryDb.mli
@@ -28,7 +28,5 @@ val instance: unit -> HMysql.dbd
 val create_owner_environment: unit -> unit
 val clean_owner_environment: unit -> unit
 
-(* returns a list of uri thet must be removed sice they reference uri,
- * but this is used only for debugging purposes *)
-val remove_uri: UriManager.uri -> string list
+val remove_uri: UriManager.uri -> unit
 val xpointers_of_ind: UriManager.uri -> UriManager.uri list

diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index 9529375ae57a6b36c3317c45b8878ff24fa6932e..a3429840b7b2e169c835c753529de9e4cabed0e3 100644 (file)
--- a/components/library/librarySync.ml
+++ b/components/library/librarySync.ml
@@ -157,22 +157,24 @@ let remove_single_obj uri =
    let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
     innertypesuri::univgraphuri::(match bodyuri with None -> [] | Some u -> [u])
   in
-  let to_remove =
-    uri :: 
-    (if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else []) @
-    derived_uris_of_uri uri
-  in   
+  let uris_to_remove =
+   if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else [uri]
+  in
+  let files_to_remove = uri :: derived_uris_of_uri uri in   
+  List.iter 
+   (fun uri -> 
+     (try
+       let file = Http_getter.resolve' ~writable:true uri in
+        HExtlib.safe_remove file;
+        HExtlib.rmdir_descend (Filename.dirname file)
+     with Http_getter_types.Key_not_found _ -> ());
+   ) files_to_remove ;
   List.iter 
-    (fun uri -> 
-      (try
-        let file = Http_getter.resolve' ~writable:true uri in
-         HExtlib.safe_remove file;
-         HExtlib.rmdir_descend (Filename.dirname file)
-      with Http_getter_types.Key_not_found _ -> ());
-      ignore (LibraryDb.remove_uri uri);
-      (*CoercGraph.remove_coercion uri;*)
-      CicEnvironment.remove_obj uri)
-  to_remove
+   (fun uri -> 
+     ignore (LibraryDb.remove_uri uri);
+     (*CoercGraph.remove_coercion uri;*)
+     CicEnvironment.remove_obj uri
+   ) uris_to_remove
 
 (*** GENERATION OF AUXILIARY LEMMAS ***)