helm/matita/matitaclean.ml

   1 module HGT = Http_getter_types;;
   2 module HG = Http_getter;;
   3 module UM = UriManager;;
   4
   5 let _ =
   6   Helm_registry.load_from "matita.conf.xml";
   7   HG.init ();
   8   MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner")
   9
  10 let clean_all () =
  11   MatitaDb.clean_owner_environment ();
  12   MatitaDb.create_owner_environment ();
  13   exit 0
  14
  15 let dbd = MatitaDb.instance ()
  16
  17 let one_step_depend suri =
  18   let dbg_q =
  19     let suri = Mysql.escape suri in
  20     (**** FIX FIX FIX ***)
  21     (****** let obj_tbl = MetadataTypes.obj_tbl () in  ******)
  22     let obj_tbl = MetadataTypes.library_obj_tbl in
  23     (**** FIX FIX FIX ***)
  24     Printf.sprintf
  25       "SELECT source FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl suri
  26   in
  27   try
  28     let rc = Mysql.exec dbd dbg_q in
  29     let l = ref [] in
  30     Mysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l := a:: !l);
  31     let l = List.sort Pervasives.compare !l in
  32     MatitaMisc.list_uniq l
  33   with
  34     exn -> raise exn (* no errors should be accepted *)
  35
  36 let cache_of_processed_baseuri = Hashtbl.create 1024
  37
  38 let close_uri_list uri_to_remove =
  39   (* to remove an uri you have to remove the whole script *)
  40   let buri_to_remove =
  41     MatitaMisc.list_uniq
  42       (List.fast_sort Pervasives.compare
  43         (List.map UM.buri_of_uri uri_to_remove))
  44   in
  45   (* cleand the already visided baseuris *)
  46   let buri_to_remove =
  47     List.filter
  48       (fun buri ->
  49         if Hashtbl.mem cache_of_processed_baseuri buri then false
  50         else true)
  51       buri_to_remove
  52   in
  53   List.iter
  54     (fun buri -> Hashtbl.add cache_of_processed_baseuri buri true)
  55     buri_to_remove;
  56   (* now calculate the list of objects that belong to these baseuris *)
  57   let uri_to_remove =
  58     List.fold_left
  59       (fun acc buri ->
  60         let inhabitants = HG.ls buri in
  61         let inhabitants = List.filter
  62             (function HGT.Ls_object _ -> true | _ -> false)
  63           inhabitants
  64         in
  65         let inhabitants = List.map
  66             (function
  67              | HGT.Ls_object e -> UM.uri_of_string (buri ^ "/" ^ e.HGT.uri)
  68              | _ -> assert false)
  69           inhabitants
  70         in
  71         inhabitants @ acc)
  72     [] buri_to_remove
  73   in
  74   (* now we want the list of all uri that depend on them *)
  75   let depend =
  76     List.fold_left
  77     (fun acc u -> one_step_depend (UM.string_of_uri u) @ acc) [] uri_to_remove
  78   in
  79   let depend =
  80     MatitaMisc.list_uniq
  81       (List.fast_sort Pervasives.compare depend)
  82   in
  83   let depend = List.map UM.uri_of_string depend in
  84   uri_to_remove, depend
  85
  86 let main uri_to_remove =
  87   let rec fix uris next =
  88     match next with
  89     | [] -> uris
  90     | l -> let uris, next = close_uri_list l in fix uris next @ uris
  91   in
  92   MatitaMisc.list_uniq
  93     (List.fast_sort Pervasives.compare (fix [] uri_to_remove))
  94
  95 let usage () =
  96   prerr_endline "";
  97   prerr_endline "usage:";
  98   prerr_endline "\tmatitaclean all";
  99   prerr_endline "\tmatitaclean dry uris...";
 100   prerr_endline "\tmatitaclean uris...";
 101   prerr_endline "";
 102   exit 1
 103
 104 let _ =
 105   at_exit
 106     (fun () ->
 107        Http_getter_logger.log "Sync map tree to disk...";
 108        Http_getter.sync_dump_file ();
 109        print_endline "\nThanks for using Matita!\n");
 110   if Array.length Sys.argv < 2 then usage ();
 111   if Sys.argv.(1) = "all" then clean_all ();
 112   let start, dry =
 113     if Sys.argv.(1) = "dry" then 2, true else 1, false
 114   in
 115   let uri_to_remove =ref [] in
 116   try
 117     for i = start to Array.length Sys.argv - 1 do
 118       let suri = Sys.argv.(i) in
 119       let uri = UM.uri_of_string suri in
 120       uri_to_remove := uri :: !uri_to_remove
 121     done
 122   with
 123     Invalid_argument _ -> usage ();
 124   let l = main !uri_to_remove in
 125   if dry then
 126     begin
 127       List.iter (fun x -> let u = UM.string_of_uri x in prerr_endline u) l;
 128       exit 0
 129     end
 130   else
 131     List.iter
 132       (fun u ->
 133         prerr_endline ("Removing " ^ UM.string_of_uri u);
 134         MatitaSync.remove u)
 135     l
 136