1 module HGT = Http_getter_types;;
2 module HG = Http_getter;;
3 module UM = UriManager;;
6 Helm_registry.load_from "matita.conf.xml";
8 MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner")
11 MatitaDb.clean_owner_environment ();
12 MatitaDb.create_owner_environment ();
15 let dbd = MatitaDb.instance ()
17 let one_step_depend suri =
19 let suri = Mysql.escape suri in
20 (**** FIX FIX FIX ***)
21 (****** let obj_tbl = MetadataTypes.obj_tbl () in ******)
22 let obj_tbl = MetadataTypes.library_obj_tbl in
23 (**** FIX FIX FIX ***)
25 "SELECT source FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl suri
28 let rc = Mysql.exec dbd dbg_q in
30 Mysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l := a:: !l);
31 let l = List.sort Pervasives.compare !l in
32 MatitaMisc.list_uniq l
34 exn -> raise exn (* no errors should be accepted *)
36 let cache_of_processed_baseuri = Hashtbl.create 1024
38 let close_uri_list uri_to_remove =
39 (* to remove an uri you have to remove the whole script *)
42 (List.fast_sort Pervasives.compare
43 (List.map UM.buri_of_uri uri_to_remove))
45 (* cleand the already visided baseuris *)
49 if Hashtbl.mem cache_of_processed_baseuri buri then false
54 (fun buri -> Hashtbl.add cache_of_processed_baseuri buri true)
56 (* now calculate the list of objects that belong to these baseuris *)
60 let inhabitants = HG.ls buri in
61 let inhabitants = List.filter
62 (function HGT.Ls_object _ -> true | _ -> false)
65 let inhabitants = List.map
67 | HGT.Ls_object e -> UM.uri_of_string (buri ^ "/" ^ e.HGT.uri)
74 (* now we want the list of all uri that depend on them *)
77 (fun acc u -> one_step_depend (UM.string_of_uri u) @ acc) [] uri_to_remove
81 (List.fast_sort Pervasives.compare depend)
83 let depend = List.map UM.uri_of_string depend in
86 let main uri_to_remove =
87 let rec fix uris next =
90 | l -> let uris, next = close_uri_list l in fix uris next @ uris
93 (List.fast_sort Pervasives.compare (fix [] uri_to_remove))
97 prerr_endline "usage:";
98 prerr_endline "\tmatitaclean all";
99 prerr_endline "\tmatitaclean dry uris...";
100 prerr_endline "\tmatitaclean uris...";
107 Http_getter_logger.log "Sync map tree to disk...";
108 Http_getter.sync_dump_file ();
109 print_endline "\nThanks for using Matita!\n");
110 if Array.length Sys.argv < 2 then usage ();
111 if Sys.argv.(1) = "all" then clean_all ();
113 if Sys.argv.(1) = "dry" then 2, true else 1, false
115 let uri_to_remove =ref [] in
117 for i = start to Array.length Sys.argv - 1 do
118 let suri = Sys.argv.(i) in
119 let uri = UM.uri_of_string suri in
120 uri_to_remove := uri :: !uri_to_remove
123 Invalid_argument _ -> usage ();
124 let l = main !uri_to_remove in
127 List.iter (fun x -> let u = UM.string_of_uri x in prerr_endline u) l;
133 prerr_endline ("Removing " ^ UM.string_of_uri u);