From ee3f2aa5b78aa77555e5e81d5a2d92501889649e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 4 Jul 2005 09:59:57 +0000 Subject: [PATCH] matitaclean splitted in matitacleanLib and matitaclean. --- helm/matita/.depend | 20 +++-- helm/matita/Makefile.in | 13 ++-- helm/matita/matitaDb.ml | 5 ++ helm/matita/matitaDb.mli | 3 +- helm/matita/matitaclean.ml | 138 +++------------------------------ helm/matita/matitacleanLib.ml | 110 ++++++++++++++++++++++++++ helm/matita/matitacleanLib.mli | 27 +++++++ 7 files changed, 172 insertions(+), 144 deletions(-) create mode 100644 helm/matita/matitacleanLib.ml create mode 100644 helm/matita/matitacleanLib.mli diff --git a/helm/matita/.depend b/helm/matita/.depend index 7a633f990..d85173458 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -1,9 +1,9 @@ matita.cmo: matitaTypes.cmo matitaScript.cmi matitaMisc.cmi \ matitaMathView.cmi matitaLog.cmi matitaGui.cmi matitaGtkMisc.cmi \ - matitaEngine.cmi matitaDisambiguator.cmi matitaDb.cmi buildTimeConf.cmo + matitaEngine.cmi matitaDisambiguator.cmi buildTimeConf.cmo matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ matitaMathView.cmx matitaLog.cmx matitaGui.cmx matitaGtkMisc.cmx \ - matitaEngine.cmx matitaDisambiguator.cmx matitaDb.cmx buildTimeConf.cmx + matitaEngine.cmx matitaDisambiguator.cmx buildTimeConf.cmx matitaDb.cmo: matitaMisc.cmi matitaDb.cmi matitaDb.cmx: matitaMisc.cmx matitaDb.cmi matitaDisambiguator.cmo: matitaTypes.cmo matitaDisambiguator.cmi @@ -47,13 +47,17 @@ matitaTypes.cmx: matitaLog.cmx matitac.cmo: matitacLib.cmi matitac.cmx: matitacLib.cmx matitacLib.cmo: matitaTypes.cmo matitaMisc.cmi matitaLog.cmi matitaExcPp.cmi \ - matitaEngine.cmi matitaDb.cmi buildTimeConf.cmo matitacLib.cmi + matitaEngine.cmi buildTimeConf.cmo matitacLib.cmi matitacLib.cmx: matitaTypes.cmx matitaMisc.cmx matitaLog.cmx matitaExcPp.cmx \ - matitaEngine.cmx matitaDb.cmx buildTimeConf.cmx matitacLib.cmi -matitaclean.cmo: matitaSync.cmi matitaMisc.cmi matitaDb.cmi -matitaclean.cmx: matitaSync.cmx matitaMisc.cmx matitaDb.cmx -matitadep.cmo: matitaMisc.cmi -matitadep.cmx: matitaMisc.cmx + matitaEngine.cmx buildTimeConf.cmx matitacLib.cmi +matitaclean.cmo: matitacleanLib.cmi matitaDb.cmi +matitaclean.cmx: matitacleanLib.cmx matitaDb.cmx +matitacleanLib.cmo: matitaSync.cmi matitaMisc.cmi matitaDb.cmi \ + matitacleanLib.cmi +matitacleanLib.cmx: matitaSync.cmx matitaMisc.cmx matitaDb.cmx \ + matitacleanLib.cmi +matitadep.cmo: matitaMisc.cmi matitaExcPp.cmi +matitadep.cmx: matitaMisc.cmx matitaExcPp.cmx matitaDisambiguator.cmi: matitaTypes.cmo matitaEngine.cmi: matitaTypes.cmo matitaGtkMisc.cmi: matitaGeneratedGui.cmi diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index 9b26d4d08..d1eff032a 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -29,13 +29,14 @@ CMOS = \ matitaMisc.cmo \ matitaDb.cmo \ matitaSync.cmo \ + matitacleanLib.cmo \ matitaDisambiguator.cmo \ matitaEngine.cmo \ matitaScript.cmo \ matitaGeneratedGui.cmo \ matitaGtkMisc.cmo \ matitaGui.cmo \ - matitaMathView.cmo + matitaMathView.cmo # objects for matitac (batch compiler) CCMOS = \ buildTimeConf.cmo \ @@ -48,6 +49,7 @@ CCMOS = \ matitaDisambiguator.cmo \ matitaEngine.cmo \ matitacLib.cmo +CLEANCMOS = $(CCMOS) matitacleanLib.cmo all: matita matitac matitatop cicbrowser matitadep matitaclean @@ -58,6 +60,7 @@ updater: $(LIB_DEPS) ifeq ($(HAVE_OCAMLOPT),yes) CMXS = $(patsubst %.cmo,%.cmx,$(CMOS)) CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS)) +CLEANCMXS = $(patsubst %.cmo,%.cmx,$(CLEANCMOS)) LIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(REQUIRES)) LIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(REQUIRES)) CLIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(CREQUIRES)) @@ -90,10 +93,10 @@ matitadep: matitadep.ml $(DEPLIB_DEPS) $(CCMOS) matitadep.opt: matitadep.ml $(DEPLIB_DEPS) $(CCMXS) $(OCAMLOPT) $(DEPPKGS) -linkpkg -o $@ $(CCMXS) $< -matitaclean: matitaclean.ml $(CLEANLIB_DEPS) $(CCMOS) - $(OCAMLC) $(CLEANPKGS) -linkpkg -o $@ $(CCMOS) $< -matitaclean.opt: matitaclean.ml $(CLEANLIB_DEPS) $(CCMXS) - $(OCAMLOPT) $(CLEANPKGS) -linkpkg -o $@ $(CCMXS) $< +matitaclean: matitaclean.ml $(CLEANLIB_DEPS) $(CLEANCMOS) + $(OCAMLC) $(CLEANPKGS) -linkpkg -o $@ $(CLEANCMOS) $< +matitaclean.opt: matitaclean.ml $(CLEANLIB_DEPS) $(CLEANCMXS) + $(OCAMLOPT) $(CLEANPKGS) -linkpkg -o $@ $(CLEANCMXS) $< cicbrowser: matita @test -f $@ || ln -s $< $@ diff --git a/helm/matita/matitaDb.ml b/helm/matita/matitaDb.ml index 17aac3745..b8f91a342 100644 --- a/helm/matita/matitaDb.ml +++ b/helm/matita/matitaDb.ml @@ -161,3 +161,8 @@ let xpointers_of_ind uri = let l = ref [] in Mysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l := a:: !l); List.map UriManager.uri_of_string !l + +let reset_owner_environment () = + clean_owner_environment (); + create_owner_environment () + diff --git a/helm/matita/matitaDb.mli b/helm/matita/matitaDb.mli index 3b3bd58c1..b7b7c273f 100644 --- a/helm/matita/matitaDb.mli +++ b/helm/matita/matitaDb.mli @@ -25,8 +25,7 @@ val instance: unit -> Mysql.dbd -val clean_owner_environment : unit -> unit -val create_owner_environment : unit -> unit +val reset_owner_environment : unit -> unit val remove_uri: UriManager.uri -> string list val xpointers_of_ind: UriManager.uri -> UriManager.uri list diff --git a/helm/matita/matitaclean.ml b/helm/matita/matitaclean.ml index c24e94d44..6a3ce06b3 100644 --- a/helm/matita/matitaclean.ml +++ b/helm/matita/matitaclean.ml @@ -8,120 +8,12 @@ let _ = 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 main uri_to_remove = MatitacleanLib.clean_baseuris 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 @@ -133,36 +25,24 @@ let _ = 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 + if Sys.argv.(1) = "all" then + begin + MatitaDb.reset_owner_environment (); + exit 0 + end let uri_to_remove =ref [] in (try - for i = start to Array.length Sys.argv - 1 do + for i = 1 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 + UM.IllFormedUri _ -> MatitacleanLib.baseuri_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 + main !uri_to_remove diff --git a/helm/matita/matitacleanLib.ml b/helm/matita/matitacleanLib.ml new file mode 100644 index 000000000..992443a35 --- /dev/null +++ b/helm/matita/matitacleanLib.ml @@ -0,0 +1,110 @@ +module HGT = Http_getter_types;; +module HG = Http_getter;; +module UM = UriManager;; +module TA = TacticAst;; + +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 (MatitaDb.instance ()) 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 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 + (function + | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", buri))) -> + uri := MatitaMisc.strip_trailing_slash buri + | _ -> ()) + stms; + !uri + +let rec fix uris next = + match next with + | [] -> uris + | l -> let uris, next = close_uri_list l in fix uris next @ uris + +let clean_baseuris buris = + let l = fix [] buris in + let l = MatitaMisc.list_uniq (List.fast_sort Pervasives.compare l) in + let l = List.map UriManager.uri_of_string l in + List.iter MatitaSync.remove l + diff --git a/helm/matita/matitacleanLib.mli b/helm/matita/matitacleanLib.mli new file mode 100644 index 000000000..f93d6eb96 --- /dev/null +++ b/helm/matita/matitacleanLib.mli @@ -0,0 +1,27 @@ +(* Copyright (C) 2004-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/ + *) + +val clean_baseuris : string list -> unit +val baseuri_of_file : string -> string -- 2.39.2