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