let buri = HMysql.escape buri in
let obj_tbl = MetadataTypes.obj_tbl () in
sprintf
- "SELECT source, h_occurrence FROM %s WHERE h_occurrence LIKE '%s%%'"
+ ("SELECT source, h_occurrence FROM %s WHERE " ^^
+ "h_occurrence REGEXP '^%s[^/]*$'")
obj_tbl buri
in
try
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 =
+ 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 _ ->
+ List.iter
+ (fun buri ->
MatitaMisc.safe_remove (MatitaMisc.obj_file_of_baseuri buri))
- cache_of_processed_baseuri;
+ (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
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
+