(* Copyright (C) 2005, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science * Department, University of Bologna, Italy. * * HELM is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License * as published by the Free Software Foundation; either version 2 * of the License, or (at your option) any later version. * * HELM is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with HELM; if not, write to the Free Software * Foundation, Inc., 59 Temple Place - Suite 330, Boston, * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, * http://helm.cs.unibo.it/ *) open Printf let debug = false let debug_prerr = if debug then prerr_endline else ignore module HGT = Http_getter_types;; module HG = Http_getter;; module HGM = Http_getter_misc;; module UM = UriManager;; module TA = GrafiteAst;; let cache_of_processed_baseuri = Hashtbl.create 1024 let one_step_depend suri = let buri = try UM.buri_of_uri (UM.uri_of_string suri) with UM.IllFormedUri _ -> suri in if Hashtbl.mem cache_of_processed_baseuri buri then [] else begin Hashtbl.add cache_of_processed_baseuri buri true; let query = let buri = buri ^ "/" in let buri = HMysql.escape buri in let obj_tbl = MetadataTypes.obj_tbl () in sprintf ("SELECT source, h_occurrence FROM %s WHERE " ^^ "h_occurrence REGEXP '^%s[^/]*$'") obj_tbl buri in try let rc = HMysql.exec (MatitaDb.instance ()) query in let l = ref [] in HMysql.iter rc ( fun row -> match row.(0), row.(1) with | Some uri, Some occ when Filename.dirname occ = 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 *) end let safe_buri_of_suri suri = try UM.buri_of_uri (UM.uri_of_string suri) with UM.IllFormedUri _ -> suri let close_uri_list uri_to_remove = (* to remove an uri you have to remove the whole script *) let buri_to_remove = HExtlib.list_uniq (List.fast_sort Pervasives.compare (List.map safe_buri_of_suri uri_to_remove)) in (* cleand the already visided baseuris *) let buri_to_remove = List.filter (fun buri -> if Hashtbl.mem cache_of_processed_baseuri buri then false else true) buri_to_remove in (* now calculate the list of objects that belong to these baseuris *) let uri_to_remove = try List.fold_left (fun acc buri -> let inhabitants = HG.ls (buri ^ "/") in let inhabitants = List.filter (function HGT.Ls_object _ -> true | _ -> false) inhabitants in let inhabitants = List.map (function | HGT.Ls_object e -> buri ^ "/" ^ e.HGT.uri | _ -> assert false) inhabitants in inhabitants @ acc) [] buri_to_remove with HGT.Invalid_URI u -> MatitaLog.error ("We were listing an invalid buri: " ^ u); exit 1 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 in let depend = HExtlib.list_uniq (List.fast_sort Pervasives.compare depend) in uri_to_remove, depend let rec close_using_db uris next = match next with | [] -> uris | l -> let uris, next = close_uri_list l in close_using_db uris next @ uris let cleaned_no = ref 0;; (** TODO repellent code ... *) let moo_root_dir = lazy ( let url = List.assoc "cic:/matita/" (List.map (fun pair -> match Str.split (Str.regexp "[ \t\r\n]+") (HExtlib.trim_blanks pair) with | [a;b] -> a, b | _ -> 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_using_moos buris = let rev_deps = Hashtbl.create 97 in let all_moos = HExtlib.find ~test:(fun name -> Filename.check_suffix name ".moo") (Lazy.force moo_root_dir) in List.iter (fun path -> let _, metadata = MatitaMoo.load_moo ~fname:path in let baseuri_of_current_moo = let rec aux = function | [] -> assert false | GrafiteAst.Baseuri buri::_ -> buri | _ :: tl -> aux tl in aux metadata in let deps = HExtlib.filter_map (function | GrafiteAst.Dependency buri -> Some buri | _ -> None ) metadata in List.iter (fun buri -> Hashtbl.add rev_deps buri baseuri_of_current_moo) deps) all_moos; 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 = Hashtbl.clear cache_of_processed_baseuri; let buris = List.map HGM.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_using_moos buris else close_using_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:"; if debug then List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l; List.iter (fun buri -> MatitaMisc.safe_remove (MatitaMisc.obj_file_of_baseuri buri)) (HExtlib.list_uniq (List.fast_sort Pervasives.compare (List.map (UriManager.buri_of_uri) l))); List.iter (MatitaSync.remove ~verbose) l; cleaned_no := !cleaned_no + List.length l; if !cleaned_no > 30 then begin cleaned_no := 0; List.iter (function table -> ignore (HMysql.exec (MatitaDb.instance ()) ("OPTIMIZE TABLE " ^ table))) [MetadataTypes.name_tbl (); MetadataTypes.rel_tbl (); MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl(); MetadataTypes.count_tbl()] end