matitacLib.cmo
-all: matita matitac matitatop cicbrowser matitadep
+all: matita matitac matitatop cicbrowser matitadep matitaclean
updater: $(LIB_DEPS)
$(OCAMLC) $(PKGS) -linkpkg -o $@ updater.ml
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"
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
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
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; *)
| 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...";
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
--- /dev/null
+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
+
projects / helm.git / commitdiff