X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FlibraryClean.ml;h=a1f2a0cfc08fd356437b20a71dd7eea3d5220d48;hb=65662e7d8de61a338b636f208d04e85eb59e6b8e;hp=1b378e6c2a72f235ac9cdb62a0955ae7f6ba2334;hpb=748a6a2ba28c43e128759efbcc04919420e38cc1;p=helm.git diff --git a/components/library/libraryClean.ml b/components/library/libraryClean.ml index 1b378e6c2..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,9 +49,9 @@ 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 + if HSql.isMysql dbtype dbd then sprintf ("SELECT source, h_occurrence FROM %s WHERE " ^^ "h_occurrence REGEXP '^%s[^/]*$'") obj_tbl buri else @@ -67,7 +67,7 @@ let one_step_depend suri = 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 -> @@ -88,35 +88,34 @@ let safe_buri_of_suri suri = 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 buri in + let buri = HSql.escape dbtype dbd buri in let obj_tbl = MetadataTypes.name_tbl () in - if HSql.isMysql then + if HSql.isMysql dbtype dbd then sprintf ("SELECT source FROM %s WHERE " - ^^ "source REGEXP '^%s[^/]*$'") obj_tbl buri + ^^ "source REGEXP '^%s[^/]*(#xpointer.*)?$'") obj_tbl buri else begin sprintf ("SELECT source FROM %s WHERE " - ^^ "REGEXP(source, '^%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 - *) + ^^ "REGEXP(source, '^%s[^/]*\\(#xpointer.*\\)?$')") obj_tbl buri end in try - let rc = HSql.exec (LibraryDb.instance ()) query in + 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 uri = buri -> + | 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 @@ -124,6 +123,10 @@ let db_uris_of_baseuri buri = ;; 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 @@ -143,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 @@ -162,7 +165,9 @@ let close_uri_list uri_to_remove = in let uri_to_remove_from_db = List.fold_left - (fun acc buri -> db_uris_of_baseuri buri @ acc + (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 @@ -171,7 +176,7 @@ let close_uri_list uri_to_remove = (* 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) @@ -201,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:"; @@ -270,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) ; @@ -294,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()]