X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitacleanLib.ml;h=82fac08af78a1a7516719a9ab78733be4e1e8e5d;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=992443a357681615771315cac4710c87aadd067b;hpb=ee3f2aa5b78aa77555e5e81d5a2d92501889649e;p=helm.git diff --git a/helm/matita/matitacleanLib.ml b/helm/matita/matitacleanLib.ml index 992443a35..82fac08af 100644 --- a/helm/matita/matitacleanLib.ml +++ b/helm/matita/matitacleanLib.ml @@ -1,7 +1,38 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +open Printf + +let debug = false +let debug_prerr = if debug then prerr_endline else ignore + module HGT = Http_getter_types;; module HG = Http_getter;; +module HGM = Http_getter_misc;; module UM = UriManager;; -module TA = TacticAst;; +module TA = GrafiteAst;; let cache_of_processed_baseuri = Hashtbl.create 1024 @@ -18,21 +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 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 (fun a -> match a.(0) with None ->()|Some a -> l:=a:: !l); + 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 @@ -43,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 @@ -57,21 +94,25 @@ let close_uri_list uri_to_remove = in (* 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 -> buri ^ "/" ^ e.HGT.uri - | _ -> assert false) - inhabitants - in - inhabitants @ acc) - [] buri_to_remove + try + 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 -> buri ^ "/" ^ e.HGT.uri + | _ -> assert false) + inhabitants + in + inhabitants @ acc) + [] buri_to_remove + with HGT.Invalid_URI u -> + MatitaLog.error ("We were listing an invalid buri: " ^ u); + exit 1 in (* now we want the list of all uri that depend on them *) let depend = @@ -79,32 +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 - (function - | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", buri))) -> - uri := MatitaMisc.strip_trailing_slash buri - | _ -> ()) - 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 clean_baseuris buris = - let l = fix [] buris in - let l = MatitaMisc.list_uniq (List.fast_sort Pervasives.compare l) in +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 - List.iter MatitaSync.remove l - + 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 = 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 +