]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/matitacleanLib.ml
- added support for "-nodb" flag (still missing support for matitaclean which relies...
[helm.git] / helm / matita / matitacleanLib.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 open Printf
27
28 let debug = false
29 let debug_prerr = if debug then prerr_endline else ignore
30
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;;
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 h_occurrence LIKE '%s%%'"
56             obj_tbl buri
57       in
58       try 
59         let rc = HMysql.exec (MatitaDb.instance ()) query in
60         let l = ref [] in
61         HMysql.iter rc (
62           fun row -> 
63             match row.(0), row.(1) with 
64             | Some uri, Some occ when Filename.dirname occ = buri -> 
65                 l := uri :: !l
66             | _ -> ());
67         let l = List.sort Pervasives.compare !l in
68         HExtlib.list_uniq l
69       with
70         exn -> raise exn (* no errors should be accepted *)
71     end
72     
73 let safe_buri_of_suri suri =
74   try
75     UM.buri_of_uri (UM.uri_of_string suri)
76   with
77     UM.IllFormedUri _ -> suri
78
79 let close_uri_list uri_to_remove =
80   (* to remove an uri you have to remove the whole script *)
81   let buri_to_remove = 
82     HExtlib.list_uniq 
83       (List.fast_sort Pervasives.compare 
84         (List.map safe_buri_of_suri uri_to_remove))
85   in
86   (* cleand the already visided baseuris *)
87   let buri_to_remove = 
88     List.filter 
89       (fun buri -> 
90         if Hashtbl.mem cache_of_processed_baseuri buri then false
91         else true)
92       buri_to_remove
93   in
94   (* now calculate the list of objects that belong to these baseuris *)
95   let uri_to_remove = 
96     try
97       List.fold_left 
98         (fun acc buri ->
99           let inhabitants = HG.ls (buri ^ "/") in
100           let inhabitants = List.filter 
101               (function HGT.Ls_object _ -> true | _ -> false) 
102             inhabitants
103           in
104           let inhabitants = List.map 
105               (function 
106                | HGT.Ls_object e -> buri ^ "/" ^ e.HGT.uri 
107                | _ -> assert false)
108             inhabitants
109           in
110           inhabitants @ acc)
111       [] buri_to_remove 
112     with HGT.Invalid_URI u -> 
113       MatitaLog.error ("We were listing an invalid buri: " ^ u);
114       exit 1
115   in
116   (* now we want the list of all uri that depend on them *) 
117   let depend = 
118     List.fold_left
119     (fun acc u -> one_step_depend u @ acc) [] uri_to_remove
120   in
121   let depend = 
122     HExtlib.list_uniq (List.fast_sort Pervasives.compare depend) 
123   in
124   uri_to_remove, depend
125
126 let rec close uris next =
127   match next with
128   | [] -> uris
129   | l -> let uris, next = close_uri_list l in close uris next @ uris
130   
131 let cleaned_no = ref 0;;
132
133 let clean_baseuris ?(verbose=true) buris =
134   Hashtbl.clear cache_of_processed_baseuri;
135   let buris = List.map HGM.strip_trailing_slash buris in
136   debug_prerr "clean_baseuris called on:";
137   if debug then
138     List.iter debug_prerr buris; 
139   let l = close [] buris in
140   let l = HExtlib.list_uniq (List.fast_sort Pervasives.compare l) in
141   let l = List.map UriManager.uri_of_string l in
142   debug_prerr "clean_baseuri will remove:";
143   if debug then
144     List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l; 
145   Hashtbl.iter
146    (fun buri _ ->
147      MatitaMisc.safe_remove (MatitaMisc.obj_file_of_baseuri buri)) 
148    cache_of_processed_baseuri;
149   List.iter (MatitaSync.remove ~verbose) l;
150   cleaned_no := !cleaned_no + List.length l;
151   if !cleaned_no > 30 then
152    begin
153     cleaned_no := 0;
154     List.iter
155      (function table ->
156        ignore (HMysql.exec (MatitaDb.instance ()) ("OPTIMIZE TABLE " ^ table)))
157      [MetadataTypes.name_tbl (); MetadataTypes.rel_tbl ();
158       MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl();
159       MetadataTypes.count_tbl()]
160    end
161