]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/library/libraryClean.ml
handles bad Appl
[helm.git] / helm / software / components / library / libraryClean.ml
1 (* Copyright (C) 2005, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://helm.cs.unibo.it/
24  *)
25
26 (* $Id$ *)
27
28 open Printf
29
30 let debug = false
31 let debug_prerr = if debug then prerr_endline else ignore
32
33 module HGT = Http_getter_types;;
34 module HG = Http_getter;;
35 module UM = UriManager;;
36
37
38 let strip_xpointer s = Pcre.replace ~pat:"#.*$" s ;;
39
40 let safe_buri_of_suri suri =
41   try
42     UM.buri_of_uri (UM.uri_of_string suri)
43   with
44     UM.IllFormedUri _ -> suri
45
46 let one_step_depend cache_of_processed_baseuri suri dbtype dbd =
47   let buri = safe_buri_of_suri suri in
48   if Hashtbl.mem cache_of_processed_baseuri buri then 
49     []
50   else
51     begin
52       Hashtbl.add cache_of_processed_baseuri buri true;
53       let query = 
54         let buri = buri ^ "/" in 
55         let buri = HSql.escape dbtype dbd buri in
56         let obj_tbl = MetadataTypes.obj_tbl () in
57         if HSql.isMysql dbtype dbd then        
58           sprintf ("SELECT source, h_occurrence FROM %s WHERE " 
59             ^^ "h_occurrence REGEXP '"^^
60             "^%s\\([^/]+\\|[^/]+#xpointer.*\\)$"^^"'")
61           obj_tbl buri
62         else
63           begin
64             sprintf ("SELECT source, h_occurrence FROM %s WHERE " 
65             ^^ "REGEXP(h_occurrence, '"^^
66             "^%s\\([^/]+\\|[^/]+#xpointer.*\\)$"^^"')")
67             obj_tbl buri
68             (* implementation with vanilla ocaml-sqlite3
69             HLog.debug "Warning SELECT without REGEXP";
70             sprintf
71               ("SELECT source, h_occurrence FROM %s WHERE " ^^ 
72                "h_occurrence LIKE '%s%%' " ^^ HSql.escape_string_for_like)
73                   obj_tbl buri*)
74           end
75       in
76       try 
77         let rc = HSql.exec dbtype dbd query in
78         let l = ref [] in
79         HSql.iter rc (
80           fun row -> 
81             match row.(0), row.(1) with 
82             | Some uri, Some occ when 
83                 Filename.dirname (strip_xpointer occ) = buri -> 
84                   l := uri :: !l
85             | _ -> ());
86         let l = List.sort Pervasives.compare !l in
87         HExtlib.list_uniq l
88       with
89         exn -> raise exn (* no errors should be accepted *)
90     end
91     
92 let db_uris_of_baseuri buri =
93  let dbd = LibraryDb.instance () in
94  let dbtype = 
95    if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User
96  in
97  let query = 
98   let buri = buri ^ "/" in 
99   let buri = HSql.escape dbtype dbd buri in
100   let obj_tbl = MetadataTypes.name_tbl () in
101   if HSql.isMysql dbtype dbd then        
102     sprintf ("SELECT source FROM %s WHERE " 
103     ^^ "source REGEXP '^%s[^/]*(#xpointer.*)?$'") obj_tbl buri
104   else
105    begin
106     sprintf ("SELECT source FROM %s WHERE " 
107       ^^ "REGEXP(source, '^%s[^/]*\\(#xpointer.*\\)?$')") obj_tbl buri
108    end
109  in
110  try 
111   let rc = HSql.exec dbtype dbd query in
112   let l = ref [] in
113   HSql.iter rc (
114     fun row -> 
115       match row.(0) with 
116       | Some uri when Filename.dirname (strip_xpointer uri) = buri -> 
117           l := uri :: !l
118       | _ -> ());
119   let l = List.sort Pervasives.compare !l in
120   HExtlib.list_uniq l
121  with
122   exn -> raise exn (* no errors should be accepted *)
123 ;;
124
125 let close_uri_list cache_of_processed_baseuri uri_to_remove =
126   let dbd = LibraryDb.instance () in
127   let dbtype = 
128     if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User
129   in
130   (* to remove an uri you have to remove the whole script *)
131   let buri_to_remove = 
132     HExtlib.list_uniq 
133       (List.fast_sort Pervasives.compare 
134         (List.map safe_buri_of_suri uri_to_remove))
135   in
136   (* cleand the already visided baseuris *)
137   let buri_to_remove = 
138     List.filter 
139       (fun buri -> 
140         if Hashtbl.mem cache_of_processed_baseuri buri then false
141         else true)
142       buri_to_remove
143   in
144   (* now calculate the list of objects that belong to these baseuris *)
145   let uri_to_remove = 
146     try
147       List.fold_left 
148         (fun acc buri ->
149           let inhabitants = HG.ls ~local:true (buri ^ "/") in
150           let inhabitants = List.filter 
151               (function HGT.Ls_object _ -> true | _ -> false) 
152             inhabitants
153           in
154           let inhabitants = List.map 
155               (function 
156                | HGT.Ls_object e -> buri ^ "/" ^ e.HGT.uri 
157                | _ -> assert false)
158             inhabitants
159           in
160           inhabitants @ acc)
161       [] buri_to_remove 
162     with HGT.Invalid_URI u -> 
163       HLog.error ("We were listing an invalid buri: " ^ u);
164       exit 1
165   in
166   let uri_to_remove_from_db =
167    List.fold_left 
168      (fun acc buri -> 
169        let dbu = db_uris_of_baseuri buri in
170        dbu @ acc
171      ) [] buri_to_remove 
172   in
173   let uri_to_remove = uri_to_remove @ uri_to_remove_from_db in
174   let uri_to_remove =
175    HExtlib.list_uniq (List.sort Pervasives.compare uri_to_remove) in
176   (* now we want the list of all uri that depend on them *) 
177   let depend = 
178     List.fold_left
179     (fun acc u -> one_step_depend cache_of_processed_baseuri u dbtype dbd @ acc)
180     [] uri_to_remove
181   in
182   let depend = 
183     HExtlib.list_uniq (List.fast_sort Pervasives.compare depend) 
184   in
185   uri_to_remove, depend
186 ;;
187
188 let rec close_db cache_of_processed_baseuri uris next =
189   match next with
190   | [] -> uris
191   | l -> 
192      let uris, next = close_uri_list cache_of_processed_baseuri l in
193      close_db cache_of_processed_baseuri uris next @ uris
194 ;;
195   
196 let cleaned_no = ref 0;;
197
198   (** TODO repellent code ... *)
199 let moo_root_dir = lazy (
200   let url =
201     List.assoc "cic:/matita/"
202       (List.map
203         (fun pair ->
204           match
205             Str.split (Str.regexp "[ \t\r\n]+") (HExtlib.trim_blanks pair)
206           with
207           | a::b::_ -> a, b
208           | _ -> assert false)
209         (Helm_registry.get_list Helm_registry.string "getter.prefix"))
210   in
211   String.sub url 7 (String.length url - 7))
212 ;;
213
214 let clean_baseuris ?(verbose=true) buris =
215   let cache_of_processed_baseuri = Hashtbl.create 1024 in
216   let dbd = LibraryDb.instance () in
217   let dbtype = 
218     if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User
219   in
220   Hashtbl.clear cache_of_processed_baseuri;
221   let buris = List.map Http_getter_misc.strip_trailing_slash buris in
222   debug_prerr "clean_baseuris called on:";
223   if debug then
224     List.iter debug_prerr buris; 
225   let l = close_db cache_of_processed_baseuri [] buris in
226   let l = HExtlib.list_uniq (List.fast_sort Pervasives.compare l) in
227   let l = List.map UriManager.uri_of_string l in
228   debug_prerr "clean_baseuri will remove:";
229   if debug then
230     List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l; 
231   List.iter
232    (fun baseuri ->
233      try 
234       let obj_file =
235        LibraryMisc.obj_file_of_baseuri ~must_exist:false ~writable:true ~baseuri
236       in
237        HExtlib.safe_remove obj_file ;
238        HExtlib.safe_remove 
239          (LibraryMisc.lexicon_file_of_baseuri 
240            ~must_exist:false ~writable:true ~baseuri) ;
241        HExtlib.rmdir_descend (Filename.chop_extension obj_file)
242      with Http_getter_types.Key_not_found _ -> ())
243    (HExtlib.list_uniq (List.fast_sort Pervasives.compare
244      (List.map (UriManager.buri_of_uri) l @ buris)));
245   List.iter
246    (let last_baseuri = ref "" in
247     fun uri ->
248      let buri = UriManager.buri_of_uri uri in
249      if buri <> !last_baseuri then
250       begin
251         if not (Helm_registry.get_bool "matita.verbose") then
252             (print_endline ("matitaclean " ^ buri ^ "/");flush stdout)
253           else 
254             HLog.message ("Removing: " ^ buri ^ "/*");
255        last_baseuri := buri
256       end;
257      LibrarySync.remove_obj uri
258    ) l;
259   if HSql.isMysql dbtype dbd then
260    begin
261    cleaned_no := !cleaned_no + List.length l;
262    if !cleaned_no > 30 && HSql.isMysql dbtype dbd then
263     begin
264      cleaned_no := 0;
265      List.iter
266       (function table ->
267         ignore (HSql.exec dbtype dbd ("OPTIMIZE TABLE " ^ table)))
268       [MetadataTypes.name_tbl (); MetadataTypes.rel_tbl ();
269        MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl();
270        MetadataTypes.count_tbl()]
271     end
272    end