module HGT = Http_getter_types;; module HG = Http_getter;; module UM = UriManager;; module TA = TacticAst;; let _ = Helm_registry.load_from "matita.conf.xml"; HG.init (); MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner") let clean_all () = MatitaDb.clean_owner_environment (); MatitaDb.create_owner_environment (); exit 0 let dbd = MatitaDb.instance () let cache_of_processed_baseuri = Hashtbl.create 1024 let one_step_depend suri = let buri = try UM.buri_of_uri (UM.uri_of_string suri) with UM.IllFormedUri _ -> suri in if Hashtbl.mem cache_of_processed_baseuri buri then [] else begin Hashtbl.add cache_of_processed_baseuri buri true; let query = let buri = buri ^ "/" in let buri = Mysql.escape buri in let obj_tbl = MetadataTypes.obj_tbl () in Printf.sprintf "SELECT source FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl buri in try let rc = Mysql.exec dbd query in let l = ref [] in Mysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l:=a:: !l); let l = List.sort Pervasives.compare !l in MatitaMisc.list_uniq l with exn -> raise exn (* no errors should be accepted *) end let safe_buri_of_suri suri = try UM.buri_of_uri (UM.uri_of_string suri) with UM.IllFormedUri _ -> suri let close_uri_list uri_to_remove = (* to remove an uri you have to remove the whole script *) let buri_to_remove = MatitaMisc.list_uniq (List.fast_sort Pervasives.compare (List.map safe_buri_of_suri uri_to_remove)) in (* cleand the already visided baseuris *) let buri_to_remove = List.filter (fun buri -> if Hashtbl.mem cache_of_processed_baseuri buri then false else true) buri_to_remove 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 in (* now we want the list of all uri that depend on them *) let depend = List.fold_left (fun acc u -> one_step_depend u @ acc) [] uri_to_remove in let depend = MatitaMisc.list_uniq (List.fast_sort Pervasives.compare depend) in uri_to_remove, depend let buri_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 (function | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", buri))) -> uri := MatitaMisc.strip_trailing_slash buri | _ -> ()) stms; !uri let main uri_to_remove = let rec fix uris next = match next with | [] -> uris | l -> let uris, next = close_uri_list l in fix uris next @ uris in MatitaMisc.list_uniq (List.fast_sort Pervasives.compare (fix [] uri_to_remove)) let usage () = prerr_endline ""; prerr_endline "usage:"; prerr_endline "\tmatitaclean all"; prerr_endline "\tmatitaclean dry (uri|file)+"; prerr_endline "\tmatitaclean (uri|file)+"; prerr_endline ""; exit 1 let _ = at_exit (fun () -> Http_getter_logger.log "Sync map tree to disk..."; Http_getter.sync_dump_file (); print_endline "\nThanks for using Matita!\n"); if Array.length Sys.argv < 2 then usage (); if Sys.argv.(1) = "all" then clean_all (); let start, dry = if Sys.argv.(1) = "dry" then 2, true else 1, false in let uri_to_remove =ref [] in (try for i = start to Array.length Sys.argv - 1 do let suri = Sys.argv.(i) in let uri = try UM.buri_of_uri (UM.uri_of_string suri) with UM.IllFormedUri _ -> buri_of_file suri in uri_to_remove := uri :: !uri_to_remove done with Invalid_argument _ -> usage ()); let l = main !uri_to_remove in if dry then begin List.iter prerr_endline l; exit 0 end else List.iter (fun u -> prerr_endline ("Removing " ^ u); try MatitaSync.remove (UM.uri_of_string u) with Sys_error _ -> ()) l