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