1 (* Copyright (C) 2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
31 let debug_prerr = if debug then prerr_endline else ignore
33 module HGT = Http_getter_types;;
34 module HG = Http_getter;;
35 module UM = UriManager;;
37 let cache_of_processed_baseuri = Hashtbl.create 1024
39 let one_step_depend suri =
42 UM.buri_of_uri (UM.uri_of_string suri)
43 with UM.IllFormedUri _ -> suri
45 if Hashtbl.mem cache_of_processed_baseuri buri then
49 Hashtbl.add cache_of_processed_baseuri buri true;
51 let buri = buri ^ "/" in
52 let buri = HSql.escape buri in
53 let obj_tbl = MetadataTypes.obj_tbl () in
55 sprintf ("SELECT source, h_occurrence FROM %s WHERE "
56 ^^ "h_occurrence REGEXP '^%s[^/]*$'") obj_tbl buri
59 HLog.debug "Warning SELECT without REGEXP";
61 ("SELECT source, h_occurrence FROM %s WHERE " ^^
62 "h_occurrence LIKE '%s%%'")
67 let rc = HSql.exec (LibraryDb.instance ()) query in
71 match row.(0), row.(1) with
72 | Some uri, Some occ when Filename.dirname occ = buri ->
75 let l = List.sort Pervasives.compare !l in
78 exn -> raise exn (* no errors should be accepted *)
81 let safe_buri_of_suri suri =
83 UM.buri_of_uri (UM.uri_of_string suri)
85 UM.IllFormedUri _ -> suri
87 let db_uris_of_baseuri buri =
89 let buri = buri ^ "/" in
90 let buri = HSql.escape buri in
91 let obj_tbl = MetadataTypes.name_tbl () in
93 sprintf ("SELECT source FROM %s WHERE "
94 ^^ "source REGEXP '^%s[^/]*$'") obj_tbl buri
97 HLog.debug "Warning SELECT without REGEXP";
99 ("SELECT source, h_occurrence FROM %s WHERE " ^^
100 "h_occurrence LIKE '%s%%'")
105 let rc = HSql.exec (LibraryDb.instance ()) query in
110 | Some uri when Filename.dirname uri = buri ->
113 let l = List.sort Pervasives.compare !l in
116 exn -> raise exn (* no errors should be accepted *)
119 let close_uri_list uri_to_remove =
120 (* to remove an uri you have to remove the whole script *)
123 (List.fast_sort Pervasives.compare
124 (List.map safe_buri_of_suri uri_to_remove))
126 (* cleand the already visided baseuris *)
130 if Hashtbl.mem cache_of_processed_baseuri buri then false
134 (* now calculate the list of objects that belong to these baseuris *)
139 let inhabitants = HG.ls (buri ^ "/") in
140 let inhabitants = List.filter
141 (function HGT.Ls_object _ -> true | _ -> false)
144 let inhabitants = List.map
146 | HGT.Ls_object e -> buri ^ "/" ^ e.HGT.uri
152 with HGT.Invalid_URI u ->
153 HLog.error ("We were listing an invalid buri: " ^ u);
156 let uri_to_remove_from_db =
158 (fun acc buri -> db_uris_of_baseuri buri @ acc
161 let uri_to_remove = uri_to_remove @ uri_to_remove_from_db in
163 HExtlib.list_uniq (List.sort Pervasives.compare uri_to_remove) in
164 (* now we want the list of all uri that depend on them *)
167 (fun acc u -> one_step_depend u @ acc) [] uri_to_remove
170 HExtlib.list_uniq (List.fast_sort Pervasives.compare depend)
172 uri_to_remove, depend
174 let rec close_db uris next =
177 | l -> let uris, next = close_uri_list l in close_db uris next @ uris
179 let cleaned_no = ref 0;;
181 (** TODO repellent code ... *)
182 let moo_root_dir = lazy (
184 List.assoc "cic:/matita/"
188 Str.split (Str.regexp "[ \t\r\n]+") (HExtlib.trim_blanks pair)
192 (Helm_registry.get_list Helm_registry.string "getter.prefix"))
194 String.sub url 7 (String.length url - 7) (* remove heading "file:///" *)
197 let close_nodb buris =
198 let rev_deps = Hashtbl.create 97 in
200 HExtlib.find ~test:(fun name -> Filename.check_suffix name ".metadata")
201 (Lazy.force moo_root_dir)
205 let metadata = LibraryNoDb.load_metadata ~fname:path in
206 let baseuri_of_current_metadata =
207 prerr_endline "ERROR, add to the getter reverse lookup";
208 let basedir = "/fake" in
209 let dirname = Filename.dirname path in
210 let basedirlen = String.length basedir in
211 assert (String.sub dirname 0 basedirlen = basedir);
213 String.sub dirname basedirlen (String.length dirname - basedirlen) ^
214 Filename.basename path
218 (function LibraryNoDb.Dependency buri -> Some buri)
222 (fun buri -> Hashtbl.add rev_deps buri baseuri_of_current_metadata) deps)
224 let buris_to_remove =
226 (List.fast_sort Pervasives.compare
227 (List.flatten (List.map (Hashtbl.find_all rev_deps) buris)))
229 let objects_to_remove =
230 let objs_of_buri buri =
233 | Http_getter_types.Ls_object o ->
234 Some (buri ^ "/" ^ o.Http_getter_types.uri)
236 (Http_getter.ls buri)
238 List.flatten (List.map objs_of_buri (buris @ buris_to_remove))
242 let clean_baseuris ?(verbose=true) buris =
243 Hashtbl.clear cache_of_processed_baseuri;
244 let buris = List.map Http_getter_misc.strip_trailing_slash buris in
245 debug_prerr "clean_baseuris called on:";
247 List.iter debug_prerr buris;
249 if Helm_registry.get_bool "db.nodb" then
254 let l = HExtlib.list_uniq (List.fast_sort Pervasives.compare l) in
255 let l = List.map UriManager.uri_of_string l in
256 debug_prerr "clean_baseuri will remove:";
258 List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l;
263 LibraryMisc.obj_file_of_baseuri ~must_exist:false ~writable:true ~baseuri
265 HExtlib.safe_remove obj_file ;
267 (LibraryMisc.metadata_file_of_baseuri
268 ~must_exist:false ~writable:true ~baseuri) ;
270 (LibraryMisc.lexicon_file_of_baseuri
271 ~must_exist:false ~writable:true ~baseuri) ;
272 HExtlib.rmdir_descend (Filename.chop_extension obj_file)
273 with Http_getter_types.Key_not_found _ -> ())
274 (HExtlib.list_uniq (List.fast_sort Pervasives.compare
275 (List.map (UriManager.buri_of_uri) l @ buris)));
277 (let last_baseuri = ref "" in
279 let buri = UriManager.buri_of_uri uri in
280 if buri <> !last_baseuri then
282 if Helm_registry.get_bool "matita.bench" then
283 (print_endline ("matitaclean " ^ buri ^ "/");flush stdout)
285 HLog.message ("Removing: " ^ buri ^ "/*");
288 LibrarySync.remove_obj uri
292 cleaned_no := !cleaned_no + List.length l;
293 if !cleaned_no > 30 then
298 ignore (HSql.exec (LibraryDb.instance ()) ("OPTIMIZE TABLE " ^ table)))
299 [MetadataTypes.name_tbl (); MetadataTypes.rel_tbl ();
300 MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl();
301 MetadataTypes.count_tbl()]