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/
29 let debug_prerr = if debug then prerr_endline else ignore
31 module HGT = Http_getter_types;;
32 module HG = Http_getter;;
33 module HGM = Http_getter_misc;;
34 module UM = UriManager;;
35 module TA = GrafiteAst;;
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 = HMysql.escape buri in
53 let obj_tbl = MetadataTypes.obj_tbl () in
55 ("SELECT source, h_occurrence FROM %s WHERE " ^^
56 "h_occurrence REGEXP '^%s[^/]*$'")
60 let rc = HMysql.exec (MatitaDb.instance ()) query in
64 match row.(0), row.(1) with
65 | Some uri, Some occ when Filename.dirname occ = buri ->
68 let l = List.sort Pervasives.compare !l in
71 exn -> raise exn (* no errors should be accepted *)
74 let safe_buri_of_suri suri =
76 UM.buri_of_uri (UM.uri_of_string suri)
78 UM.IllFormedUri _ -> suri
80 let close_uri_list uri_to_remove =
81 (* to remove an uri you have to remove the whole script *)
84 (List.fast_sort Pervasives.compare
85 (List.map safe_buri_of_suri uri_to_remove))
87 (* cleand the already visided baseuris *)
91 if Hashtbl.mem cache_of_processed_baseuri buri then false
95 (* now calculate the list of objects that belong to these baseuris *)
100 let inhabitants = HG.ls (buri ^ "/") in
101 let inhabitants = List.filter
102 (function HGT.Ls_object _ -> true | _ -> false)
105 let inhabitants = List.map
107 | HGT.Ls_object e -> buri ^ "/" ^ e.HGT.uri
113 with HGT.Invalid_URI u ->
114 MatitaLog.error ("We were listing an invalid buri: " ^ u);
117 (* now we want the list of all uri that depend on them *)
120 (fun acc u -> one_step_depend u @ acc) [] uri_to_remove
123 HExtlib.list_uniq (List.fast_sort Pervasives.compare depend)
125 uri_to_remove, depend
127 let rec close_using_db uris next =
130 | l -> let uris, next = close_uri_list l in close_using_db uris next @ uris
132 let cleaned_no = ref 0;;
134 (** TODO repellent code ... *)
135 let moo_root_dir = lazy (
137 List.assoc "cic:/matita/"
141 Str.split (Str.regexp "[ \t\r\n]+") (HExtlib.trim_blanks pair)
145 (Helm_registry.get_list Helm_registry.string "getter.prefix"))
147 String.sub url 7 (String.length url - 7) (* remove heading "file:///" *)
150 let close_using_moos buris =
151 let rev_deps = Hashtbl.create 97 in
153 HExtlib.find ~test:(fun name -> Filename.check_suffix name ".moo")
154 (Lazy.force moo_root_dir)
158 let _, metadata = MatitaMoo.load_moo ~fname:path in
159 let baseuri_of_current_moo =
160 let rec aux = function
162 | GrafiteAst.Baseuri buri::_ -> buri
170 | GrafiteAst.Dependency buri -> Some buri
175 (fun buri -> Hashtbl.add rev_deps buri baseuri_of_current_moo) deps)
177 let buris_to_remove =
179 (List.fast_sort Pervasives.compare
180 (List.flatten (List.map (Hashtbl.find_all rev_deps) buris)))
182 let objects_to_remove =
183 let objs_of_buri buri =
186 | Http_getter_types.Ls_object o ->
187 Some (buri ^ "/" ^ o.Http_getter_types.uri)
189 (Http_getter.ls buri)
191 List.flatten (List.map objs_of_buri (buris @ buris_to_remove))
195 let clean_baseuris ?(verbose=true) buris =
196 Hashtbl.clear cache_of_processed_baseuri;
197 let buris = List.map HGM.strip_trailing_slash buris in
198 debug_prerr "clean_baseuris called on:";
200 List.iter debug_prerr buris;
202 if Helm_registry.get_bool "db.nodb" then
203 close_using_moos buris
205 close_using_db [] buris
207 let l = HExtlib.list_uniq (List.fast_sort Pervasives.compare l) in
208 let l = List.map UriManager.uri_of_string l in
209 debug_prerr "clean_baseuri will remove:";
211 List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l;
214 MatitaMisc.safe_remove (MatitaMisc.obj_file_of_baseuri buri))
215 (HExtlib.list_uniq (List.fast_sort Pervasives.compare
216 (List.map (UriManager.buri_of_uri) l)));
217 List.iter (MatitaSync.remove ~verbose) l;
218 cleaned_no := !cleaned_no + List.length l;
219 if !cleaned_no > 30 then
224 ignore (HMysql.exec (MatitaDb.instance ()) ("OPTIMIZE TABLE " ^ table)))
225 [MetadataTypes.name_tbl (); MetadataTypes.rel_tbl ();
226 MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl();
227 MetadataTypes.count_tbl()]
230 let baseuri_of_file file =
231 let uri = ref None in
232 let ic = open_in file in
233 let istream = Ulexing.from_utf8_channel ic in
237 let stm = GrafiteParser.parse_statement istream in
238 match MatitaMisc.baseuri_of_baseuri_decl stm with
240 let u = MatitaMisc.strip_trailing_slash buri in
241 if String.length u < 5 || String.sub u 0 5 <> "cic:/" then
242 MatitaLog.error (file ^ " sets an incorrect baseuri: " ^ buri);
244 ignore(Http_getter.resolve u)
246 | Http_getter_types.Unresolvable_URI _ ->
247 MatitaLog.error (file ^ " sets an unresolvable baseuri: "^buri)
248 | Http_getter_types.Key_not_found _ -> ());
253 CicNotationParser.Parse_error _ as exn ->
254 prerr_endline ("Unable to parse: " ^ file);
255 prerr_endline (MatitaExcPp.to_string exn);
258 with End_of_file -> close_in ic);
261 | None -> failwith ("No baseuri defined in " ^ file)
263 let obj_file_of_script f =
264 if f = "coq.ma" then BuildTimeConf.coq_notation_script else
265 let baseuri = baseuri_of_file f in
266 MatitaMisc.obj_file_of_baseuri baseuri