X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitacleanLib.ml;h=82fac08af78a1a7516719a9ab78733be4e1e8e5d;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=51635a30a130426a9986b829c34f2fe00d0fcff4;hpb=b8193e0717e01edfcf826a6edce0866496537e8a;p=helm.git diff --git a/helm/matita/matitacleanLib.ml b/helm/matita/matitacleanLib.ml index 51635a30a..82fac08af 100644 --- a/helm/matita/matitacleanLib.ml +++ b/helm/matita/matitacleanLib.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +open Printf + let debug = false let debug_prerr = if debug then prerr_endline else ignore @@ -32,12 +34,6 @@ module HGM = Http_getter_misc;; module UM = UriManager;; module TA = GrafiteAst;; -let baseuri_of_baseuri_decl st = - match st with - | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", buri))) -> - Some buri - | _ -> None - let cache_of_processed_baseuri = Hashtbl.create 1024 let one_step_depend suri = @@ -53,26 +49,27 @@ let one_step_depend suri = Hashtbl.add cache_of_processed_baseuri buri true; let query = let buri = buri ^ "/" in - let buri = Mysql.escape buri in + let buri = HMysql.escape buri in let obj_tbl = MetadataTypes.obj_tbl () in - Printf.sprintf - "SELECT source, h_occurrence FROM %s WHERE h_occurrence LIKE '%s%%'" obj_tbl buri + sprintf + ("SELECT source, h_occurrence FROM %s WHERE " ^^ + "h_occurrence REGEXP '^%s[^/]*$'") + obj_tbl buri in try - let rc = Mysql.exec (MatitaDb.instance ()) query in + let rc = HMysql.exec (MatitaDb.instance ()) query in let l = ref [] in - Mysql.iter rc ( + HMysql.iter rc ( fun row -> match row.(0), row.(1) with | Some uri, Some occ when Filename.dirname occ = buri -> l := uri :: !l | _ -> ()); let l = List.sort Pervasives.compare !l in - MatitaMisc.list_uniq l + HExtlib.list_uniq l with exn -> raise exn (* no errors should be accepted *) end - let safe_buri_of_suri suri = try @@ -83,7 +80,7 @@ let safe_buri_of_suri 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 + HExtlib.list_uniq (List.fast_sort Pervasives.compare (List.map safe_buri_of_suri uri_to_remove)) in @@ -123,30 +120,132 @@ let close_uri_list uri_to_remove = (fun acc u -> one_step_depend u @ acc) [] uri_to_remove in let depend = - MatitaMisc.list_uniq - (List.fast_sort Pervasives.compare depend) + HExtlib.list_uniq (List.fast_sort Pervasives.compare depend) in uri_to_remove, depend +let rec close_using_db uris next = + match next with + | [] -> uris + | l -> let uris, next = close_uri_list l in close_using_db uris next @ uris + +let cleaned_no = ref 0;; + + (** TODO repellent code ... *) +let moo_root_dir = lazy ( + let url = + List.assoc "cic:/matita/" + (List.map + (fun pair -> + match + Str.split (Str.regexp "[ \t\r\n]+") (HExtlib.trim_blanks pair) + with + | [a;b] -> a, b + | _ -> assert false) + (Helm_registry.get_list Helm_registry.string "getter.prefix")) + in + String.sub url 7 (String.length url - 7) (* remove heading "file:///" *) +) + +let close_using_moos buris = + let rev_deps = Hashtbl.create 97 in + let all_moos = + HExtlib.find ~test:(fun name -> Filename.check_suffix name ".moo") + (Lazy.force moo_root_dir) + in + List.iter + (fun path -> + let _, metadata = MatitaMoo.load_moo ~fname:path in + let baseuri_of_current_moo = + let rec aux = function + | [] -> assert false + | GrafiteAst.Baseuri buri::_ -> buri + | _ :: tl -> aux tl + in + aux metadata + in + let deps = + HExtlib.filter_map + (function + | GrafiteAst.Dependency buri -> Some buri + | _ -> None ) + metadata + in + List.iter + (fun buri -> Hashtbl.add rev_deps buri baseuri_of_current_moo) deps) + all_moos; + let buris_to_remove = + HExtlib.list_uniq + (List.fast_sort Pervasives.compare + (List.flatten (List.map (Hashtbl.find_all rev_deps) buris))) + in + let objects_to_remove = + let objs_of_buri buri = + HExtlib.filter_map + (function + | Http_getter_types.Ls_object o -> + Some (buri ^ "/" ^ o.Http_getter_types.uri) + | _ -> None) + (Http_getter.ls buri) + in + List.flatten (List.map objs_of_buri (buris @ buris_to_remove)) + in + objects_to_remove + +let clean_baseuris ?(verbose=true) buris = + Hashtbl.clear cache_of_processed_baseuri; + let buris = List.map HGM.strip_trailing_slash buris in + debug_prerr "clean_baseuris called on:"; + if debug then + List.iter debug_prerr buris; + let l = + if Helm_registry.get_bool "db.nodb" then + close_using_moos buris + else + close_using_db [] buris + in + let l = HExtlib.list_uniq (List.fast_sort Pervasives.compare l) in + let l = List.map UriManager.uri_of_string l in + debug_prerr "clean_baseuri will remove:"; + if debug then + List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l; + List.iter + (fun buri -> + MatitaMisc.safe_remove (MatitaMisc.obj_file_of_baseuri buri)) + (HExtlib.list_uniq (List.fast_sort Pervasives.compare + (List.map (UriManager.buri_of_uri) l))); + List.iter (MatitaSync.remove ~verbose) l; + cleaned_no := !cleaned_no + List.length l; + if !cleaned_no > 30 then + begin + cleaned_no := 0; + List.iter + (function table -> + ignore (HMysql.exec (MatitaDb.instance ()) ("OPTIMIZE TABLE " ^ table))) + [MetadataTypes.name_tbl (); MetadataTypes.rel_tbl (); + MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl(); + MetadataTypes.count_tbl()] + end + let baseuri_of_file file = let uri = ref None in let ic = open_in file in - let istream = Stream.of_channel ic in + let istream = Ulexing.from_utf8_channel ic in (try while true do try let stm = GrafiteParser.parse_statement istream in - match baseuri_of_baseuri_decl stm with + match MatitaMisc.baseuri_of_baseuri_decl stm with | Some buri -> let u = MatitaMisc.strip_trailing_slash buri in if String.length u < 5 || String.sub u 0 5 <> "cic:/" then MatitaLog.error (file ^ " sets an incorrect baseuri: " ^ buri); (try - ignore(HG.resolve u) + ignore(Http_getter.resolve u) with - | HGT.Unresolvable_URI _ -> + | Http_getter_types.Unresolvable_URI _ -> MatitaLog.error (file ^ " sets an unresolvable baseuri: "^buri) - | HGT.Key_not_found _ -> ()); + | Http_getter_types.Key_not_found _ -> ()); uri := Some u; raise End_of_file | None -> () @@ -161,34 +260,8 @@ let baseuri_of_file file = | Some uri -> uri | None -> failwith ("No baseuri defined in " ^ file) -let rec fix uris next = - match next with - | [] -> uris - | l -> let uris, next = close_uri_list l in fix uris next @ uris - -let cleaned_no = ref 0;; - -let clean_baseuris ?(verbose=true) buris = - Hashtbl.clear cache_of_processed_baseuri; - let buris = List.map HGM.strip_trailing_slash buris in - debug_prerr "clean_baseuris called on:"; - if debug then - List.iter debug_prerr 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 - debug_prerr "clean_baseuri will remove:"; - if debug then - List.iter (fun u -> debug_prerr (UriManager.string_of_uri u)) l; - List.iter (MatitaSync.remove ~verbose) l; - cleaned_no := !cleaned_no + List.length l; - if !cleaned_no > 30 then - List.iter - (function table -> - ignore (Mysql.exec (MatitaDb.instance ()) ("OPTIMIZE TABLE " ^ table))) - [MetadataTypes.name_tbl (); MetadataTypes.rel_tbl (); - MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl(); - MetadataTypes.count_tbl()] - -let is_empty buri = HG.ls (HGM.strip_trailing_slash buri ^ "/") = [] +let obj_file_of_script f = + if f = "coq.ma" then BuildTimeConf.coq_notation_script else + let baseuri = baseuri_of_file f in + MatitaMisc.obj_file_of_baseuri baseuri