X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatitaclean.ml;h=5aabf7558dab32467027798a40446199f0fc3646;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=60292515ae11b598856128822507ece6f925c946;hpb=76c28672a95473ee68935a7ca09b69f9b2f9cdc8;p=helm.git diff --git a/helm/matita/matitaclean.ml b/helm/matita/matitaclean.ml index 60292515a..5aabf7558 100644 --- a/helm/matita/matitaclean.ml +++ b/helm/matita/matitaclean.ml @@ -1,136 +1,70 @@ -module HGT = Http_getter_types;; -module HG = Http_getter;; -module UM = UriManager;; +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) -let _ = - Helm_registry.load_from "matita.conf.xml"; - HG.init (); - MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner") +open Printf -let clean_all () = - MatitaDb.clean_owner_environment (); - MatitaDb.create_owner_environment (); - exit 0 - -let dbd = MatitaDb.instance () +module UM = UriManager +module TA = GrafiteAst -let one_step_depend suri = - let dbg_q = - let suri = Mysql.escape suri in - (**** FIX FIX FIX ***) - (****** let obj_tbl = MetadataTypes.obj_tbl () in ******) - let obj_tbl = MetadataTypes.library_obj_tbl in - (**** FIX FIX FIX ***) - Printf.sprintf - "SELECT source FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl suri - in - try - let rc = Mysql.exec dbd dbg_q 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 *) - -let cache_of_processed_baseuri = Hashtbl.create 1024 - -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 UM.buri_of_uri 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 - List.iter - (fun buri -> Hashtbl.add cache_of_processed_baseuri buri true) - buri_to_remove; - (* 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 -> UM.uri_of_string (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 (UM.string_of_uri u) @ acc) [] uri_to_remove - in - let depend = - MatitaMisc.list_uniq - (List.fast_sort Pervasives.compare depend) - in - let depend = List.map UM.uri_of_string depend in - uri_to_remove, depend - -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 uris..."; - prerr_endline "\tmatitaclean uris..."; - 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 = UM.uri_of_string 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 (fun x -> let u = UM.string_of_uri x in prerr_endline u) l; +let main () = + let _ = MatitaInit.initialize_all () in + let uris_to_remove = ref [] in + let files_to_remove = ref [] in + (match Helm_registry.get_list Helm_registry.string "matita.args" with + | [ "all" ] -> + MatitaDb.clean_owner_environment (); + let xmldir = Helm_registry.get "matita.basedir" ^ "/xml" in + ignore + (Sys.command + ("find " ^ xmldir ^ + " \\( -name \\*.xml.gz -o -name \\*.moo \\) " ^ + "-exec rm \\{\\} \\; 2> /dev/null")); + ignore + (Sys.command ("find " ^ xmldir ^ + " -type d -exec rmdir -p {} \\; 2> /dev/null")); exit 0 - end - else - List.iter - (fun u -> - prerr_endline ("Removing " ^ UM.string_of_uri u); - MatitaSync.remove u) - l - + | [] -> MatitaInit.die_usage () + | files -> + List.iter + (fun suri -> + let uri = + try + UM.buri_of_uri (UM.uri_of_string suri) + with UM.IllFormedUri _ -> + files_to_remove := suri :: !files_to_remove; + let u = MatitacleanLib.baseuri_of_file suri in + if String.length u < 5 || String.sub u 0 5 <> "cic:/" then begin + MatitaLog.error (sprintf "File %s defines a bad baseuri: %s" + suri u); + exit 1 + end else + u + in + uris_to_remove := uri :: !uris_to_remove) + files); + MatitacleanLib.clean_baseuris !uris_to_remove; + let moos = List.map MatitacleanLib.obj_file_of_script !files_to_remove in + List.iter MatitaMisc.safe_remove moos +