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 decompile = ref (fun ~baseuri -> assert false);;
38 let set_decompile_cb f = decompile := f;;
40 let strip_xpointer s = Pcre.replace ~pat:"#.*$" s ;;
42 let safe_buri_of_suri suri =
44 UM.buri_of_uri (UM.uri_of_string suri)
46 UM.IllFormedUri _ -> suri
48 let one_step_depend cache_of_processed_baseuri suri dbtype dbd =
49 assert false (* MATITA 1.0
50 let buri = safe_buri_of_suri suri in
51 if Hashtbl.mem cache_of_processed_baseuri buri then
55 Hashtbl.add cache_of_processed_baseuri buri true;
57 let buri = buri ^ "/" in
58 let buri = HSql.escape dbtype dbd buri in
59 let obj_tbl = MetadataTypes.obj_tbl () in
60 if HSql.isMysql dbtype dbd then
61 sprintf ("SELECT source, h_occurrence FROM %s WHERE "
62 ^^ "h_occurrence REGEXP '"^^
63 "^%s\\([^/]+\\|[^/]+#xpointer.*\\)$"^^"'")
67 sprintf ("SELECT source, h_occurrence FROM %s WHERE "
68 ^^ "REGEXP(h_occurrence, '"^^
69 "^%s\\([^/]+\\|[^/]+#xpointer.*\\)$"^^"')")
71 (* implementation with vanilla ocaml-sqlite3
72 HLog.debug "Warning SELECT without REGEXP";
74 ("SELECT source, h_occurrence FROM %s WHERE " ^^
75 "h_occurrence LIKE '%s%%' " ^^ HSql.escape_string_for_like)
80 let rc = HSql.exec dbtype dbd query in
84 match row.(0), row.(1) with
85 | Some uri, Some occ when
86 Filename.dirname (strip_xpointer occ) = buri ->
89 let l = List.sort Pervasives.compare !l in
92 exn -> raise exn (* no errors should be accepted *)
96 let db_uris_of_baseuri buri =
98 let dbd = LibraryDb.instance () in
100 if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User
103 let buri = buri ^ "/" in
104 let buri = HSql.escape dbtype dbd buri in
105 let obj_tbl = MetadataTypes.name_tbl () in
106 if HSql.isMysql dbtype dbd then
107 sprintf ("SELECT source FROM %s WHERE "
108 ^^ "source REGEXP '^%s[^/]*(#xpointer.*)?$'") obj_tbl buri
111 sprintf ("SELECT source FROM %s WHERE "
112 ^^ "REGEXP(source, '^%s[^/]*\\(#xpointer.*\\)?$')") obj_tbl buri
116 let rc = HSql.exec dbtype dbd query in
121 | Some uri when Filename.dirname (strip_xpointer uri) = buri ->
124 let l = List.sort Pervasives.compare !l in
127 exn -> raise exn (* no errors should be accepted *)
131 let close_uri_list cache_of_processed_baseuri uri_to_remove =
132 let dbd = LibraryDb.instance () in
134 if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User
136 (* to remove an uri you have to remove the whole script *)
139 (List.fast_sort Pervasives.compare
140 (List.map safe_buri_of_suri uri_to_remove))
142 (* cleand the already visided baseuris *)
146 if Hashtbl.mem cache_of_processed_baseuri buri then false
150 (* now calculate the list of objects that belong to these baseuris *)
155 let inhabitants = HG.ls ~local:true (buri ^ "/") in
156 let inhabitants = List.filter
157 (function HGT.Ls_object _ -> true | _ -> false)
160 let inhabitants = List.map
162 | HGT.Ls_object e -> buri ^ "/" ^ e.HGT.uri
168 with HGT.Invalid_URI u ->
169 HLog.error ("We were listing an invalid buri: " ^ u);
172 let uri_to_remove_from_db =
175 let dbu = db_uris_of_baseuri buri in
179 let uri_to_remove = uri_to_remove @ uri_to_remove_from_db in
181 HExtlib.list_uniq (List.sort Pervasives.compare uri_to_remove) in
182 (* now we want the list of all uri that depend on them *)
185 (fun acc u -> one_step_depend cache_of_processed_baseuri u dbtype dbd @ acc)
189 HExtlib.list_uniq (List.fast_sort Pervasives.compare depend)
191 uri_to_remove, depend
194 let rec close_db cache_of_processed_baseuri uris next =
198 let uris, next = close_uri_list cache_of_processed_baseuri l in
199 close_db cache_of_processed_baseuri uris next @ uris
202 let cleaned_no = ref 0;;
204 (** TODO repellent code ... *)
205 let moo_root_dir = lazy (
207 List.assoc "cic:/matita/"
211 Str.split (Str.regexp "[ \t\r\n]+") (HExtlib.trim_blanks pair)
215 (Helm_registry.get_list Helm_registry.string "getter.prefix"))
217 String.sub url 7 (String.length url - 7))
220 let clean_baseuris ?(verbose=true) buris =
221 prerr_endline "CLEAN_BASEURIS to be removed MATITA 1.0"; (* MATITA 1.0
222 let cache_of_processed_baseuri = Hashtbl.create 1024 in
223 let dbd = LibraryDb.instance () in
225 if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User
227 Hashtbl.clear cache_of_processed_baseuri;
228 let buris = List.map Http_getter_misc.strip_trailing_slash buris in
229 debug_prerr "clean_baseuris called on:";
231 List.iter debug_prerr buris;
232 let l = close_db cache_of_processed_baseuri [] buris in
233 let l = HExtlib.list_uniq (List.fast_sort Pervasives.compare l) in
234 let l = List.map UriManager.uri_of_string l in
235 debug_prerr "clean_baseuri will remove:";
237 List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l;
243 LibraryMisc.obj_file_of_baseuri ~must_exist:false ~writable:true ~baseuri
245 HExtlib.safe_remove obj_file ;
247 (LibraryMisc.lexicon_file_of_baseuri
248 ~must_exist:false ~writable:true ~baseuri) ;
249 HExtlib.rmdir_descend (Filename.chop_extension obj_file)
250 with Http_getter_types.Key_not_found _ -> ())
251 (HExtlib.list_uniq (List.fast_sort Pervasives.compare
252 (List.map (UriManager.buri_of_uri) l @ buris)));
254 (let last_baseuri = ref "" in
256 let buri = UriManager.buri_of_uri uri in
257 if buri <> !last_baseuri then
259 if not (Helm_registry.get_bool "matita.verbose") then
260 (print_endline ("matitaclean " ^ buri ^ "/");flush stdout)
262 HLog.message ("Removing: " ^ buri ^ "/*");
265 LibrarySync.remove_obj uri
267 if HSql.isMysql dbtype dbd then
269 cleaned_no := !cleaned_no + List.length l;
270 if !cleaned_no > 30 && HSql.isMysql dbtype dbd then
275 ignore (HSql.exec dbtype dbd ("OPTIMIZE TABLE " ^ table)))
276 [MetadataTypes.name_tbl (); MetadataTypes.rel_tbl ();
277 MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl();
278 MetadataTypes.count_tbl()]