X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitacleanLib.ml;h=82fac08af78a1a7516719a9ab78733be4e1e8e5d;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=06c6835ca5797b32b09a38e68c06cc55d88bb526;hpb=b11d278a26840884692cdfb89e168081134d293f;p=helm.git diff --git a/helm/matita/matitacleanLib.ml b/helm/matita/matitacleanLib.ml index 06c6835ca..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 @@ -30,14 +32,7 @@ module HGT = Http_getter_types;; module HG = Http_getter;; module HGM = Http_getter_misc;; module UM = UriManager;; -module TA = TacticAst;; - -let baseuri_of_baseuri_decl st = - let module TA = TacticAst in - match st with - | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", buri))) -> - Some buri - | _ -> None +module TA = GrafiteAst;; let cache_of_processed_baseuri = Hashtbl.create 1024 @@ -54,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 @@ -84,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 @@ -124,52 +120,148 @@ 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 baseuri_of_file file = - let ic = open_in file in - let stms = CicTextualParser2.parse_statements (Stream.of_channel ic) in - close_in ic; - let uri = ref "" in - List.iter - (fun stm -> - match 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) - with - | HGT.Unresolvable_URI _ -> - MatitaLog.error (file ^ " sets an unresolvable baseuri: "^buri) - | HGT.Key_not_found _ -> ()); - uri := u - | None -> ()) - stms; - !uri - -let rec fix uris next = +let rec close_using_db uris next = match next with | [] -> uris - | l -> let uris, next = close_uri_list l in fix uris next @ 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 = fix [] buris in - let l = MatitaMisc.list_uniq (List.fast_sort Pervasives.compare l) in + 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 (MatitaSync.remove ~verbose) l - -let is_empty buri = HG.ls (HGM.strip_trailing_slash buri ^ "/") = [] + 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 = Ulexing.from_utf8_channel ic in + (try + while true do + try + let stm = GrafiteParser.parse_statement istream in + 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(Http_getter.resolve u) + with + | Http_getter_types.Unresolvable_URI _ -> + MatitaLog.error (file ^ " sets an unresolvable baseuri: "^buri) + | Http_getter_types.Key_not_found _ -> ()); + uri := Some u; + raise End_of_file + | None -> () + with + CicNotationParser.Parse_error _ as exn -> + prerr_endline ("Unable to parse: " ^ file); + prerr_endline (MatitaExcPp.to_string exn); + () + done + with End_of_file -> close_in ic); + match !uri with + | Some uri -> uri + | None -> failwith ("No baseuri defined in " ^ file) + +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