module HG = Http_getter;;
module HGM = Http_getter_misc;;
module UM = UriManager;;
-module TA = TacticAst;;
-
-let baseuri_of_baseuri_decl st =
- let module TA = TacticAst in
- match st with
- | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", buri))) ->
- Some buri
- | _ -> None
+module TA = GrafiteAst;;
let cache_of_processed_baseuri = Hashtbl.create 1024
in
(* now calculate the list of objects that belong to these baseuris *)
let uri_to_remove =
- List.fold_left
- (fun acc buri ->
- let inhabitants = HG.ls (buri ^ "/") in
- let inhabitants = List.filter
- (function HGT.Ls_object _ -> true | _ -> false)
- inhabitants
- in
- let inhabitants = List.map
- (function
- | HGT.Ls_object e -> buri ^ "/" ^ e.HGT.uri
- | _ -> assert false)
- inhabitants
- in
- inhabitants @ acc)
- [] buri_to_remove
+ try
+ List.fold_left
+ (fun acc buri ->
+ let inhabitants = HG.ls (buri ^ "/") in
+ let inhabitants = List.filter
+ (function HGT.Ls_object _ -> true | _ -> false)
+ inhabitants
+ in
+ let inhabitants = List.map
+ (function
+ | HGT.Ls_object e -> buri ^ "/" ^ e.HGT.uri
+ | _ -> assert false)
+ inhabitants
+ in
+ inhabitants @ acc)
+ [] buri_to_remove
+ with HGT.Invalid_URI u ->
+ MatitaLog.error ("We were listing an invalid buri: " ^ u);
+ exit 1
in
(* now we want the list of all uri that depend on them *)
let depend =
in
uri_to_remove, depend
-let baseuri_of_file file =
- let ic = open_in file in
- let stms = CicTextualParser2.parse_statements (Stream.of_channel ic) in
- close_in ic;
- let uri = ref "" in
- List.iter
- (fun stm ->
- match baseuri_of_baseuri_decl stm with
- | Some buri -> uri := MatitaMisc.strip_trailing_slash buri
- | None -> ())
- stms;
- !uri
-
-let rec fix uris next =
+let rec close uris next =
match next with
| [] -> uris
- | l -> let uris, next = close_uri_list l in fix uris next @ uris
+ | l -> let uris, next = close_uri_list l in close uris next @ uris
+let cleaned_no = ref 0;;
+
let clean_baseuris ?(verbose=true) buris =
Hashtbl.clear cache_of_processed_baseuri;
let buris = List.map HGM.strip_trailing_slash buris in
debug_prerr "clean_baseuris called on:";
if debug then
List.iter debug_prerr buris;
- let l = fix [] buris in
+ let l = close [] buris in
let l = MatitaMisc.list_uniq (List.fast_sort Pervasives.compare l) in
let l = List.map UriManager.uri_of_string l in
debug_prerr "clean_baseuri will remove:";
if debug then
List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l;
- List.iter (MatitaSync.remove ~verbose) l
-
-let is_empty buri = HG.ls (HGM.strip_trailing_slash buri ^ "/") = []
-
+ Hashtbl.iter
+ (fun buri _ ->
+ MatitaMisc.safe_remove (MatitaMisc.obj_file_of_baseuri buri)
+ ) cache_of_processed_baseuri;
+ List.iter (MatitaSync.remove ~verbose) l;
+ cleaned_no := !cleaned_no + List.length l;
+ if !cleaned_no > 30 then
+ List.iter
+ (function table ->
+ ignore (Mysql.exec (MatitaDb.instance ()) ("OPTIMIZE TABLE " ^ table)))
+ [MetadataTypes.name_tbl (); MetadataTypes.rel_tbl ();
+ MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl();
+ MetadataTypes.count_tbl()]