X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FlibraryClean.ml;h=a1f2a0cfc08fd356437b20a71dd7eea3d5220d48;hb=dc9c722d837c1342798920762b2d0015b71b051f;hp=04333fc9a66724230fea843153a4d36d22d42e3b;hpb=d4c6f8464dc183326b7f7b4dc6171e69b482a26b;p=helm.git diff --git a/components/library/libraryClean.ml b/components/library/libraryClean.ml index 04333fc9a..a1f2a0cfc 100644 --- a/components/library/libraryClean.ml +++ b/components/library/libraryClean.ml @@ -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,17 +49,27 @@ let one_step_depend suri = Hashtbl.add cache_of_processed_baseuri buri true; let query = let buri = buri ^ "/" in - let buri = HMysql.escape buri in + let buri = HSql.escape dbtype dbd buri in let obj_tbl = MetadataTypes.obj_tbl () in - sprintf - ("SELECT source, h_occurrence FROM %s WHERE " ^^ - "h_occurrence REGEXP '^%s[^/]*$'") - obj_tbl buri + 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%%' " ^^ HSql.escape_string_for_like) + obj_tbl buri*) + end in try - let rc = HMysql.exec (LibraryDb.instance ()) query in + let rc = HSql.exec dbtype dbd query in let l = ref [] in - HMysql.iter rc ( + HSql.iter rc ( fun row -> match row.(0), row.(1) with | Some uri, Some occ when Filename.dirname occ = buri -> @@ -77,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 @@ -97,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 @@ -114,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) @@ -147,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:"; @@ -212,15 +225,17 @@ let clean_baseuris ?(verbose=true) buris = List.iter (fun baseuri -> try + let obj_file = + LibraryMisc.obj_file_of_baseuri ~must_exist:false ~writable:true ~baseuri + in + HExtlib.safe_remove obj_file ; HExtlib.safe_remove - (LibraryMisc.obj_file_of_baseuri ~writable:true ~baseuri); - HExtlib.safe_remove - (LibraryMisc.metadata_file_of_baseuri ~writable:true ~baseuri); - HExtlib.safe_remove - (LibraryMisc.lexicon_file_of_baseuri ~writable:true ~baseuri) + (LibraryMisc.lexicon_file_of_baseuri + ~must_exist:false ~writable:true ~baseuri) ; + HExtlib.rmdir_descend (Filename.chop_extension obj_file) with Http_getter_types.Key_not_found _ -> ()) (HExtlib.list_uniq (List.fast_sort Pervasives.compare - (List.map (UriManager.buri_of_uri) l))); + (List.map (UriManager.buri_of_uri) l @ buris))); List.iter (let last_baseuri = ref "" in fun uri -> @@ -235,14 +250,17 @@ let clean_baseuris ?(verbose=true) buris = end; LibrarySync.remove_obj uri ) l; - cleaned_no := !cleaned_no + List.length l; - if !cleaned_no > 30 then + if HSql.isMysql dbtype dbd then begin - cleaned_no := 0; - List.iter - (function table -> - ignore (HMysql.exec (LibraryDb.instance ()) ("OPTIMIZE TABLE " ^ table))) - [MetadataTypes.name_tbl (); MetadataTypes.rel_tbl (); - MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl(); - MetadataTypes.count_tbl()] + cleaned_no := !cleaned_no + List.length l; + if !cleaned_no > 30 && HSql.isMysql dbtype dbd then + begin + cleaned_no := 0; + List.iter + (function table -> + ignore (HSql.exec dbtype dbd ("OPTIMIZE TABLE " ^ table))) + [MetadataTypes.name_tbl (); MetadataTypes.rel_tbl (); + MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl(); + MetadataTypes.count_tbl()] + end end