X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FlibraryClean.ml;h=8e9f430ba7ee467969ebe947b5142b1fc73d4804;hb=d43b4cfa41256e90fceb0129b7eadb38207190c3;hp=a544991e85b109e3df0f74f68b27efaf04c612e5;hpb=622a76e7473084ea2dafb34cbc52fb7756b809b2;p=helm.git diff --git a/helm/software/components/library/libraryClean.ml b/helm/software/components/library/libraryClean.ml index a544991e8..8e9f430ba 100644 --- a/helm/software/components/library/libraryClean.ml +++ b/helm/software/components/library/libraryClean.ml @@ -34,14 +34,19 @@ module HGT = Http_getter_types;; module HG = Http_getter;; module UM = UriManager;; -let cache_of_processed_baseuri = Hashtbl.create 1024 +let decompile = ref (fun ~baseuri -> assert false);; +let set_decompile_cb f = decompile := f;; -let one_step_depend suri = - let buri = - try - UM.buri_of_uri (UM.uri_of_string suri) - with UM.IllFormedUri _ -> suri - in +let strip_xpointer s = Pcre.replace ~pat:"#.*$" s ;; + +let safe_buri_of_suri suri = + try + UM.buri_of_uri (UM.uri_of_string suri) + with + UM.IllFormedUri _ -> suri + +let one_step_depend cache_of_processed_baseuri suri dbtype dbd = + let buri = safe_buri_of_suri suri in if Hashtbl.mem cache_of_processed_baseuri buri then [] else @@ -49,21 +54,36 @@ 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[^/]*$'") + if HSql.isMysql dbtype dbd then + sprintf ("SELECT source, h_occurrence FROM %s WHERE " + ^^ "h_occurrence REGEXP '"^^ + "^%s\\([^/]+\\|[^/]+#xpointer.*\\)$"^^"'") + obj_tbl buri + else + begin + sprintf ("SELECT source, h_occurrence FROM %s WHERE " + ^^ "REGEXP(h_occurrence, '"^^ + "^%s\\([^/]+\\|[^/]+#xpointer.*\\)$"^^"')") 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 -> - l := uri :: !l + | Some uri, Some occ when + Filename.dirname (strip_xpointer occ) = buri -> + l := uri :: !l | _ -> ()); let l = List.sort Pervasives.compare !l in HExtlib.list_uniq l @@ -71,13 +91,44 @@ let one_step_depend suri = exn -> raise exn (* no errors should be accepted *) end -let safe_buri_of_suri suri = - try - UM.buri_of_uri (UM.uri_of_string 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 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 close_uri_list cache_of_processed_baseuri 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 +148,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,20 +165,35 @@ 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 cache_of_processed_baseuri u dbtype dbd @ acc) + [] uri_to_remove in let depend = HExtlib.list_uniq (List.fast_sort Pervasives.compare depend) in uri_to_remove, depend +;; -let rec close_db uris next = +let rec close_db cache_of_processed_baseuri uris next = match next with | [] -> uris - | l -> let uris, next = close_uri_list l in close_db uris next @ uris + | l -> + let uris, next = close_uri_list cache_of_processed_baseuri l in + close_db cache_of_processed_baseuri uris next @ uris +;; let cleaned_no = ref 0;; @@ -144,66 +210,21 @@ let moo_root_dir = lazy ( | _ -> assert false) (Helm_registry.get_list Helm_registry.string "getter.prefix")) in - 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 + String.sub url 7 (String.length url - 7)) +;; let clean_baseuris ?(verbose=true) buris = + let cache_of_processed_baseuri = Hashtbl.create 1024 in + 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 cache_of_processed_baseuri [] 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:"; @@ -211,14 +232,12 @@ let clean_baseuris ?(verbose=true) buris = List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l; List.iter (fun baseuri -> + !decompile ~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.metadata_file_of_baseuri - ~must_exist:false ~writable:true ~baseuri) ; HExtlib.safe_remove (LibraryMisc.lexicon_file_of_baseuri ~must_exist:false ~writable:true ~baseuri) ; @@ -232,7 +251,7 @@ let clean_baseuris ?(verbose=true) buris = let buri = UriManager.buri_of_uri uri in if buri <> !last_baseuri then begin - if Helm_registry.get_bool "matita.bench" then + if not (Helm_registry.get_bool "matita.verbose") then (print_endline ("matitaclean " ^ buri ^ "/");flush stdout) else HLog.message ("Removing: " ^ buri ^ "/*"); @@ -240,14 +259,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