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