helm/matita/matitaclean.ml

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