]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/library/libraryClean.ml
fixed a bug in the cleanup ofsedir that was not properly catching #xpointer
[helm.git] / helm / software / components / library / libraryClean.ml
index f61fc89c27f0ada471af7926b734f470a5570e28..7a4168402c48875303acdaaa151a216845917631 100644 (file)
@@ -36,7 +36,7 @@ module UM = UriManager;;
 
 let cache_of_processed_baseuri = Hashtbl.create 1024
 
-let one_step_depend suri =
+let one_step_depend suri dbtype dbd =
   let buri =
     try
       UM.buri_of_uri (UM.uri_of_string suri)
@@ -49,22 +49,25 @@ let one_step_depend suri =
       Hashtbl.add cache_of_processed_baseuri buri true;
       let query = 
         let buri = buri ^ "/" in 
-        let buri = HSql.escape buri in
+        let buri = HSql.escape dbtype dbd buri in
         let obj_tbl = MetadataTypes.obj_tbl () in
-       if HSql.isMysql then        
-         sprintf ("SELECT source, h_occurrence FROM %s WHERE " 
-         ^^ "h_occurrence REGEXP '^%s[^/]*$'") obj_tbl buri
-       else
-        begin
+        if HSql.isMysql dbtype dbd then        
+          sprintf ("SELECT source, h_occurrence FROM %s WHERE " 
+            ^^ "h_occurrence REGEXP '^%s[^/]*$'") obj_tbl buri
+       else
+               begin
+            sprintf ("SELECT source, h_occurrence FROM %s WHERE " 
+            ^^ "REGEXP(h_occurrence, '^%s[^/]*$')") obj_tbl buri
+          (* implementation with vanilla ocaml-sqlite3
           HLog.debug "Warning SELECT without REGEXP";
-         sprintf
-          ("SELECT source, h_occurrence FROM %s WHERE " ^^ 
-          "h_occurrence LIKE '%s%%'")
-         obj_tbl buri
-        end
+         sprintf
+            ("SELECT source, h_occurrence FROM %s WHERE " ^^ 
+             "h_occurrence LIKE '%s%%' " ^^ HSql.escape_string_for_like)
+                 obj_tbl buri*)
+               end
       in
       try 
-        let rc = HSql.exec (LibraryDb.instance ()) query in
+        let rc = HSql.exec dbtype dbd query in
         let l = ref [] in
         HSql.iter rc (
           fun row -> 
@@ -84,7 +87,46 @@ let safe_buri_of_suri suri =
   with
     UM.IllFormedUri _ -> suri
 
+let db_uris_of_baseuri buri =
+ let dbd = LibraryDb.instance () in
+ let dbtype = 
+   if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User
+ in
+ let query = 
+  let buri = buri ^ "/" in 
+  let buri = HSql.escape dbtype dbd buri in
+  let obj_tbl = MetadataTypes.name_tbl () in
+  if HSql.isMysql dbtype dbd then        
+    sprintf ("SELECT source FROM %s WHERE " 
+    ^^ "source REGEXP '^%s[^/]*(#xpointer.*)?$'") obj_tbl buri
+  else
+   begin
+    sprintf ("SELECT source FROM %s WHERE " 
+      ^^ "REGEXP(source, '^%s[^/]*(#xpointer.*)?$')") obj_tbl buri
+   end
+ in
+ try 
+  let rc = HSql.exec dbtype dbd query in
+  let strip_xpointer s = Pcre.replace ~pat:"#.*$" s in
+  let l = ref [] in
+  HSql.iter rc (
+    fun row -> 
+      match row.(0) with 
+      | Some uri when Filename.dirname (strip_xpointer uri) = buri -> 
+          l := uri :: !l
+      | _ ->
+          ());
+  let l = List.sort Pervasives.compare !l in
+  HExtlib.list_uniq l
+ with
+  exn -> raise exn (* no errors should be accepted *)
+;;
+
 let close_uri_list uri_to_remove =
+  let dbd = LibraryDb.instance () in
+  let dbtype = 
+    if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User
+  in
   (* to remove an uri you have to remove the whole script *)
   let buri_to_remove = 
     HExtlib.list_uniq 
@@ -104,7 +146,7 @@ let close_uri_list uri_to_remove =
     try
       List.fold_left 
         (fun acc buri ->
-          let inhabitants = HG.ls (buri ^ "/") in
+          let inhabitants = HG.ls ~local:true (buri ^ "/") in
           let inhabitants = List.filter 
               (function HGT.Ls_object _ -> true | _ -> false) 
             inhabitants
@@ -121,10 +163,20 @@ let close_uri_list uri_to_remove =
       HLog.error ("We were listing an invalid buri: " ^ u);
       exit 1
   in
+  let uri_to_remove_from_db =
+   List.fold_left 
+     (fun acc buri -> 
+       let dbu = db_uris_of_baseuri buri in
+       dbu @ acc
+     ) [] buri_to_remove 
+  in
+  let uri_to_remove = uri_to_remove @ uri_to_remove_from_db in
+  let uri_to_remove =
+   HExtlib.list_uniq (List.sort Pervasives.compare uri_to_remove) in
   (* now we want the list of all uri that depend on them *) 
   let depend = 
     List.fold_left
-    (fun acc u -> one_step_depend u @ acc) [] uri_to_remove
+    (fun acc u -> one_step_depend u dbtype dbd @ acc) [] uri_to_remove
   in
   let depend = 
     HExtlib.list_uniq (List.fast_sort Pervasives.compare depend) 
@@ -154,63 +206,17 @@ let moo_root_dir = lazy (
   String.sub url 7 (String.length url - 7)  (* remove heading "file:///" *)
 )
 
-let close_nodb buris =
-  let rev_deps = Hashtbl.create 97 in
-  let all_metadata =
-    HExtlib.find ~test:(fun name -> Filename.check_suffix name ".metadata")
-      (Lazy.force moo_root_dir)
-  in
-  List.iter
-    (fun path -> 
-      let metadata = LibraryNoDb.load_metadata ~fname:path in
-      let baseuri_of_current_metadata =
-       prerr_endline "ERROR, add to the getter reverse lookup";
-       let basedir = "/fake" in
-       let dirname = Filename.dirname path in
-       let basedirlen = String.length basedir in
-        assert (String.sub dirname 0 basedirlen = basedir);
-        "cic:" ^
-        String.sub dirname basedirlen (String.length dirname - basedirlen) ^
-         Filename.basename path
-      in
-      let deps = 
-        HExtlib.filter_map 
-          (function LibraryNoDb.Dependency buri -> Some buri)
-        metadata
-      in
-      List.iter 
-        (fun buri -> Hashtbl.add rev_deps buri baseuri_of_current_metadata) deps)
-    all_metadata;
-  let buris_to_remove = 
-    HExtlib.list_uniq  
-      (List.fast_sort Pervasives.compare 
-        (List.flatten (List.map (Hashtbl.find_all rev_deps) buris)))
-  in
-  let objects_to_remove = 
-    let objs_of_buri buri =
-      HExtlib.filter_map 
-        (function 
-        | Http_getter_types.Ls_object o ->
-            Some (buri ^ "/" ^ o.Http_getter_types.uri)
-        | _ -> None) 
-      (Http_getter.ls buri)
-    in
-    List.flatten (List.map objs_of_buri (buris @ buris_to_remove))
-  in
-  objects_to_remove
-
 let clean_baseuris ?(verbose=true) buris =
+  let dbd = LibraryDb.instance () in
+  let dbtype = 
+    if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User
+  in
   Hashtbl.clear cache_of_processed_baseuri;
   let buris = List.map Http_getter_misc.strip_trailing_slash buris in
   debug_prerr "clean_baseuris called on:";
   if debug then
     List.iter debug_prerr buris; 
-  let l = 
-    if Helm_registry.get_bool "db.nodb" then
-      close_nodb buris
-    else
-      close_db [] buris 
-  in
+  let l = close_db [] buris in
   let l = HExtlib.list_uniq (List.fast_sort Pervasives.compare l) in
   let l = List.map UriManager.uri_of_string l in
   debug_prerr "clean_baseuri will remove:";
@@ -223,9 +229,6 @@ let clean_baseuris ?(verbose=true) buris =
        LibraryMisc.obj_file_of_baseuri ~must_exist:false ~writable:true ~baseuri
       in
        HExtlib.safe_remove obj_file ;
-       HExtlib.safe_remove 
-         (LibraryMisc.metadata_file_of_baseuri 
-           ~must_exist:false ~writable:true ~baseuri) ;
        HExtlib.safe_remove 
          (LibraryMisc.lexicon_file_of_baseuri 
            ~must_exist:false ~writable:true ~baseuri) ;
@@ -247,15 +250,15 @@ let clean_baseuris ?(verbose=true) buris =
       end;
      LibrarySync.remove_obj uri
    ) l;
-  if HSql.isMysql then
+  if HSql.isMysql dbtype dbd then
    begin
    cleaned_no := !cleaned_no + List.length l;
-   if !cleaned_no > 30 then
+   if !cleaned_no > 30 && HSql.isMysql dbtype dbd then
     begin
      cleaned_no := 0;
      List.iter
       (function table ->
-        ignore (HSql.exec (LibraryDb.instance ()) ("OPTIMIZE TABLE " ^ table)))
+        ignore (HSql.exec dbtype dbd ("OPTIMIZE TABLE " ^ table)))
       [MetadataTypes.name_tbl (); MetadataTypes.rel_tbl ();
        MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl();
        MetadataTypes.count_tbl()]