From 76c28672a95473ee68935a7ca09b69f9b2f9cdc8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 30 Jun 2005 16:19:00 +0000 Subject: [PATCH] matitaclean anapshot --- helm/matita/Makefile.in | 11 ++- helm/matita/matitaDb.ml | 2 +- helm/matita/matitaSync.ml | 6 ++ helm/matita/matitaSync.mli | 3 + helm/matita/matitacLib.ml | 26 ++++--- helm/matita/matitaclean.ml | 136 +++++++++++++++++++++++++++++++++++++ 6 files changed, 171 insertions(+), 13 deletions(-) create mode 100644 helm/matita/matitaclean.ml diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index c7b250a3b..168dfa305 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -46,7 +46,7 @@ CCMOS = \ matitacLib.cmo -all: matita matitac matitatop cicbrowser matitadep +all: matita matitac matitatop cicbrowser matitadep matitaclean updater: $(LIB_DEPS) $(OCAMLC) $(PKGS) -linkpkg -o $@ updater.ml @@ -56,7 +56,7 @@ CMXS = $(patsubst %.cmo,%.cmx,$(CMOS)) CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS)) LIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(REQUIRES)) LIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(REQUIRES)) -opt: matita.opt matitac.opt cicbrowser.opt matitadep.opt +opt: matita.opt matitac.opt cicbrowser.opt matitadep.opt matitaclean.opt else opt: @echo "Native code compilation is disabled" @@ -80,6 +80,11 @@ matitadep: matitadep.ml $(LIB_DEPS) $(CCMOS) matitadep.opt: matitadep.ml $(LIB_DEPS) $(CCMXS) $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $< +matitaclean: matitaclean.ml $(LIB_DEPS) $(CCMOS) + $(OCAMLC) $(CPKGS) -linkpkg -o $@ $(CCMOS) $< +matitaclean.opt: matitaclean.ml $(LIB_DEPS) $(CCMXS) + $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $< + cicbrowser: matita @test -f $@ || ln -s $< $@ cicbrowser.opt: matita.opt @@ -109,7 +114,7 @@ distclean: clean rm -f matita.glade.bak matita.gladep.bak rm -rf autom4te.cache/ -tests: matita +tests: matitac @scripts/do_tests.sh ./matitac /dev/null tests/*.ma tests.opt: matitac.opt @scripts/do_tests.sh ./matitac.opt /dev/null tests/*.ma diff --git a/helm/matita/matitaDb.ml b/helm/matita/matitaDb.ml index 423fa2b5a..c5bdbf84b 100644 --- a/helm/matita/matitaDb.ml +++ b/helm/matita/matitaDb.ml @@ -112,7 +112,7 @@ let create_owner_environment () = (* removes uri from the ownerized tables, and returns the list of other objects * (theyr uris) that ref the one removed. * AFAIK there is no need to return it, since the MatitaTypes.staus should - * contain all defined objects. but to double ckeck we do not garbage the + * contain all defined objects. but to double check we do not garbage the * metadata... *) let remove_uri uri = diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml index df29edc3b..42e8f1c40 100644 --- a/helm/matita/matitaSync.ml +++ b/helm/matita/matitaSync.ml @@ -222,3 +222,9 @@ let alias_diff ~from status = acc) status.aliases Map.empty +let remove uri = + let path = Http_getter.resolve' uri in + remove_object_from_disk uri path; + remove_coercion uri; + ignore(MatitaDb.remove_uri uri) + diff --git a/helm/matita/matitaSync.mli b/helm/matita/matitaSync.mli index fa82d974f..0c866d4e5 100644 --- a/helm/matita/matitaSync.mli +++ b/helm/matita/matitaSync.mli @@ -36,3 +36,6 @@ val time_travel: val alias_diff: from:MatitaTypes.status -> MatitaTypes.status -> DisambiguateTypes.environment + (* removes the object from DB, Disk, CoercionsDB *) +val remove: UriManager.uri -> unit + diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index 4d04d371c..ea8888eb7 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -36,16 +36,14 @@ let usage = sprintf "MatitaC v%s\nUsage: matitac [option ...] file\nOptions:" BuildTimeConf.version -let _ = - Helm_registry.load_from "matita.conf.xml"; - Http_getter.init (); - MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); - MatitaDb.clean_owner_environment (); - MatitaDb.create_owner_environment () - -let status = ref (Lazy.force MatitaEngine.initial_status) ;; +let status = ref None let run_script is eval_function = + let status = + match !status with + | None -> assert false + | Some s -> s + in let slash_n_RE = Pcre.regexp "\\n" in let cb status stm = (* dump_status status; *) @@ -102,6 +100,12 @@ let rec go () = | exn -> MatitaLog.error (Printexc.to_string exn); go () let main ~mode = + Helm_registry.load_from "matita.conf.xml"; + Http_getter.init (); + MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); + MatitaDb.clean_owner_environment (); + MatitaDb.create_owner_environment (); + status := Some (ref (Lazy.force MatitaEngine.initial_status)); at_exit (fun () -> Http_getter_logger.log "Sync map tree to disk..."; @@ -130,7 +134,11 @@ let main ~mode = let hou = if tm.Unix.tm_hour > 0 then (string_of_int tm.Unix.tm_hour ^ "h ") else "" in - let proof_status = !status.proof_status in + let proof_status = + match !status with + | Some s -> !s.proof_status + | None -> assert false + in if proof_status <> MatitaTypes.No_proof then begin MatitaLog.error diff --git a/helm/matita/matitaclean.ml b/helm/matita/matitaclean.ml new file mode 100644 index 000000000..60292515a --- /dev/null +++ b/helm/matita/matitaclean.ml @@ -0,0 +1,136 @@ +module HGT = Http_getter_types;; +module HG = Http_getter;; +module UM = UriManager;; + +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 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; + exit 0 + end + else + List.iter + (fun u -> + prerr_endline ("Removing " ^ UM.string_of_uri u); + MatitaSync.remove u) + l + -- 2.39.2