X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitacleanLib.ml;h=82fac08af78a1a7516719a9ab78733be4e1e8e5d;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=a263a526fd7e05a65855b3413a8eecef3818b630;hpb=ed7711935c7377ea8785a9f3b85984785b92030e;p=helm.git diff --git a/helm/matita/matitacleanLib.ml b/helm/matita/matitacleanLib.ml index a263a526f..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 @@ -49,8 +51,10 @@ let one_step_depend suri = let buri = 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 = HMysql.exec (MatitaDb.instance ()) query in @@ -62,11 +66,10 @@ let one_step_depend suri = 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 @@ -77,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 @@ -117,34 +120,100 @@ 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 uris next = +let rec close_using_db uris next = match next with | [] -> uris - | l -> let uris, next = close_uri_list l in close 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 = close [] 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; - Hashtbl.iter - (fun buri _ -> - MatitaMisc.safe_remove (MatitaMisc.obj_file_of_baseuri buri) - ) cache_of_processed_baseuri; + 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 @@ -157,3 +226,42 @@ let clean_baseuris ?(verbose=true) buris = 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 +