extractor: extractor.ml
$(H)echo " OCAMLC $<"
$(H)$(OCAMLFIND) ocamlc \
- -thread -package mysql,helm-metadata -linkpkg -o $@ $<
+ -thread -package mysql,helm-metadata,helm-library -linkpkg -o $@ $<
extractor.opt: extractor.ml
$(H)echo " OCAMLOPT $<"
$(H)$(OCAMLFIND) ocamlopt \
- -thread -package mysql,helm-metadata -linkpkg -o $@ $<
+ -thread -package mysql,helm-metadata,helm-library -linkpkg -o $@ $<
extractor_manager: extractor_manager.ml
$(H)echo " OCAMLC $<"
$(H)$(OCAMLFIND) ocamlc \
- -thread -package mysql,helm-metadata -linkpkg -o $@ $<
+ -thread -package mysql,helm-metadata,helm-library -linkpkg -o $@ $<
extractor_manager.opt: extractor_manager.ml
$(H)echo " OCAMLOPT $<"
$(H)$(OCAMLFIND) ocamlopt \
- -thread -package mysql,helm-metadata -linkpkg -o $@ $<
+ -thread -package mysql,helm-metadata,helm-library -linkpkg -o $@ $<
export: extractor.opt extractor_manager.opt
nice -n 20 \
<key name="dir">.tmp/</key>
</section>
<section name="db">
- <key name="host">localhost</key>
- <key name="user">helm</key>
- <key name="database">mowgli</key>
+ <key name="metadata">mysql://mowgli.cs.unibo.it mowgli helm helm library</key>
+ <key name="metadata">file:///tmp/ user.db helm helm user</key>
</section>
<section name="getter">
<key name="servers">
let main () =
print_endline (Printf.sprintf "%d alive on path:%s owner:%s"
(Unix.getpid()) path owner);
+ Helm_registry.load_from "extractor.conf.xml";
Helm_registry.set "tmp.dir" path;
Http_getter.init ();
- let dbd =
- HSql.quick_connect
- ~host:(Helm_registry.get "db.host")
- ~user:(Helm_registry.get "db.user")
- ~database:(Helm_registry.get "db.database") ()
- in
+ let dbspec = LibraryDb.parse_dbd_conf () in
+ let dbd = HSql.quick_connect dbspec in
MetadataTypes.ownerize_tables owner;
let uris =
let ic = open_in (path ^ "/todo") in
(name_tbl,`ObjectName) ; (count_tbl,`Count) ]
in
let statements =
- (SqlStatements.create_tables tbls) @ (SqlStatements.create_indexes tbls)
+ (SqlStatements.create_tables tbls) @
+ (SqlStatements.create_indexes tbls)
in
List.iter (fun statement ->
try
- ignore (Mysql.exec dbd statement)
+ ignore (HSql.exec HSql.Library dbd statement)
with
- exn ->
- let status = Mysql.status dbd in
- match status with
- | Mysql.StatusError Mysql.Table_exists_error -> ()
- | Mysql.StatusError _ -> raise exn
- | _ -> ()
+ HSql.Error _ as exn ->
+ match HSql.errno HSql.Library dbd with
+ | HSql.Table_exists_error -> ()
+ | HSql.OK -> ()
+ | _ -> raise exn
) statements
let drop_all dbd =
(name_tbl,`ObjectName) ; (count_tbl,`Count) ]
in
let statements =
- (SqlStatements.drop_tables tbls) @ (SqlStatements.drop_indexes tbls)
+ (SqlStatements.drop_tables tbls) @
+ (SqlStatements.drop_indexes tbls HSql.Library dbd)
in
List.iter (fun statement ->
try
- ignore (Mysql.exec dbd statement)
- with Mysql.Error _ as exn ->
- match Mysql.errno dbd with
- | Mysql.Bad_table_error
- | Mysql.No_such_index | Mysql.No_such_table -> ()
+ ignore (HSql.exec HSql.Library dbd statement)
+ with HSql.Error _ as exn ->
+ match HSql.errno HSql.Library dbd with
+ | HSql.Bad_table_error
+ | HSql.No_such_index | HSql.No_such_table -> ()
| _ -> raise exn
) statements
ignore(Unix.system ("mkdir -p " ^ fmt));
ignore(Unix.system ("cp -r " ^ base ^ " " ^ fmt ^ "/../"));
done;
- let dbd =
- Mysql.quick_connect
- ~host:(Helm_registry.get "db.host")
- ~user:(Helm_registry.get "db.user")
- ~database:(Helm_registry.get "db.database") ()
- in
+ let dbspec = LibraryDb.parse_dbd_conf () in
+ let dbd = HSql.quick_connect dbspec in
MetadataTypes.ownerize_tables owner;
let uri_RE = Str.regexp ".*\\(ind\\|var\\|con\\)$" in
drop_all dbd;
(rel_tbl_c,`RefRel);
(name_tbl_c,`ObjectName);
(count_tbl_c,`Count);
- (hits_tbl,`Hits) ] @
+ (hits_tbl,`Hits) ] HSql.Library dbd @
SqlStatements.rename_tables [
(obj_tbl,obj_tbl_b);
(sort_tbl,sort_tbl_b);
in
List.iter (fun statement ->
try
-(* prerr_endline statement;*)
- ignore (Mysql.exec dbd statement)
- with exn ->
- let status = Mysql.status dbd in
- match status with
- | Mysql.StatusError Mysql.Table_exists_error
- | Mysql.StatusError Mysql.Bad_table_error
- | Mysql.StatusError Mysql.Cant_drop_field_or_key
- | Mysql.StatusError Mysql.Unknown_table -> ()
- | Mysql.StatusError status ->
-(* prerr_endline (string_of_int (Obj.magic status));*)
- prerr_endline (Printexc.to_string exn);
- raise exn
+ ignore (HSql.exec HSql.Library dbd statement)
+ with HSql.Error _ as exn ->
+ match HSql.errno HSql.Library dbd with
+ | HSql.Table_exists_error
+ | HSql.Bad_table_error -> ()
| _ ->
prerr_endline (Printexc.to_string exn);
- ())
+ raise exn)
stats
;;
begin
let tab,idx,fill =
if am_i_destructor () then
- (SqlStatements.drop_tables,SqlStatements.drop_indexes,
+ (SqlStatements.drop_tables,
+ (fun x ->
+ let dbd = HSql.fake_db_for_mysql HSql.Library in
+ SqlStatements.drop_indexes x HSql.Library dbd),
fun _ t -> [sprintf "DELETE * FROM %s;" t])
else
- (SqlStatements.create_tables,SqlStatements.create_indexes,
+ (SqlStatements.create_tables,
+ SqlStatements.create_indexes,
SqlStatements.fill_hits)
in
let from = 2 in
cicParser.cmi: cic.cmo
cicUtil.cmi: cic.cmo
helmLibraryObjects.cmi: cic.cmo
+libraryObjects.cmi: cic.cmo
discrimination_tree.cmi: cic.cmo
path_indexing.cmi: cic.cmo
cicInspect.cmi: cic.cmo
cicUtil.cmx: cicUniv.cmx cic.cmx cicUtil.cmi
helmLibraryObjects.cmo: cic.cmo helmLibraryObjects.cmi
helmLibraryObjects.cmx: cic.cmx helmLibraryObjects.cmi
-libraryObjects.cmo: libraryObjects.cmi
-libraryObjects.cmx: libraryObjects.cmi
+libraryObjects.cmo: cic.cmo libraryObjects.cmi
+libraryObjects.cmx: cic.cmx libraryObjects.cmi
discrimination_tree.cmo: cicUtil.cmi cic.cmo discrimination_tree.cmi
discrimination_tree.cmx: cicUtil.cmx cic.cmx discrimination_tree.cmi
path_indexing.cmo: cic.cmo path_indexing.cmi
| C.Implicit a, C.Implicit a' -> a = a'
we insert an unused variable below to genarate a warning at compile time
*)
- | _,_ -> let fix_alpha_equivalence_please = 0 in false (* we already know that t != t' *)
+ | _,_ -> false (* we already know that t != t' *)
and aux_exp_named_subst exp_named_subst1 exp_named_subst2 =
try
List.fold_left2
match UriManager.bodyuri_of_uri uri with
None -> None
| Some bodyuri ->
- if Http_getter.exists' bodyuri then
+ if Http_getter.exists' ~local:false bodyuri then
Some (Http_getter.getxml' bodyuri)
else
None
let add_type_checked_obj uri (obj,ugraph,univlist) =
Cache.add_cooked ~key:uri (obj,ugraph,univlist)
-let in_library uri = in_cache uri || Http_getter.exists' uri
+let in_library uri = in_cache uri || Http_getter.exists' ~local:false uri
let remove_obj = Cache.remove
| Exception e -> raise e
| Resolved url -> url
-let deref_index_theory uri =
- if Http_getter_storage.exists (uri ^ xml_suffix) then uri
- else if is_theory_uri uri && Filename.basename uri = "index.theory" then
+let deref_index_theory ~local uri =
+(* if Http_getter_storage.exists ~local (uri ^ xml_suffix) then uri *)
+ if is_theory_uri uri && Filename.basename uri = "index.theory" then
strip_trailing_slash (Filename.dirname uri) ^ theory_suffix
else
uri
let help () = Http_getter_const.usage_string (Http_getter_env.env_to_string ())
-let exists uri =
+let exists ~local uri =
(* prerr_endline ("Http_getter.exists " ^ uri); *)
if remote () then
exists_remote uri
else
- let uri = deref_index_theory uri in
- Http_getter_storage.exists (uri ^ xml_suffix)
+ let uri = deref_index_theory ~local uri in
+ Http_getter_storage.exists ~local (uri ^ xml_suffix)
let is_an_obj s =
try
s <> UriManager.buri_of_uri (UriManager.uri_of_string s)
with UriManager.IllFormedUri _ -> true
-let resolve ~writable uri =
+let resolve ~local ~writable uri =
if remote () then
resolve_remote ~writable uri
else
- let uri = deref_index_theory uri in
+ let uri = deref_index_theory ~local uri in
try
if is_an_obj uri then
- Http_getter_storage.resolve ~writable (uri ^ xml_suffix)
+ Http_getter_storage.resolve ~writable ~local (uri ^ xml_suffix)
else
- Http_getter_storage.resolve ~writable uri
+ Http_getter_storage.resolve ~writable ~local uri
with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri)
-let filename ~writable uri =
+let filename ~local ~writable uri =
if remote () then
raise (Key_not_found uri)
else
- let uri = deref_index_theory uri in
+ let uri = deref_index_theory ~local uri in
try
Http_getter_storage.resolve
- ~must_exists:false ~writable uri
+ ~must_exists:false ~writable ~local uri
with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri)
let getxml uri =
if remote () then getxml_remote uri
else begin
- let uri' = deref_index_theory uri in
+ let uri' = deref_index_theory ~local:false uri in
(try
- Http_getter_storage.filename (uri' ^ xml_suffix)
+ Http_getter_storage.filename ~local:false (uri' ^ xml_suffix)
with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri))
end
let getxslt uri =
if remote () then getxslt_remote uri
- else Http_getter_storage.filename ~find:true ("xslt:/" ^ uri)
+ else Http_getter_storage.filename ~local:false ~find:true ("xslt:/" ^ uri)
let getdtd uri =
if remote () then
let contains_object = (<>) []
(** non regexp-aware version of ls *)
-let rec dumb_ls uri_prefix =
+let rec dumb_ls ~local uri_prefix =
(* prerr_endline ("Http_getter.dumb_ls " ^ uri_prefix); *)
if is_cic_obj_uri uri_prefix then begin
let dirs = ref StringSet.empty in
try
store_obj objs (strip_suffix ~suffix:xml_suffix fname)
with Invalid_argument _ -> ())
- (Http_getter_storage.ls uri_prefix);
+ (Http_getter_storage.ls ~local uri_prefix);
collect_ls_items !dirs objs
end else if is_theory_uri uri_prefix then begin
let items = ref [] in
let fname = strip_suffix ~suffix:xml_suffix fname in
let theory_name = strip_suffix ~suffix:theory_suffix fname in
let sub_theory = normalize_dir cic_uri_prefix ^ theory_name ^ "/" in
- if is_empty_theory sub_theory then add_theory fname
+ if is_empty_theory ~local sub_theory then add_theory fname
with Invalid_argument _ -> ())
- (Http_getter_storage.ls uri_prefix);
+ (Http_getter_storage.ls ~local uri_prefix);
(try
- if contains_object (dumb_ls cic_uri_prefix)
- && exists (strip_trailing_slash uri_prefix ^ theory_suffix)
+ if contains_object (dumb_ls ~local cic_uri_prefix)
+ && exists ~local:false (strip_trailing_slash uri_prefix ^ theory_suffix)
then
add_theory "index.theory";
with Unresolvable_URI _ -> ());
end else
raise (Invalid_URI uri_prefix)
-and is_empty_theory uri_prefix =
+and is_empty_theory ~local uri_prefix =
(* prerr_endline ("is_empty_theory " ^ uri_prefix); *)
- not (contains_object (dumb_ls uri_prefix))
+ not (contains_object (dumb_ls ~local uri_prefix))
(* handle simple regular expressions of the form "...(..|..|..)..." on cic
* uris, not meant to be a real implementation of regexp. The only we use is
in
aux [] [] (List.concat results)
-let ls regexp =
+let ls ~local regexp =
if remote () then
ls_remote regexp
else
let prefixes = explode_ls_regexp regexp in
- merge_results (List.map dumb_ls prefixes)
+ merge_results (List.map (dumb_ls ~local) prefixes)
let getalluris () =
let rec aux acc = function
| Ls_object obj -> (dir ^ obj.uri) :: acc, subdirs
| Ls_section sect -> acc, (dir ^ sect ^ "/") :: subdirs)
(acc, todo)
- (dumb_ls dir)
+ (dumb_ls ~local:false dir)
in
aux acc' todo'
in
(* Shorthands from now on *)
let getxml' uri = getxml (UriManager.string_of_uri uri)
-let resolve' ~writable uri = resolve ~writable (UriManager.string_of_uri uri)
-let exists' uri = exists (UriManager.string_of_uri uri)
-let filename' ~writable uri = filename ~writable (UriManager.string_of_uri uri)
+let resolve' ~local ~writable uri =
+ resolve ~local ~writable (UriManager.string_of_uri uri)
+;;
+let exists' ~local uri = exists ~local (UriManager.string_of_uri uri)
+let filename' ~local ~writable uri =
+ filename ~local ~writable (UriManager.string_of_uri uri)
+;;
let tilde_expand_key k =
try
(** @raise Http_getter_types.Unresolvable_URI _
* @raise Http_getter_types.Key_not_found _ *)
-val resolve: writable:bool -> string -> string (* uri -> url *)
+val resolve: local:bool -> writable:bool -> string -> string (* uri -> url *)
(** as resolve, but does not check if the resource exists
* @raise Http_getter_types.Key_not_found *)
-val filename: writable:bool -> string -> string (* uri -> url *)
+val filename: local:bool -> writable:bool -> string -> string (* uri -> url *)
-val exists: string -> bool
+val exists: local:bool -> string -> bool
val getxml : string -> string
val getxslt : string -> string
(** @param baseuri uri to be listed, simple form or regular expressions (a
* single choice among parens) are permitted *)
-val ls: string -> ls_item list
+val ls: local:bool -> string -> ls_item list
(** {2 UriManager shorthands} *)
val getxml' : UriManager.uri -> string
-val resolve' : writable:bool -> UriManager.uri -> string
-val exists' : UriManager.uri -> bool
-val filename' : writable:bool -> UriManager.uri -> string
+val resolve' : local:bool -> writable:bool -> UriManager.uri -> string
+val exists' : local:bool -> UriManager.uri -> bool
+val filename' : local:bool -> writable:bool -> UriManager.uri -> string
(** {2 Misc} *)
let prefix_map () = !prefix_map_ref
+let keep_first l =
+ let cmp (_,x) (_,y) = x = y in
+ let rec aux prev = function
+ | [] -> []
+ | hd::tl -> if cmp prev hd then hd :: aux prev tl else []
+ in
+ match l with
+ | hd :: tl -> hd :: aux hd tl
+ | _ -> assert false
+;;
+
(** given an uri returns the prefixes for it *)
let lookup uri =
let matches =
- List.filter (fun (rex, _, l, _) -> Pcre.pmatch ~rex uri)
- (Lazy.force (prefix_map ())) in
+ HExtlib.filter_map
+ (fun (rex, _, l, _ as entry) ->
+ try
+ let got = Pcre.extract ~full_match:true ~rex uri in
+ Some (entry, String.length got.(0))
+ with Not_found -> None)
+ (Lazy.force (prefix_map ()))
+ in
if matches = [] then raise (Unresolvable_URI uri);
- matches
+ List.map fst (keep_first (List.sort (fun (_,l1) (_,l2) -> l2 - l1) matches))
+;;
let get_attrs uri = List.map (fun (_, _, _, attrs) -> attrs) (lookup uri)
(*************************** ACTIONS ******************************************)
-let exists_http _ url =
+let exists_http ~local _ url =
+ if local then false else
Http_getter_wget.exists (url ^ gz_suffix) || Http_getter_wget.exists url
let exists_file _ fname =
Sys.file_exists (fname ^ gz_suffix) || Sys.file_exists fname
-let resolve_http ~must_exists _ url =
+let resolve_http ~must_exists ~local _ url =
+ if local then raise Not_found' else
try
if must_exists then
List.find Http_getter_wget.exists [ url ^ gz_suffix; url ]
remove_duplicates !entries
with Unix.Unix_error (_, "opendir", _) -> []
-let ls_http_single _ url_prefix =
+let ls_http_single ~local _ url_prefix =
+ if local then raise (Resource_not_found ("get","")) else
+ let url = normalize_dir url_prefix ^ index_fname in
try
- let index = Http_getter_wget.get (normalize_dir url_prefix ^ index_fname) in
+ let index = Http_getter_wget.get url in
Pcre.split ~rex:newline_RE index
- with Http_client_error _ -> raise Not_found'
+ with Http_client_error _ -> raise (Resource_not_found ("get",url))
+;;
let get_file _ path =
if Sys.file_exists (path ^ gz_suffix) then
else
raise Not_found'
-let get_http uri url =
+let get_http ~local uri url =
+ if local then raise Not_found' else
let scheme, path =
match Pcre.split ~rex:cic_scheme_sep_RE uri with
| [scheme; path] -> scheme, path
(**************************** RESOLUTION OF PREFIXES ************************)
-let resolve_prefixes write exists uri =
+let resolve_prefixes n local write exists uri =
let exists_test new_uri =
if is_file_schema new_uri then
exists_file () (path_of_file_url new_uri)
else if is_http_schema new_uri then
- exists_http () new_uri
+ exists_http ~local () new_uri
else false
in
- let rec aux = function
- | (rex, _, url_prefix, attrs) :: tl ->
+ let rec aux n = function
+ | (rex, _, url_prefix, attrs) :: tl when n > 0->
(match write, is_readwrite attrs, exists with
- | true ,false, _ -> aux tl
+ | true ,false, _ -> aux n tl
| true ,true ,true
| false,_ ,true ->
let new_uri = (Pcre.replace_first ~rex ~templ:url_prefix uri) in
- if exists_test new_uri then new_uri::aux tl else aux tl
+ if exists_test new_uri then new_uri::aux (n-1) tl else aux n tl
| true ,true ,false
| false,_ ,false ->
- (Pcre.replace_first ~rex ~templ:url_prefix uri) :: (aux tl))
- | [] -> []
+ (Pcre.replace_first ~rex ~templ:url_prefix uri) :: (aux (n-1) tl))
+ | _ -> []
in
- aux (lookup uri)
+ aux n (lookup uri)
-let resolve_prefix w e u =
- match resolve_prefixes w e u with
+let resolve_prefix l w e u =
+ match resolve_prefixes 1 l w e u with
| hd :: _ -> hd
| [] ->
raise
name: string;
write: bool;
exists: bool;
+ local: bool;
file: string -> string -> 'a; (* unresolved uri, resolved uri *)
http: string -> string -> 'a; (* unresolved uri, resolved uri *)
}
let dispatch_single storage_method uri =
assert (extension uri <> gz_suffix);
let uri = normalize_root uri in
- let url = resolve_prefix storage_method.write storage_method.exists uri in
+ let url =
+ resolve_prefix
+ storage_method.local storage_method.write storage_method.exists uri
+ in
invoke_method storage_method uri url
let dispatch_multi storage_method uri =
- let urls = resolve_prefixes storage_method.write storage_method.exists uri in
+ let urls =
+ resolve_prefixes max_int
+ storage_method.local storage_method.write storage_method.exists uri
+ in
let rec aux = function
| [] -> raise (Resource_not_found (storage_method.name, uri))
| url :: tl ->
aux urls
let dispatch_all storage_method uri =
- let urls = resolve_prefixes storage_method.write storage_method.exists uri in
+ let urls =
+ resolve_prefixes max_int
+ storage_method.local storage_method.write storage_method.exists uri
+ in
List.map (fun url -> invoke_method storage_method uri url) urls
(******************************** EXPORTED FUNCTIONS *************************)
-let exists s =
+let exists ~local s =
try
dispatch_single
{ write = false;
name = "exists";
exists = true;
- file = exists_file; http = exists_http; } s
+ local=local;
+ file = exists_file; http = exists_http ~local; } s
with Resource_not_found _ -> false
-let resolve ?(must_exists=true) ~writable =
+let resolve ~local ?(must_exists=true) ~writable =
(if must_exists then
dispatch_multi
else
{ write = writable;
name="resolve";
exists = must_exists;
+ local=local;
file = resolve_file ~must_exists;
- http = resolve_http ~must_exists; }
+ http = resolve_http ~local ~must_exists; }
let remove =
dispatch_single
{ write = false;
name = "remove";
exists=true;
+ local=false;
file = remove_file; http = remove_http; }
-let filename ?(find = false) =
+let filename ~local ?(find = false) =
(if find then dispatch_multi else dispatch_single)
{ write = false;
name = "filename";
exists=true;
- file = get_file; http = get_http; }
+ local=local;
+ file = get_file; http = get_http ~local ; }
-let ls uri_prefix =
+let ls ~local uri_prefix =
let ls_all s =
try
dispatch_all
{ write=false;
name = "ls";
exists=true;
- file = ls_file_single; http = ls_http_single; } s
+ local=local;
+ file = ls_file_single; http = ls_http_single ~local; } s
with Resource_not_found _ -> []
in
let direct_results = List.flatten (ls_all uri_prefix) in
None)
(Lazy.force (prefix_map ()))
-let is_legacy uri = List.for_all has_legacy (get_attrs uri)
+let is_legacy uri = List.for_all has_legacy (get_attrs uri)
(* implement this in a fast way! *)
-let is_empty buri =
+let is_empty ~local buri =
let buri = strip_trailing_slash buri ^ "/" in
- let files = ls buri in
+ let files = ls ~local buri in
is_empty_listing files
let is_read_only uri =
let is_empty_dir path =
let files =
- if is_file_schema path then
- ls_file_single () (path_of_file_url path)
- else if is_http_schema path then
- ls_http_single () path
- else
- assert false
+ try
+ if is_file_schema path then
+ ls_file_single () (path_of_file_url path)
+ else if is_http_schema path then
+ ls_http_single ~local:false () path
+ else
+ assert false
+ with Resource_not_found _ -> []
in
is_empty_listing files
in
exception Resource_not_found of string * string (** method, uri *)
(** @return a list of string where dir are returned with a trailing "/" *)
-val ls: string -> string list
+val ls: local:bool -> string -> string list
(** @return the filename of the resource corresponding to a given uri. Handle
* that the search is performed only if the asked resource is not found in
* cache (i.e. to perform the find again you need to clean the cache).
* Defaults to false *)
-val filename: ?find:bool -> string -> string
+val filename: local:bool -> ?find:bool -> string -> string
(** only works for local resources
* if both compressed and non-compressed versions of a resource exist, both of
* them are removed *)
val remove: string -> unit
-val exists: string -> bool
-val resolve: ?must_exists:bool -> writable:bool -> string -> string
+val exists: local:bool -> string -> bool
+val resolve:
+ local:bool -> ?must_exists:bool -> writable:bool -> string -> string
(* val get_attrs: string -> Http_getter_types.prefix_attr list *)
val is_read_only: string -> bool
val is_legacy: string -> bool
-val is_empty: string -> bool
+val is_empty: local:bool -> string -> bool
val clean_cache: unit -> unit
HLog.error (Printf.sprintf "uri %s belongs to a read-only repository" value);
raise (ReadOnlyUri value)
end;
- if (not (Http_getter_storage.is_empty value) ||
+ if (not (Http_getter_storage.is_empty ~local:true value) ||
LibraryClean.db_uris_of_baseuri value <> [])
&& opts.clean_baseuri
then begin
HLog.message ("baseuri " ^ value ^ " is not empty");
HLog.message ("cleaning baseuri " ^ value);
LibraryClean.clean_baseuris [value];
- assert (Http_getter_storage.is_empty value);
+ assert (Http_getter_storage.is_empty ~local:true value);
end;
if not (Helm_registry.get_opt_default Helm_registry.bool "matita.nodisk"
~default:false)
then
HExtlib.mkdir
- (Filename.dirname (Http_getter.filename ~writable:true (value ^
+ (Filename.dirname
+ (Http_getter.filename ~local:true ~writable:true (value ^
"/foo.con")));
end;
GrafiteTypes.set_option status name value,[]
| Cic.CurrentProof (_,metasenv',bo,ty,_, attrs) ->
let name = UriManager.name_of_uri uri in
if not(CicPp.check name ty) then
- HLog.error ("Bad name: " ^ name);
+ HLog.warn ("Bad name: " ^ name);
if opts.do_heavy_checks then
begin
let dbd = LibraryDb.instance () in
-hSql.cmo: hSql.cmi
-hSql.cmx: hSql.cmi
+hSql.cmo: hSqlite3.cmo hMysql.cmo hSql.cmi
+hSql.cmx: hSqlite3.cmx hMysql.cmx hSql.cmi
INTERFACE_FILES = \
hSql.mli
IMPLEMENTATION_FILES = \
+ hSqlite3.ml \
+ hMysql.ml \
$(INTERFACE_FILES:%.mli=%.ml)
EXTRA_OBJECTS_TO_INSTALL =
EXTRA_OBJECTS_TO_CLEAN =
let profiler = HExtlib.profile "mysql"
-let use_real_db () =
- not (Helm_registry.get_opt_default Helm_registry.bool
- ~default:false "db.nodb")
-
let quick_connect ?host ?database ?port ?password ?user () =
profiler.HExtlib.profile
- (fun () ->
- if use_real_db () then
- (Some (Mysql.quick_connect ?host ?database ?port ?password ?user ()))
- else
- None)
+ (fun () ->
+ Some (Mysql.quick_connect ?host ?database ?port ?password ?user ()))
()
+;;
let disconnect = function
| None -> ()
let escape s =
profiler.HExtlib.profile Mysql.escape s
-let exec dbd s =
+let exec s dbd =
match dbd with
| None -> None
| Some dbd ->
+++ /dev/null
-hMysql.ml
\ No newline at end of file
--- /dev/null
+(* 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://cs.unibo.it/helm/.
+ *)
+
+type error_code =
+ | OK
+ | Table_exists_error
+ | Dup_keyname
+ | No_such_table
+ | No_such_index
+ | Bad_table_error
+ | GENERIC_ERROR of string
+
+exception Error of string
+
+(* the exceptions raised are from the Mysql module *)
+
+type dbtype = User | Library | Legacy
+type dbimplementation = Mysql of HMysql.dbd | Sqlite of HSqlite3.dbd | FakeMySql
+type result = Mysql_rc of HMysql.result | Sqlite_rc of HSqlite3.result | Nothing
+
+ (* host port dbname user password type *)
+type dbspec = (string * int option * string * string * string option * dbtype) list
+type dbd = (dbtype * dbimplementation) list
+
+let debug = false;;
+let debug_print s = if debug then prerr_endline (Lazy.force s) else ();;
+
+let pp_dbtype = function
+ | User -> "User"
+ | Library -> "Library"
+ | Legacy -> "Legacy"
+;;
+
+let mk_dbspec l = l;;
+
+let quick_connect dbspec =
+ HExtlib.filter_map
+ (fun (host, port, database, user, password, kind) ->
+ if Pcre.pmatch ~pat:"^file://" host then
+ Some (kind, (Sqlite (HSqlite3.quick_connect (kind = Library)
+ ~host:(Pcre.replace ~pat:"^file://" host)
+ ?port ~user ~database ?password ())))
+ else if Pcre.pmatch ~pat:"^mysql://" host then
+ Some (kind, (Mysql (HMysql.quick_connect
+ ~host:(Pcre.replace ~pat:"^mysql://" host)
+ ?port ~user ~database ?password ())))
+ else
+ None)
+ dbspec
+;;
+
+let mk f1 f2 = function
+ | (Sqlite dbd) -> Sqlite_rc (f1 dbd)
+ | (Mysql dbd) -> Mysql_rc (f2 dbd)
+ | FakeMySql -> assert false
+;;
+
+let mk_u f1 f2 = function
+ | (_, (Sqlite dbd)) -> f1 dbd
+ | (_, (Mysql dbd)) -> f2 dbd
+ | (_, FakeMySql) -> assert false
+;;
+
+let wrap f x =
+ try f x with
+ | HMysql.Error s | HSqlite3.Error s -> raise (Error s)
+ | Not_found -> raise (Error "Not_found")
+;;
+
+let disconnect dbd =
+ wrap (List.iter (mk_u HSqlite3.disconnect HMysql.disconnect)) dbd
+;;
+
+let exec (dbtype : dbtype) (dbd : dbd) (query : string) =
+ try
+ debug_print (lazy ("EXEC: " ^ pp_dbtype dbtype ^ "|" ^ query));
+ let dbd = List.assoc dbtype dbd in
+ wrap (mk (HSqlite3.exec query) (HMysql.exec query)) dbd
+ with Not_found ->
+ if dbtype = Legacy then Nothing else raise (Error "No ro or writable db")
+;;
+
+let map result ~f =
+ match result with
+ | Mysql_rc rc -> HMysql.map rc ~f
+ | Sqlite_rc rc -> HSqlite3.map rc ~f
+ | Nothing -> []
+;;
+
+let iter result ~f =
+ match result with
+ | Mysql_rc rc -> HMysql.iter rc ~f
+ | Sqlite_rc rc -> HSqlite3.iter rc ~f
+ | Nothing -> ()
+;;
+
+let sqlite_err = function
+ | HSqlite3.OK -> OK
+ | HSqlite3.Table_exists_error -> Table_exists_error
+ | HSqlite3.Dup_keyname -> Dup_keyname
+ | HSqlite3.No_such_table -> No_such_table
+ | HSqlite3.No_such_index -> No_such_index
+ | HSqlite3.Bad_table_error -> Bad_table_error
+ | HSqlite3.GENERIC_ERROR s -> GENERIC_ERROR s
+;;
+
+let mysql_err = function
+ | HMysql.OK -> OK
+ | HMysql.Table_exists_error -> Table_exists_error
+ | HMysql.Dup_keyname -> Dup_keyname
+ | HMysql.No_such_table -> No_such_table
+ | HMysql.No_such_index -> No_such_index
+ | HMysql.Bad_table_error -> Bad_table_error
+ | HMysql.GENERIC_ERROR s -> GENERIC_ERROR s
+;;
+
+let errno dbtype dbd =
+ wrap
+ (fun d -> match List.assoc dbtype d with
+ | Mysql dbd -> mysql_err (HMysql.errno dbd)
+ | Sqlite dbd -> sqlite_err (HSqlite3.errno dbd)
+ | FakeMySql -> assert false)
+ dbd
+;;
+
+let escape dbtype dbd s =
+ try
+ match List.assoc dbtype dbd with
+ | Mysql _ | FakeMySql -> wrap HMysql.escape s
+ | Sqlite _ -> wrap HSqlite3.escape s
+ with Not_found ->
+ if dbtype = Legacy then s else raise (Error "No ro or writable db")
+;;
+
+let escape_string_for_like dbtype dbd =
+ try
+ match List.assoc dbtype dbd with
+ | Mysql _ | FakeMySql -> HMysql.escape_string_for_like
+ | Sqlite _ -> HSqlite3.escape_string_for_like
+ with Not_found ->
+ if dbtype = Legacy then ("ESCAPE \"\\\"" : ('a,'b,'c,'a) format4)
+ else raise (Error "No ro or writable db")
+;;
+
+let isMysql dbtype dbd =
+ wrap
+ (fun d -> match List.assoc dbtype d with Mysql _ -> true | _ -> false)
+ dbd
+;;
+
+let fake_db_for_mysql dbtype =
+ [dbtype, FakeMySql]
+;;
* http://cs.unibo.it/helm/.
*)
-(**
- * {2 Proxy module around MySQL conection}
- *
- * The behaviour of this module is influenced by the Helm_registry boolean value
- * of the "db.nodb" key. When set to "false" the module works as expected. When
- * set to "true" all functions perform dummy action: connect and disconnect do
- * nothing; exec, iter, and map work like the empty set of results has been
- * returned; errno and status return Mysql.Connection_error
- *)
-
type dbd
type result
type error_code =
| No_such_index
| Bad_table_error
| GENERIC_ERROR of string
+
exception Error of string
(* the exceptions raised are from the Mysql module *)
-val quick_connect :
- ?host:string ->
- ?database:string ->
- ?port:int -> ?password:string -> ?user:string -> unit -> dbd
+type dbtype = User | Library | Legacy
+
+ (* host port dbname user password type *)
+type dbspec
+
+val mk_dbspec :
+ (string * int option * string * string * string option * dbtype) list ->
+ dbspec
+
+val quick_connect : dbspec -> dbd
val disconnect : dbd -> unit
-val exec: dbd -> string -> result
+val exec: dbtype -> dbd -> string -> result
val map : result -> f:(string option array -> 'a) -> 'a list
val iter : result -> f:(string option array -> unit) -> unit
-val errno : dbd -> error_code
+val errno : dbtype -> dbd -> error_code
(* val status : dbd -> Mysql.status *)
-val escape: string -> string
+val escape: dbtype -> dbd -> string -> string
+
+val escape_string_for_like: dbtype -> dbd -> ('a,'b,'c,'a) format4
+
+val isMysql : dbtype -> dbd -> bool
-val escape_string_for_like: ('a,'b,'c,'a) format4
+(* this dbd can't du queries, used only in table_creator *)
+val fake_db_for_mysql: dbtype -> dbd
-val isMysql : bool
let profiler = HExtlib.profile "Sqlite3"
-let quick_connect ?host ?(database = "sqlite") ?port ?password ?user () =
+let quick_connect
+ is_library
+ ?(host = Helm_registry.get "matita.basedir")
+ ?(database = "sqlite") ?port ?password ?user ()
+=
let username = Helm_registry.get "user.name" in
- let tmp_db_name =
- if HExtlib.is_dir "/dev/shm/" && HExtlib.writable_dir "/dev/shm/" then
- ((*HLog.debug "using /dev/shm to store the working copy of the db";*)
- "/dev/shm/matita.db." ^ username ^ "." ^ string_of_int (Unix.getpid ()))
- else
- ((*HLog.debug "/dev/shm not available";*)
- Helm_registry.get "matita.basedir" ^ "/matita.db." ^ username ^ "." ^
- string_of_int (Unix.getpid ()))
- in
- let db_name = Helm_registry.get "matita.basedir" ^ "/" ^ database ^ ".db" in
- let standard_db_name =
- Helm_registry.get "matita.rt_base_dir" ^ "/metadata.db"
+ let host_mangled = Pcre.replace ~pat:"[/ .]" ~templ:"_" host in
+ let tmp_db_name =
+ "/dev/shm/matita.db." ^ username ^ "." ^ host_mangled ^ "." ^
+ string_of_int (Unix.getpid ())
in
- let cp_to_ram_cmd =
- if HExtlib.is_regular db_name then
- "cp " ^ db_name ^ " " ^ tmp_db_name
+ let db_name = host ^ "/" ^ database in
+ let db_to_open =
+ if HExtlib.is_dir "/dev/shm/" && HExtlib.writable_dir "/dev/shm/"
+ && (not is_library)
+ then
+ (let cp_to_ram_cmd = "cp " ^ db_name ^ " " ^ tmp_db_name in
+ ignore (Sys.command cp_to_ram_cmd);
+ let mv_to_disk_cmd _ =
+ ignore (Sys.command ("mv " ^ tmp_db_name ^ " " ^ db_name))
+ in
+ at_exit mv_to_disk_cmd;
+ tmp_db_name)
else
- (* we start from the standard library *)
- "cp " ^ standard_db_name ^ " " ^ tmp_db_name
- in
- ignore (Sys.command cp_to_ram_cmd);
- let mv_to_disk_cmd _ =
- ignore (Sys.command ("mv " ^ tmp_db_name ^ " " ^ db_name))
+ db_name
in
- at_exit mv_to_disk_cmd;
- let db = Sqlite3.db_open tmp_db_name in
+ let db = Sqlite3.db_open db_to_open in
(* attach the REGEX function *)
- Sqlite3.create_fun_2 db "REGEXP"
+ Sqlite3.create_fun2 db "REGEXP"
(fun s rex ->
match rex, s with
| Sqlite3.Data.TEXT rex, Sqlite3.Data.BLOB s
let pp_rc rc = prerr_endline (string_of_rc rc);;
-let exec db s =
+let exec s db =
prerr_endline s;
let stored_result = ref [] in
let store row =
multi_aliases: DisambiguateTypes.multiple_environment;
lexicon_content_rev: LexiconMarshal.lexicon;
notation_ids: CicNotation.notation_id list; (** in-scope notation ids *)
- metadata: LibraryNoDb.metadata list;
}
let initial_status = {
multi_aliases = DisambiguateTypes.Environment.empty;
lexicon_content_rev = [];
notation_ids = [];
- metadata = [];
}
let add_lexicon_content cmds status =
LexiconAstPp.pp_command content')); *)
{ status with lexicon_content_rev = content' }
-let add_metadata new_metadata status =
- if Helm_registry.get_bool "db.nodb" then
- let metadata = status.metadata in
- let metadata' =
- List.fold_left
- (fun acc m ->
- match m with
- | LibraryNoDb.Dependency buri ->
- if List.exists (LibraryNoDb.eq_metadata m) metadata
- then acc
- else m :: acc)
- metadata new_metadata
- in
- { status with metadata = metadata' }
- else
- status
-
let set_proof_aliases mode status new_aliases =
if mode = LexiconAst.WithoutPreferences then
status
List.map
(fun alias -> LexiconAst.Alias (HExtlib.dummy_floc, alias))
in
- let deps_of_aliases =
- HExtlib.filter_map
- (function
- | LexiconAst.Ident_alias (_, suri) ->
- let buri = UriManager.buri_of_uri (UriManager.uri_of_string suri) in
- Some (LibraryNoDb.Dependency buri)
- | _ -> None)
- in
let aliases =
List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
status.aliases new_aliases in
let status =
add_lexicon_content (commands_of_aliases aliases) new_status
in
- let status = add_metadata (deps_of_aliases aliases) status in
status
in
let lexicon = LexiconMarshal.load_lexicon lexiconpath in
let status = List.fold_left (eval_command ~mode) status lexicon in
- if Helm_registry.get_bool "db.nodb" then
- let metadatapath_rw, metadatapath_r =
- LibraryMisc.metadata_file_of_baseuri
- ~must_exist:false ~baseuri ~writable:true,
- LibraryMisc.metadata_file_of_baseuri
- ~must_exist:false ~baseuri ~writable:false
- in
- let metadatapath =
- if Sys.file_exists metadatapath_rw then metadatapath_rw else
- if Sys.file_exists metadatapath_r then metadatapath_r else
- raise (MetadataNotFound metadatapath_rw)
- in
- add_metadata (LibraryNoDb.load_metadata ~fname:metadatapath) status
- else
- status
+ status
| LexiconAst.Alias (loc, spec) ->
let diff =
(*CSC: Warning: this code should be factorized with the corresponding
set_proof_aliases mode status diff
| LexiconAst.Interpretation (_, dsc, (symbol, _), cic_appl_pattern) as stm ->
let status = add_lexicon_content [stm] status in
- let uris =
- List.map
- (fun uri -> LibraryNoDb.Dependency (UriManager.buri_of_uri uri))
- (CicNotationUtil.find_appl_pattern_uris cic_appl_pattern)
- in
let diff =
[DisambiguateTypes.Symbol (symbol, 0),
DisambiguateChoices.lookup_symbol_by_dsc symbol dsc]
in
let status = set_proof_aliases mode status diff in
- let status = add_metadata uris status in
status
| LexiconAst.Notation _ as stm -> add_lexicon_content [stm] status
multi_aliases: DisambiguateTypes.multiple_environment;
lexicon_content_rev: LexiconMarshal.lexicon;
notation_ids: CicNotation.notation_id list; (** in-scope notation ids *)
- metadata: LibraryNoDb.metadata list;
}
val initial_status: status
-cicCoercion.cmi: refinementTool.cmo coercDb.cmi
+cicCoercion.cmi: coercDb.cmi
librarySync.cmi: refinementTool.cmo
cicElim.cmo: cicElim.cmi
cicElim.cmx: cicElim.cmi
libraryDb.cmx: libraryDb.cmi
coercDb.cmo: coercDb.cmi
coercDb.cmx: coercDb.cmi
-cicCoercion.cmo: refinementTool.cmo coercDb.cmi cicCoercion.cmi
-cicCoercion.cmx: refinementTool.cmx coercDb.cmx cicCoercion.cmi
+cicCoercion.cmo: coercDb.cmi cicCoercion.cmi
+cicCoercion.cmx: coercDb.cmx cicCoercion.cmi
librarySync.cmo: refinementTool.cmo libraryDb.cmi coercDb.cmi cicRecord.cmi \
cicElim.cmi cicCoercion.cmi librarySync.cmi
librarySync.cmx: refinementTool.cmx libraryDb.cmx coercDb.cmx cicRecord.cmx \
cicElim.cmx cicCoercion.cmx librarySync.cmi
-libraryNoDb.cmo: libraryNoDb.cmi
-libraryNoDb.cmx: libraryNoDb.cmi
-libraryClean.cmo: librarySync.cmi libraryNoDb.cmi libraryMisc.cmi \
- libraryDb.cmi libraryClean.cmi
-libraryClean.cmx: librarySync.cmx libraryNoDb.cmx libraryMisc.cmx \
- libraryDb.cmx libraryClean.cmi
+libraryClean.cmo: librarySync.cmi libraryMisc.cmi libraryDb.cmi \
+ libraryClean.cmi
+libraryClean.cmx: librarySync.cmx libraryMisc.cmx libraryDb.cmx \
+ libraryClean.cmi
-cicCoercion.cmi: refinementTool.cmx coercDb.cmi
+cicCoercion.cmi: coercDb.cmi
librarySync.cmi: refinementTool.cmx
cicElim.cmo: cicElim.cmi
cicElim.cmx: cicElim.cmi
libraryDb.cmx: libraryDb.cmi
coercDb.cmo: coercDb.cmi
coercDb.cmx: coercDb.cmi
-cicCoercion.cmo: refinementTool.cmx coercDb.cmi cicCoercion.cmi
-cicCoercion.cmx: refinementTool.cmx coercDb.cmx cicCoercion.cmi
+cicCoercion.cmo: coercDb.cmi cicCoercion.cmi
+cicCoercion.cmx: coercDb.cmx cicCoercion.cmi
librarySync.cmo: refinementTool.cmx libraryDb.cmi coercDb.cmi cicRecord.cmi \
cicElim.cmi cicCoercion.cmi librarySync.cmi
librarySync.cmx: refinementTool.cmx libraryDb.cmx coercDb.cmx cicRecord.cmx \
cicElim.cmx cicCoercion.cmx librarySync.cmi
-libraryNoDb.cmo: libraryNoDb.cmi
-libraryNoDb.cmx: libraryNoDb.cmi
-libraryClean.cmo: librarySync.cmi libraryNoDb.cmi libraryMisc.cmi \
- libraryDb.cmi libraryClean.cmi
-libraryClean.cmx: librarySync.cmx libraryNoDb.cmx libraryMisc.cmx \
- libraryDb.cmx libraryClean.cmi
+libraryClean.cmo: librarySync.cmi libraryMisc.cmi libraryDb.cmi \
+ libraryClean.cmi
+libraryClean.cmx: librarySync.cmx libraryMisc.cmx libraryDb.cmx \
+ libraryClean.cmi
coercDb.mli \
cicCoercion.mli \
librarySync.mli \
- libraryNoDb.mli \
libraryClean.mli \
$(NULL)
IMPLEMENTATION_FILES = \
let cache_of_processed_baseuri = Hashtbl.create 1024
-let one_step_depend suri =
+let one_step_depend suri dbtype dbd =
let buri =
try
UM.buri_of_uri (UM.uri_of_string suri)
Hashtbl.add cache_of_processed_baseuri buri true;
let query =
let buri = buri ^ "/" in
- let buri = HSql.escape buri in
+ let buri = HSql.escape dbtype dbd buri in
let obj_tbl = MetadataTypes.obj_tbl () in
- if HSql.isMysql then
+ if HSql.isMysql dbtype dbd then
sprintf ("SELECT source, h_occurrence FROM %s WHERE "
^^ "h_occurrence REGEXP '^%s[^/]*$'") obj_tbl buri
else
end
in
try
- let rc = HSql.exec (LibraryDb.instance ()) query in
+ let rc = HSql.exec dbtype dbd query in
let l = ref [] in
HSql.iter rc (
fun row ->
UM.IllFormedUri _ -> suri
let db_uris_of_baseuri buri =
+ let dbd = LibraryDb.instance () in
+ let dbtype =
+ if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User
+ in
let query =
let buri = buri ^ "/" in
- let buri = HSql.escape buri in
+ let buri = HSql.escape dbtype dbd buri in
let obj_tbl = MetadataTypes.name_tbl () in
- if HSql.isMysql then
+ if HSql.isMysql dbtype dbd then
sprintf ("SELECT source FROM %s WHERE "
^^ "source REGEXP '^%s[^/]*$'") obj_tbl buri
else
end
in
try
- let rc = HSql.exec (LibraryDb.instance ()) query in
+ let rc = HSql.exec dbtype dbd query in
let l = ref [] in
HSql.iter rc (
fun row ->
;;
let close_uri_list uri_to_remove =
+ let dbd = LibraryDb.instance () in
+ let dbtype =
+ if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User
+ in
(* to remove an uri you have to remove the whole script *)
let buri_to_remove =
HExtlib.list_uniq
try
List.fold_left
(fun acc buri ->
- let inhabitants = HG.ls (buri ^ "/") in
+ let inhabitants = HG.ls ~local:true (buri ^ "/") in
let inhabitants = List.filter
(function HGT.Ls_object _ -> true | _ -> false)
inhabitants
(* now we want the list of all uri that depend on them *)
let depend =
List.fold_left
- (fun acc u -> one_step_depend u @ acc) [] uri_to_remove
+ (fun acc u -> one_step_depend u dbtype dbd @ acc) [] uri_to_remove
in
let depend =
HExtlib.list_uniq (List.fast_sort Pervasives.compare depend)
String.sub url 7 (String.length url - 7) (* remove heading "file:///" *)
)
-let close_nodb buris =
- let rev_deps = Hashtbl.create 97 in
- let all_metadata =
- HExtlib.find ~test:(fun name -> Filename.check_suffix name ".metadata")
- (Lazy.force moo_root_dir)
- in
- List.iter
- (fun path ->
- let metadata = LibraryNoDb.load_metadata ~fname:path in
- let baseuri_of_current_metadata =
- prerr_endline "ERROR, add to the getter reverse lookup";
- let basedir = "/fake" in
- let dirname = Filename.dirname path in
- let basedirlen = String.length basedir in
- assert (String.sub dirname 0 basedirlen = basedir);
- "cic:" ^
- String.sub dirname basedirlen (String.length dirname - basedirlen) ^
- Filename.basename path
- in
- let deps =
- HExtlib.filter_map
- (function LibraryNoDb.Dependency buri -> Some buri)
- metadata
- in
- List.iter
- (fun buri -> Hashtbl.add rev_deps buri baseuri_of_current_metadata) deps)
- all_metadata;
- 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 =
+ let dbd = LibraryDb.instance () in
+ let dbtype =
+ if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User
+ in
Hashtbl.clear cache_of_processed_baseuri;
let buris = List.map Http_getter_misc.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_nodb buris
- else
- close_db [] buris
- in
+ let l = close_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:";
LibraryMisc.obj_file_of_baseuri ~must_exist:false ~writable:true ~baseuri
in
HExtlib.safe_remove obj_file ;
- HExtlib.safe_remove
- (LibraryMisc.metadata_file_of_baseuri
- ~must_exist:false ~writable:true ~baseuri) ;
HExtlib.safe_remove
(LibraryMisc.lexicon_file_of_baseuri
~must_exist:false ~writable:true ~baseuri) ;
end;
LibrarySync.remove_obj uri
) l;
- if HSql.isMysql then
+ if HSql.isMysql dbtype dbd then
begin
cleaned_no := !cleaned_no + List.length l;
- if !cleaned_no > 30 then
+ if !cleaned_no > 30 && HSql.isMysql dbtype dbd then
begin
cleaned_no := 0;
List.iter
(function table ->
- ignore (HSql.exec (LibraryDb.instance ()) ("OPTIMIZE TABLE " ^ table)))
+ ignore (HSql.exec dbtype dbd ("OPTIMIZE TABLE " ^ table)))
[MetadataTypes.name_tbl (); MetadataTypes.rel_tbl ();
MetadataTypes.sort_tbl (); MetadataTypes.obj_tbl();
MetadataTypes.count_tbl()]
open Printf ;;
+let parse_dbd_conf _ =
+ let metadata = Helm_registry.get_list Helm_registry.string "db.metadata" in
+ List.map
+ (fun s ->
+ match Pcre.split ~pat:"\\s+" s with
+ | [path;db;user;pwd;dbtype] ->
+ let dbtype =
+ if dbtype = "library" then HSql.Library
+ else if dbtype = "user" then HSql.User
+ else if dbtype = "legacy" then HSql.Legacy
+ else raise (HSql.Error "HSql: wrong config file format")
+ in
+ let pwd = if pwd = "none" then None else Some pwd in
+ (* TODO parse port *)
+ path, None, db, user, pwd, dbtype
+ | _ -> raise (HSql.Error "HSql: Bad format in config file"))
+ metadata
+;;
+
+let parse_dbd_conf _ =
+ HSql.mk_dbspec (parse_dbd_conf ())
+;;
+
let instance =
let dbd = lazy (
- HSql.quick_connect
- ~host:(Helm_registry.get "db.host")
- ~user:(Helm_registry.get "db.user")
- ~database:(Helm_registry.get "db.database")
- ())
+ let dbconf = parse_dbd_conf () in
+ HSql.quick_connect dbconf)
in
fun () -> Lazy.force dbd
-
+;;
let xpointer_RE = Pcre.regexp "#.*$"
let file_scheme_RE = Pcre.regexp "^file://"
(obj_tbl,`RefObj) ; (sort_tbl,`RefSort) ; (rel_tbl,`RefRel) ;
(name_tbl,`ObjectName) ; (count_tbl,`Count) ]
in
+ let dbtype =
+ if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User
+ in
let statements =
- (SqlStatements.drop_tables tbls) @ (SqlStatements.drop_indexes tbls)
+ (SqlStatements.drop_tables tbls) @
+ (SqlStatements.drop_indexes tbls dbtype dbd)
in
let owned_uris =
try
MetadataDb.clean ~dbd
with (HSql.Error _) as exn ->
- match HSql.errno dbd with
+ match HSql.errno dbtype dbd with
| HSql.No_such_table -> []
| _ -> raise exn
in
(fun suffix ->
try
HExtlib.safe_remove
- (Http_getter.resolve ~writable:true (uri ^ suffix))
+ (Http_getter.resolve ~local:true ~writable:true (uri ^ suffix))
with Http_getter_types.Key_not_found _ -> ())
[""; ".body"; ".types"])
owned_uris;
List.iter (fun statement ->
try
- ignore (HSql.exec dbd statement)
+ ignore (HSql.exec dbtype dbd statement)
with (HSql.Error _) as exn ->
- match HSql.errno dbd with
+ match HSql.errno dbtype dbd with
| HSql.No_such_table
| HSql.Bad_table_error
| HSql.No_such_index -> prerr_endline statement; ()
(l_obj_tbl,`RefObj) ; (l_sort_tbl,`RefSort) ; (l_rel_tbl,`RefRel) ;
(l_name_tbl,`ObjectName) ; (l_count_tbl,`Count) ]
in
+ let tag tag l = List.map (fun x -> tag, x) l in
let statements =
- (SqlStatements.create_tables system_tbls) @
- (SqlStatements.create_tables tbls) @
- (SqlStatements.create_indexes system_tbls) @
- (SqlStatements.create_indexes tbls)
+ (tag HSql.Library (SqlStatements.create_tables system_tbls)) @
+ (tag HSql.User (SqlStatements.create_tables tbls)) @
+ (tag HSql.Library (SqlStatements.create_indexes system_tbls)) @
+ (tag HSql.User (SqlStatements.create_indexes tbls))
in
- List.iter (fun statement ->
- try
- ignore (HSql.exec dbd statement)
- with
- (HSql.Error _) as exc ->
- let status = HSql.errno dbd in
- match status with
- | HSql.Table_exists_error -> ()
- | HSql.Dup_keyname -> ()
- | HSql.GENERIC_ERROR _ ->
- prerr_endline statement;
- raise exc
- | _ -> ()
-
-
- ) statements
+ List.iter
+ (fun (dbtype, statement) ->
+ try
+ ignore (HSql.exec dbtype dbd statement)
+ with
+ (HSql.Error _) as exc ->
+ let status = HSql.errno dbtype dbd in
+ match status with
+ | HSql.Table_exists_error -> ()
+ | HSql.Dup_keyname -> ()
+ | HSql.GENERIC_ERROR _ ->
+ prerr_endline statement;
+ raise exc
+ | _ -> ())
+ statements
;;
(* removes uri from the ownerized tables, and returns the list of other objects
let dbd = instance () in
let suri = UriManager.string_of_uri uri in
+ let dbtype =
+ if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User
+ in
let query table suri =
- if HSql.isMysql then
- sprintf "DELETE QUICK LOW_PRIORITY FROM %s WHERE source='%s'" table (HSql.escape suri)
- else sprintf "DELETE FROM %s WHERE source='%s'" table (HSql.escape suri)
+ if HSql.isMysql dbtype dbd then
+ sprintf "DELETE QUICK LOW_PRIORITY FROM %s WHERE source='%s'" table
+ (HSql.escape dbtype dbd suri)
+ else
+ sprintf "DELETE FROM %s WHERE source='%s'" table
+ (HSql.escape dbtype dbd suri)
in
List.iter (fun t ->
try
- ignore (HSql.exec dbd (query t suri))
+ ignore (HSql.exec dbtype dbd (query t suri))
with
exn -> raise exn (* no errors should be accepted *)
)
let xpointers_of_ind uri =
let dbd = instance () in
let name_tbl = MetadataTypes.name_tbl () in
+ let dbtype =
+ if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User
+ in
let escape s =
- Pcre.replace ~pat:"([^\\\\])_" ~templ:"$1\\_" (HSql.escape s)
+ Pcre.replace ~pat:"([^\\\\])_" ~templ:"$1\\_"
+ (HSql.escape dbtype dbd s)
in
let query = sprintf
("SELECT source FROM %s WHERE source LIKE '%s#xpointer%%' "
- ^^ HSql.escape_string_for_like)
+ ^^ HSql.escape_string_for_like dbtype dbd)
name_tbl (escape (UriManager.string_of_uri uri))
in
- let rc = HSql.exec dbd query in
+ let rc = HSql.exec dbtype dbd query in
let l = ref [] in
HSql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l := a:: !l);
List.map UriManager.uri_of_string !l
*)
val instance: unit -> HSql.dbd
+val parse_dbd_conf: unit -> HSql.dbspec
val create_owner_environment: unit -> unit
val clean_owner_environment: unit -> unit
(* $Id$ *)
-let resolve ~must_exist ~writable baseuri =
+let resolve ~must_exist ~writable ~local baseuri =
if must_exist then
- Http_getter.resolve ~writable baseuri
+ Http_getter.resolve ~local ~writable baseuri
else
- Http_getter.filename ~writable baseuri
+ Http_getter.filename ~local ~writable baseuri
let obj_file_of_baseuri ~must_exist ~writable ~baseuri =
- resolve ~must_exist ~writable baseuri ^ ".moo"
+ resolve ~must_exist ~writable ~local:true baseuri ^ ".moo"
let lexicon_file_of_baseuri ~must_exist ~writable ~baseuri =
- resolve ~must_exist ~writable baseuri ^ ".lexicon"
-let metadata_file_of_baseuri~must_exist ~writable ~baseuri =
- resolve ~must_exist ~writable baseuri ^ ".metadata"
+ resolve ~must_exist ~writable ~local:true baseuri ^ ".lexicon"
* http://helm.cs.unibo.it/
*)
+(* only for local uris *)
val obj_file_of_baseuri:
must_exist:bool -> writable:bool -> baseuri:string -> string
val lexicon_file_of_baseuri:
must_exist:bool -> writable:bool -> baseuri:string -> string
-val metadata_file_of_baseuri:
- must_exist:bool -> writable:bool -> baseuri:string -> string
+++ /dev/null
-(* 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/
- *)
-
-(* $Id$ *)
-
-open Printf
-
-exception Checksum_failure of string
-exception Corrupt_metadata of string
-exception Version_mismatch of string
-
-let magic = 1
-let format_name = "metadata"
-
-type metadata =
- | Dependency of string (* baseuri without trailing slash *)
-
-let eq_metadata (m1:metadata) (m2:metadata) = m1 = m2
-
-let save_metadata_to_file ~fname metadata =
- HMarshal.save ~fmt:format_name ~version:magic ~fname metadata
-
-let load_metadata_from_file ~fname =
- let raw = HMarshal.load ~fmt:format_name ~version:magic ~fname in
- (raw: metadata list)
-
-let save_metadata ~fname metadata = save_metadata_to_file ~fname metadata
-let load_metadata ~fname = load_metadata_from_file ~fname
-
+++ /dev/null
-(* 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/
- *)
-
-(* TODO the strings below should be UriManager.uri, but UriManager ATM does not
- * support their format *)
-type metadata =
- | Dependency of string (* baseuri without trailing slash *)
-
-val eq_metadata: metadata -> metadata -> bool
-
-val save_metadata: fname:string -> metadata list -> unit
-val load_metadata: fname:string -> metadata list
-
innertypesuri,bodyuri,univgraphuri
let paths_and_uris_of_obj uri =
- let resolved = Http_getter.filename' ~writable:true uri in
+ let resolved = Http_getter.filename' ~local:true ~writable:true uri in
let basepath = Filename.dirname resolved in
let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
let innertypesfilename=(UriManager.nameext_of_uri innertypesuri)^".xml.gz"in
List.iter
(fun uri ->
(try
- let file = Http_getter.resolve' ~writable:true uri in
+ let file = Http_getter.resolve' ~local:true ~writable:true uri in
HExtlib.safe_remove file;
HExtlib.rmdir_descend (Filename.dirname file)
with Http_getter_types.Key_not_found _ -> ());
in
((n+2), from, where)
-let exec ~(dbd:HSql.dbd) ?rating (n,from,where) =
+let exec dbtype ~(dbd:HSql.dbd) ?rating (n,from,where) =
let from = String.concat ", " from in
let where = String.concat " and " where in
let query =
from where
in
(* prerr_endline query; *)
- let result = HSql.exec dbd query in
+ let result = HSql.exec dbtype dbd query in
HSql.map result
- (fun row -> match row.(0) with Some s -> UriManager.uri_of_string s | _ -> assert false)
-
+ ~f:(fun row ->
+ match row.(0) with Some s -> UriManager.uri_of_string s
+ | _ -> assert false)
+;;
-let at_least ~(dbd:HSql.dbd) ?concl_card ?full_card ?diff ?rating tables
+let at_least dbtype ~(dbd:HSql.dbd) ?concl_card ?full_card ?diff ?rating tables
(metadata: MetadataTypes.constr list)
=
let obj_tbl,rel_tbl,sort_tbl, count_tbl = tables in
let (n,from,where) =
add_all_constr ~tbl:count_tbl (n,from,where) concl_card full_card diff
in
- exec ~dbd ?rating (n,from,where)
+ exec dbtype ~dbd ?rating (n,from,where)
;;
let at_least
(metadata: MetadataTypes.constr list)
=
if are_tables_ownerized () then
- (at_least
- ~dbd ?concl_card ?full_card ?diff ?rating default_tables metadata) @
- (at_least
- ~dbd ?concl_card ?full_card ?diff ?rating (current_tables ()) metadata)
+ at_least
+ HSql.Library ~dbd ?concl_card ?full_card ?diff ?rating
+ default_tables metadata
+ @
+ at_least
+ HSql.Legacy ~dbd ?concl_card ?full_card ?diff ?rating
+ default_tables metadata
+ @
+ at_least
+ HSql.User ~dbd ?concl_card ?full_card ?diff ?rating
+ (current_tables ()) metadata
+
else
at_least
- ~dbd ?concl_card ?full_card ?diff ?rating default_tables metadata
+ HSql.Library ~dbd ?concl_card ?full_card ?diff ?rating
+ default_tables metadata
+ @
+ at_least
+ HSql.Legacy ~dbd ?concl_card ?full_card ?diff ?rating
+ default_tables metadata
(** Prefix handling *)
[ MetadataTypes.mainconcl_pos; MetadataTypes.inconcl_pos;
MetadataTypes.inhyp_pos; MetadataTypes.mainhyp_pos ]
in
- let query =
- let pos_predicate =
- String.concat " OR "
- (List.map (fun pos -> sprintf "(h_position = \"%s\")" pos) positions)
- in
- sprintf ("SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s) UNION "^^
- "SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s)")
- (MetadataTypes.obj_tbl ()) uri pos_predicate
- MetadataTypes.library_obj_tbl uri pos_predicate
-
+ let pos_predicate =
+ String.concat " OR "
+ (List.map (fun pos -> sprintf "(h_position = \"%s\")" pos) positions)
+ in
+ let query tbl =
+ sprintf "SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s)"
+ tbl uri pos_predicate
+ in
+ let db = [
+ HSql.Library, MetadataTypes.library_obj_tbl;
+ HSql.Legacy, MetadataTypes.library_obj_tbl;
+ HSql.User, MetadataTypes.obj_tbl ()]
in
- let result = HSql.exec dbd query in
let set = ref UriManagerSet.empty in
- HSql.iter result
- (fun col ->
- match col.(0) with
- | Some uri -> set := UriManagerSet.add (UriManager.uri_of_string uri) !set
- | _ -> assert false);
+ List.iter
+ (fun (dbtype, table) ->
+ let result = HSql.exec dbtype dbd (query table) in
+ HSql.iter result
+ (fun col ->
+ match col.(0) with
+ | Some uri ->
+ set := UriManagerSet.add (UriManager.uri_of_string uri) !set
+ | _ -> assert false))
+ db;
!set
let at_most ~(dbd:HSql.dbd) ?(where = `Conclusion) only u =
int * string list * string list
val exec:
+ HSql.dbtype ->
dbd:HSql.dbd ->
?rating:[ `Hits ] ->
int * string list * string list ->
open Printf
-let format_insert tbl tuples =
- if HSql.isMysql then
+let format_insert dbtype dbd tbl tuples =
+ if HSql.isMysql dbtype dbd then
[sprintf "INSERT %s VALUES %s;" tbl (String.concat "," tuples)]
else
List.map (fun tup ->
| _ -> assert false)
[] obj_cols
in
+ let dbtype =
+ if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User
+ in
if sort_tuples <> [] then
begin
let query_sort =
- format_insert(sort_tbl ()) sort_tuples
+ format_insert dbtype dbd (sort_tbl ()) sort_tuples
in
- List.iter (fun query -> ignore (HSql.exec dbd query)) query_sort
+ List.iter (fun query -> ignore (HSql.exec dbtype dbd query)) query_sort
end;
if rel_tuples <> [] then
begin
let query_rel =
- format_insert(rel_tbl ()) rel_tuples
+ format_insert dbtype dbd (rel_tbl ()) rel_tuples
in
- List.iter (fun query -> ignore (HSql.exec dbd query)) query_rel
+ List.iter (fun query -> ignore (HSql.exec dbtype dbd query)) query_rel
end;
if obj_tuples <> [] then
begin
let query_obj =
- format_insert(obj_tbl ()) obj_tuples
+ format_insert dbtype dbd (obj_tbl ()) obj_tuples
in
- List.iter (fun query -> ignore (HSql.exec dbd query)) query_obj
+ List.iter (fun query -> ignore (HSql.exec dbtype dbd query)) query_obj
end
(sprintf "(\"%s\", %d, %d, %d)"
(UriManager.string_of_uri uri) no_concl no_hyp no_full) :: acc
) [] l in
+ let dbtype =
+ if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User
+ in
let insert =
- format_insert(count_tbl ()) data
+ format_insert dbtype dbd (count_tbl ()) data
in
- List.iter (fun query -> ignore (HSql.exec dbd query)) insert
+ List.iter (fun query -> ignore (HSql.exec dbtype dbd query)) insert
let insert_name ~dbd l =
+ let dbtype =
+ if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User
+ in
let data =
List.fold_left
(fun acc (uri,name,_) ->
(sprintf "(\"%s\", \"%s\")" (UriManager.string_of_uri uri) name) :: acc
) [] l in
let insert =
- format_insert(name_tbl ()) data
+ format_insert dbtype dbd (name_tbl ()) data
in
- List.iter (fun query -> ignore (HSql.exec dbd query)) insert
+ List.iter (fun query -> ignore (HSql.exec dbtype dbd query)) insert
type columns =
MetadataPp.t list list * MetadataPp.t list list * MetadataPp.t list list
let eventually_analyze dbd =
incr analyze_index;
if !analyze_index > 30 then
- if HSql.isMysql then
+ if HSql.isMysql HSql.User dbd then
begin
let analyze t = "OPTIMIZE TABLE " ^ t ^ ";" in
List.iter
- (fun table -> ignore (HSql.exec dbd (analyze table)))
+ (fun table -> ignore (HSql.exec HSql.User dbd (analyze table)))
[name_tbl (); rel_tbl (); sort_tbl (); obj_tbl(); count_tbl()]
end
let clean ~(dbd:HSql.dbd) =
let owned_uris = (* list of uris in list-of-columns format *)
let query = sprintf "SELECT source FROM %s" (name_tbl ()) in
- let result = HSql.exec dbd query in
+ let result = HSql.exec HSql.User dbd query in
let uris = HSql.map result (fun cols ->
match cols.(0) with
| Some src -> src
in
let del_from tbl =
let escape s =
- Pcre.replace ~pat:"([^\\\\])_" ~templ:"$1\\_" (HSql.escape s)
+ Pcre.replace ~pat:"([^\\\\])_" ~templ:"$1\\_" (HSql.escape HSql.User dbd s)
in
let query s =
sprintf
("DELETE FROM %s WHERE source LIKE \"%s%%\" " ^^
- HSql.escape_string_for_like)
+ HSql.escape_string_for_like HSql.User dbd)
(tbl ()) (escape s)
in
List.iter
- (fun source_col -> ignore (HSql.exec dbd (query source_col)))
+ (fun source_col -> ignore (HSql.exec HSql.User dbd (query source_col)))
owned_uris
in
List.iter del_from tables_to_clean;
let uri = UriManager.string_of_uri uri in
let del_from tbl =
let escape s =
- Pcre.replace ~pat:"([^\\\\])_" ~templ:"$1\\_" (HSql.escape s)
+ Pcre.replace
+ ~pat:"([^\\\\])_" ~templ:"$1\\_" (HSql.escape HSql.User dbd s)
in
let query tbl =
sprintf
("DELETE FROM %s WHERE source LIKE \"%s%%\" " ^^
- HSql.escape_string_for_like)
+ HSql.escape_string_for_like HSql.User dbd)
(tbl ()) (escape uri)
in
- ignore (HSql.exec dbd (query tbl))
+ ignore (HSql.exec HSql.User dbd (query tbl))
in
List.iter del_from tables_to_clean
prerr_endline "invalid (direct) refObj metadata row";
assert false
in
- let do_query tbl =
- let res = HSql.exec dbd (SqlStatements.direct_deps tbl uri) in
+ let do_query (dbtype, tbl) =
+ let res =
+ HSql.exec dbtype dbd (SqlStatements.direct_deps tbl uri dbtype dbd)
+ in
let deps =
HSql.map res (fun row -> unbox_row (obj_metadata_of_row row)) in
deps
in
- do_query (MetadataTypes.obj_tbl ())
- @ do_query MetadataTypes.library_obj_tbl
+ do_query (HSql.User, MetadataTypes.obj_tbl ())
+ @ do_query (HSql.Library, MetadataTypes.library_obj_tbl)
+ @ do_query (HSql.Legacy, MetadataTypes.library_obj_tbl)
let inverse_deps ~dbd uri =
let inv_obj_metadata_of_row =
prerr_endline "invalid (inverse) refObj metadata row";
assert false
in
- let do_query tbl =
- let res = HSql.exec dbd (SqlStatements.inverse_deps tbl uri) in
+ let do_query (dbtype, tbl) =
+ let res =
+ HSql.exec dbtype dbd (SqlStatements.inverse_deps tbl uri dbtype dbd)
+ in
let deps =
HSql.map res (fun row -> unbox_row (inv_obj_metadata_of_row row)) in
deps
in
- do_query (MetadataTypes.obj_tbl ())
- @ do_query MetadataTypes.library_obj_tbl
+ do_query (HSql.User, MetadataTypes.obj_tbl ())
+ @ do_query (HSql.Library, MetadataTypes.library_obj_tbl)
+ @ do_query (HSql.Legacy, MetadataTypes.library_obj_tbl)
let topological_sort ~dbd uris =
let module OrderedUri =
let sql_pat =
Pcre.replace ~pat:"([^\\\\])_" ~templ:"$1\\_" baseuri ^ "%"
in
- let query =
+ let query dbtype tbl =
Printf.sprintf
("SELECT source FROM %s WHERE source LIKE \"%s\" "
- ^^ HSql.escape_string_for_like ^^ " UNION " ^^
- "SELECT source FROM %s WHERE source LIKE \"%s\" "
- ^^ HSql.escape_string_for_like)
- (MetadataTypes.name_tbl ()) sql_pat
- MetadataTypes.library_name_tbl sql_pat
+ ^^ HSql.escape_string_for_like dbtype dbd)
+ tbl sql_pat
in
- let result = HSql.exec dbd query in
let map cols = match cols.(0) with
| Some s -> UriManager.uri_of_string s
| _ -> assert false
in
- let uris = HSql.map result map in
+ let uris =
+ List.fold_left
+ (fun acc (dbtype, table) ->
+ let result = HSql.exec dbtype dbd (query dbtype table) in
+ HSql.map result map @ acc)
+ []
+ [HSql.User, MetadataTypes.name_tbl ();
+ HSql.Library, MetadataTypes.library_name_tbl;
+ HSql.Legacy, MetadataTypes.library_name_tbl]
+ in
let sorted_uris = topological_sort ~dbd uris in
let filter_map uri =
let s =
let sprintf_refRel_index name = [
sprintf "CREATE INDEX %s_index ON %s (source,h_position,h_depth);" name name]
-let format_drop name sufix =
- if HSql.isMysql then
+let format_drop name sufix dtype dbd =
+ if HSql.isMysql dtype dbd then
(sprintf "DROP INDEX %s_%s ON %s;" name sufix name)
else
(sprintf "DROP INDEX %s_%s;" name sufix);;
-let sprintf_refObj_index_drop name = [(format_drop name "index")]
+let sprintf_refObj_index_drop name dtype dbd= [(format_drop name "index" dtype dbd)]
-let sprintf_refSort_index_drop name = [(format_drop name "index")]
+let sprintf_refSort_index_drop name dtype dbd = [(format_drop name "index" dtype dbd)]
-let sprintf_objectName_index_drop name = [(format_drop name "value")]
+let sprintf_objectName_index_drop name dtype dbd = [(format_drop name "value" dtype dbd)]
-let sprintf_hits_index_drop name = [
-(format_drop name "source");
-(format_drop name "no")]
+let sprintf_hits_index_drop name dtype dbd = [
+(format_drop name "source" dtype dbd);
+(format_drop name "no" dtype dbd)]
-let sprintf_count_index_drop name = [
-(format_drop name "source");
-(format_drop name "conclusion");
-(format_drop name "hypothesis");
-(format_drop name "statement")]
+let sprintf_count_index_drop name dtype dbd = [
+(format_drop name "source" dtype dbd);
+(format_drop name "conclusion" dtype dbd);
+(format_drop name "hypothesis" dtype dbd);
+(format_drop name "statement" dtype dbd)]
-let sprintf_refRel_index_drop name = [(format_drop name "index")]
+let sprintf_refRel_index_drop name dtype dbd =
+ [(format_drop name "index" dtype dbd)]
let sprintf_rename_table oldname newname = [
sprintf "RENAME TABLE %s TO %s;" oldname newname
| `Hits -> sprintf_hits_drop named
| `Count -> sprintf_count_drop named
-let get_index_drop t named =
+let get_index_drop t named dtype dbd =
match t with
- | `RefObj -> sprintf_refObj_index_drop named
- | `RefSort -> sprintf_refSort_index_drop named
- | `RefRel -> sprintf_refRel_index_drop named
- | `ObjectName -> sprintf_objectName_index_drop named
- | `Hits -> sprintf_hits_index_drop named
- | `Count -> sprintf_count_index_drop named
+ | `RefObj -> sprintf_refObj_index_drop named dtype dbd
+ | `RefSort -> sprintf_refSort_index_drop named dtype dbd
+ | `RefRel -> sprintf_refRel_index_drop named dtype dbd
+ | `ObjectName -> sprintf_objectName_index_drop named dtype dbd
+ | `Hits -> sprintf_hits_index_drop named dtype dbd
+ | `Count -> sprintf_count_index_drop named dtype dbd
let create_tables l =
List.fold_left (fun s (name,table) -> s @ get_table_format table name) [] l
let drop_tables l =
List.fold_left (fun s (name,table) -> s @ get_table_drop table name) [] l
-let drop_indexes l =
- List.fold_left (fun s (name,table) -> s @ get_index_drop table name) [] l
+let drop_indexes l dtype dbd=
+ List.fold_left (fun s (name,table) -> s @ get_index_drop table name dtype dbd) [] l
let rename_tables l =
List.fold_left (fun s (o,n) -> s @ sprintf_rename_table o n) [] l
hits refObj ]
-let move_content (name1, tbl1) (name2, tbl2) buri =
+let move_content (name1, tbl1) (name2, tbl2) buri dtype dbd =
let escape s =
- Pcre.replace ~pat:"([^\\\\])_" ~templ:"$1\\_" (HSql.escape s)
+ Pcre.replace ~pat:"([^\\\\])_" ~templ:"$1\\_" (HSql.escape dtype dbd s)
in
assert (tbl1 = tbl2);
sprintf
"INSERT INTRO %s SELECT * FROM %s WHERE source LIKE \"%s%%\";"
name2 name1 (escape buri)
-let direct_deps refObj uri =
+let direct_deps refObj uri dtype dbd =
sprintf "SELECT * FROM %s WHERE source = \"%s\";"
- (HSql.escape refObj) (UriManager.string_of_uri uri)
+ (HSql.escape dtype dbd refObj) (UriManager.string_of_uri uri)
-let inverse_deps refObj uri =
+let inverse_deps refObj uri dtype dbd =
sprintf "SELECT * FROM %s WHERE h_occurrence = \"%s\";"
- (HSql.escape refObj) (UriManager.string_of_uri uri)
+ (HSql.escape dtype dbd refObj) (UriManager.string_of_uri uri)
val create_tables: (string * tbl) list -> string list
val create_indexes: (string * tbl) list -> string list
val drop_tables: (string * tbl) list -> string list
-val drop_indexes: (string * tbl) list -> string list
+val drop_indexes: (string * tbl) list -> HSql.dbtype -> HSql.dbd -> string list
val rename_tables: (string * string) list -> string list
(** @param refObj name of the refObj table
(** move content [t1] [t2] [buri]
* moves all the tuples with 'source' that match regex '^buri' from t1 to t2
* *)
-val move_content: (string * tbl) -> (string * tbl) -> string -> string
+val move_content: (string * tbl) -> (string * tbl) -> string -> HSql.dbtype ->
+ HSql.dbd -> string
(** @param refObj name of the refObj table
* @param src uri of the desired 'source' field *)
-val direct_deps: string -> UriManager.uri -> string
+val direct_deps: string -> UriManager.uri -> HSql.dbtype -> HSql.dbd -> string
(** @param refObj name of the refObj table
* @param src uri of the desired 'h_occurrence' field *)
-val inverse_deps: string -> UriManager.uri -> string
+val inverse_deps: string -> UriManager.uri -> HSql.dbtype -> HSql.dbd -> string
fourierR.cmi: proofEngineTypes.cmi
fwdSimplTactic.cmi: proofEngineTypes.cmi
statefulProofEngine.cmi: proofEngineTypes.cmi
-tactics.cmi: universe.cmi tacticals.cmi proofEngineTypes.cmi
declarative.cmi: universe.cmi proofEngineTypes.cmi
proofEngineTypes.cmo: proofEngineTypes.cmi
proofEngineTypes.cmx: proofEngineTypes.cmi
hashtbl_equiv.cmi metadataQuery.cmi
metadataQuery.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
hashtbl_equiv.cmx metadataQuery.cmi
-closeCoercionGraph.cmo: closeCoercionGraph.cmi
-closeCoercionGraph.cmx: closeCoercionGraph.cmi
universe.cmo: proofEngineTypes.cmi proofEngineReduction.cmi universe.cmi
universe.cmx: proofEngineTypes.cmx proofEngineReduction.cmx universe.cmi
autoTypes.cmo: autoTypes.cmi
autoCache.cmx: universe.cmx autoCache.cmi
paramodulation/utils.cmo: proofEngineReduction.cmi paramodulation/utils.cmi
paramodulation/utils.cmx: proofEngineReduction.cmx paramodulation/utils.cmi
+closeCoercionGraph.cmo: closeCoercionGraph.cmi
+closeCoercionGraph.cmx: closeCoercionGraph.cmi
paramodulation/subst.cmo: paramodulation/subst.cmi
paramodulation/subst.cmx: paramodulation/subst.cmi
paramodulation/equality.cmo: paramodulation/utils.cmi \
introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \
equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \
compose.cmx closeCoercionGraph.cmx auto.cmx tactics.cmi
-declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi \
+declarative.cmo: universe.cmi tactics.cmi tacticals.cmi proofEngineTypes.cmi \
declarative.cmi
-declarative.cmx: tactics.cmx tacticals.cmx proofEngineTypes.cmx \
+declarative.cmx: universe.cmx tactics.cmx tacticals.cmx proofEngineTypes.cmx \
declarative.cmi
if List.exists (UriManager.eq uri) l then retry ()
else
try
- let _ = Http_getter.resolve' ~writable:true uri in
- if Http_getter.exists' uri then retry () else uri
+ let _ = Http_getter.resolve' ~local:true ~writable:true uri in
+ if Http_getter.exists' ~local:true uri then retry () else uri
with
| Http_getter_types.Key_not_found _ -> uri
| Http_getter_types.Unresolvable_URI _ -> assert false
[] [] univ arity true
in
if (menv = []) then
- prerr_endline
- "MENV non empty after composing coercions";
+ HLog.warn "MENV non empty after composing coercions";
build_obj t univ arity
| _ -> assert false
) (first_step, CicUniv.empty_ugraph) tl
-(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Jun 13 14:11:00 CEST 2007 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Fri Jul 6 11:03:35 CEST 2007 *)
val absurd : term:Cic.term -> ProofEngineTypes.tactic
val apply : term:Cic.term -> ProofEngineTypes.tactic
val applyS :
let from = "genLemma" in
let where =
Printf.sprintf "h_outer = \"%s\""
- (HSql.escape (UriManager.string_of_uri outer)) in
+ (HSql.escape HSql.Library dbd (UriManager.string_of_uri outer)) in
let query = Printf.sprintf "SELECT %s FROM %s WHERE %s" select from where in
- let result = HSql.exec dbd query in
+ let result = HSql.exec HSql.Library dbd query in
let lemmas = HSql.map ~f:(map inners) result in
let ranked = List.fold_left rank [] lemmas in
let ordered = List.rev (List.fast_sort compare ranked) in
in
let select, from = "source", "decomposables" in
let query = Printf.sprintf "SELECT %s FROM %s" select from in
- let decomposables = HSql.map ~f:map (HSql.exec dbd query) in
+ let decomposables = HSql.map ~f:map (HSql.exec HSql.Library dbd query) in
filter_map_n (fun _ x -> x) 0 decomposables
shellglob)))
let locate ~(dbd:HSql.dbd) ?(vars = false) pat =
- let escape s = HSql.escape s in
+ let escape dbtype dbd s = HSql.escape dbtype dbd s in
let sql_pat = sqlpat_of_shellglob pat in
- let query =
+ let query dbtype tbl =
sprintf
("SELECT source FROM %s WHERE value LIKE \"%s\" "
- ^^ HSql.escape_string_for_like
- ^^ " UNION " ^^
- "SELECT source FROM %s WHERE value LIKE \"%s\" "
- ^^ HSql.escape_string_for_like)
- (MetadataTypes.name_tbl ()) (escape sql_pat)
- MetadataTypes.library_name_tbl (escape sql_pat)
+ ^^ HSql.escape_string_for_like dbtype dbd)
+ tbl (escape dbtype dbd sql_pat)
in
- let result = HSql.exec dbd query in
- List.filter nonvar
- (HSql.map result
- (fun cols -> match cols.(0) with Some s -> UriManager.uri_of_string s | _ -> assert false))
+ let tbls =
+ [HSql.User, MetadataTypes.name_tbl ();
+ HSql.Library, MetadataTypes.library_name_tbl;
+ HSql.Legacy, MetadataTypes.library_name_tbl]
+ in
+ let map cols =
+ match cols.(0) with
+ | Some s -> UriManager.uri_of_string s | _ -> assert false
+ in
+ let result =
+ List.fold_left
+ (fun acc (dbtype,tbl) ->
+ acc @ HSql.map ~f:map (HSql.exec dbtype dbd (query dbtype tbl)))
+ [] tbls
+ in
+ List.filter nonvar result
let match_term ~(dbd:HSql.dbd) ty =
(* debug_print (lazy (CicPp.ppterm ty)); *)
let constraints_for_dummy_type =
List.map MetadataTypes.constr_of_metadata metadata_for_dummy_type in
(* start with the dummy constant in main conlusion *)
- let from = ["refObj as table0"] in
+ let from = ["refObj as table0"] in (* XXX table hardcoded *)
let where =
[sprintf "table0.h_position = \"%s\"" MetadataTypes.mainconcl_pos;
sprintf "table0.h_depth >= %d" depth] in
sprintf "table0.h_depth - table%d.h_depth = %d"
n (depth - depth')::where
in
+ (* XXX performed only in library and legacy not user *)
let (m,from,where) =
List.fold_left
(MetadataConstraints.add_constraint ~start:n)
- (n,from,where) constraints_for_dummy_type in
- MetadataConstraints.exec ~dbd (m,from,where)
+ (n,from,where) constraints_for_dummy_type
+ in
+ MetadataConstraints.exec HSql.Library ~dbd (m,from,where)
+ @
+ MetadataConstraints.exec HSql.Legacy ~dbd (m,from,where)
let elim ~dbd uri =
let constraints =
# Distribution settings
# (i.e. settings (automatically) manipulated before a release)
DEBUG_DEFAULT="true"
-DEFAULT_DBHOST="mowgli.cs.unibo.it"
+DEFAULT_DBHOST="mysql://mowgli.cs.unibo.it"
RT_BASE_DIR_DEFAULT="`pwd`/matita"
MATITA_VERSION="0.1.0"
DISTRIBUTED="no" # "yes" for distributed tarballs
| `Xml -> return_all_uris "alluris" uris outchan
let return_ls regexp fmt outchan =
- let ls_items = Http_getter.ls regexp in
+ let ls_items = Http_getter.ls ~local:false regexp in
let buf = Buffer.create 10240 in
(match fmt with
| `Text ->
let return_resolve writable uri outchan =
try
return_xml_raw
- (sprintf "<url value=\"%s\" />\n" (Http_getter.resolve ~writable uri))
+ (sprintf "<url value=\"%s\" />\n"
+ (Http_getter.resolve ~writable ~local:false uri))
outchan
with
| Unresolvable_URI _ -> return_xml_raw "<unresolvable />\n" outchan
let uri = req#param "uri" in
let fname = Http_getter.getxml uri in (* local name, in cache *)
(* remote name *)
- let remote_name = Http_getter.resolve ~writable:false uri in
+ let remote_name =
+ Http_getter.resolve ~writable:false ~local:false uri
+ in
let src_enc = if is_gzip fname then `Gzipped else `Normal in
let enc = parse_enc req in
let fname, cleanup = convert_file ~from_enc:src_enc ~to_enc:enc fname in
flush stdout;
Unix.putenv "http_proxy" "";
let dbd () =
- HMysql.quick_connect
- ~host:(Helm_registry.get "db.host")
- ~database:(Helm_registry.get "db.database")
- ~user:(Helm_registry.get "db.user")
- ()
+ let dbspec = LibraryDb.parse_dbd_conf () in
+ HSql.quick_connect dbspec
in
restore_environment ();
read_notation ();
matitaGui.cmx: matitaprover.cmx matitamakeLib.cmx matitaTypes.cmx \
matitaScript.cmx matitaMisc.cmx matitaMathView.cmx matitaGtkMisc.cmx \
matitaGeneratedGui.cmx matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi
-matitaInit.cmo: matitamakeLib.cmi buildTimeConf.cmo matitaInit.cmi
-matitaInit.cmx: matitamakeLib.cmx buildTimeConf.cmx matitaInit.cmi
+matitaInit.cmo: matitamakeLib.cmi matitaExcPp.cmi buildTimeConf.cmo \
+ matitaInit.cmi
+matitaInit.cmx: matitamakeLib.cmx matitaExcPp.cmx buildTimeConf.cmx \
+ matitaInit.cmi
matitamakeLib.cmo: buildTimeConf.cmo matitamakeLib.cmi
matitamakeLib.cmx: buildTimeConf.cmx matitamakeLib.cmi
matitamake.cmo: matitamakeLib.cmi matitaInit.cmi matitamake.cmi
matitaGui.cmx: matitaprover.cmx matitamakeLib.cmx matitaTypes.cmx \
matitaScript.cmx matitaMisc.cmx matitaMathView.cmx matitaGtkMisc.cmx \
matitaGeneratedGui.cmx matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi
-matitaInit.cmo: matitamakeLib.cmi buildTimeConf.cmx matitaInit.cmi
-matitaInit.cmx: matitamakeLib.cmx buildTimeConf.cmx matitaInit.cmi
+matitaInit.cmo: matitamakeLib.cmi matitaExcPp.cmi buildTimeConf.cmx \
+ matitaInit.cmi
+matitaInit.cmx: matitamakeLib.cmx matitaExcPp.cmx buildTimeConf.cmx \
+ matitaInit.cmi
matitamakeLib.cmo: buildTimeConf.cmx matitamakeLib.cmi
matitamakeLib.cmx: buildTimeConf.cmx matitamakeLib.cmi
matitamake.cmo: matitamakeLib.cmi matitaInit.cmi matitamake.cmi
matitaTypes.mli \
matitaMisc.mli \
matitamakeLib.mli \
- matitaInit.mli \
matitaExcPp.mli \
+ matitaInit.mli \
matitaEngine.mli \
applyTransformation.mli \
matitacLib.mli \
matitaTypes.mli \
matitaMisc.mli \
matitamakeLib.mli \
- matitaInit.mli \
matitaExcPp.mli \
+ matitaInit.mli \
matitaEngine.mli \
applyTransformation.mli \
matitacLib.mli \
ln -fs matita $(WHERE)/$$p;\
done
$(H)cp -a library/ $(WHERE)/ma/standard-library
- $(H)cp -a contribs/ $(WHERE)/ma/
+ #$(H)cp -a contribs/ $(WHERE)/ma/
$(H)touch install_preliminaries.stamp
uninstall:
-<?xml version="1.0"?>
-<!DOCTYPE book PUBLIC "-//OASIS//DTD DocBook XML V4.1.2//EN"
-"http://www.oasis-open.org/docbook/xml/4.1.2/docbookx.dtd" [
-
- <!ENTITY legal SYSTEM "legal.xml">
- <!ENTITY license SYSTEM "sec_license.xml">
- <!ENTITY install SYSTEM "sec_install.xml">
- <!ENTITY gettingstarted SYSTEM "sec_gettingstarted.xml">
- <!ENTITY intro SYSTEM "sec_intro.xml">
- <!ENTITY terms SYSTEM "sec_terms.xml">
- <!ENTITY tacticals SYSTEM "sec_tacticals.xml">
- <!ENTITY tactics SYSTEM "sec_tactics.xml">
- <!ENTITY declarative_tactics SYSTEM "sec_declarative_tactics.xml">
- <!ENTITY othercommands SYSTEM "sec_commands.xml">
- <!ENTITY usernotation SYSTEM "sec_usernotation.xml">
-
- <!ENTITY tacticref SYSTEM "tactics_quickref.xml">
- <!ENTITY declarativetacticref SYSTEM "declarative_tactics_quickref.xml">
-
- <!ENTITY manrevision "1α">
- <!ENTITY date "12/07/2006">
- <!ENTITY app "<application>Matita</application>">
- <!ENTITY appname "Matita">
- <!ENTITY appversion SYSTEM "version.txt">
-
- <!ENTITY TODO "<emphasis>TODO</emphasis>">
- <!ENTITY MYSQL "<application> <ulink type='http'
- url='http://www.mysql.com'>MySQL</ulink> </application>">
-
- <!-- Entities for BNF -->
- <!ENTITY id "<emphasis><link linkend='grammar.id'>id</link></emphasis>">
- <!ENTITY uri "<emphasis><link linkend='grammar.uri'>uri</link></emphasis>">
- <!ENTITY char "<emphasis><link linkend='grammar.char'>char</link></emphasis>">
- <!ENTITY uri-step "<emphasis><link linkend='grammar.uri-step'>uri-step</link></emphasis>">
- <!ENTITY nat "<emphasis><link linkend='grammar.nat'>nat</link></emphasis>">
- <!ENTITY term "<emphasis><link linkend='grammar.term'>term</link></emphasis>">
- <!ENTITY rec_def "<emphasis><link linkend='grammar.rec_def'>rec_def</link></emphasis>">
- <!ENTITY match_pattern "<emphasis><link linkend='grammar.match_pattern'>match_pattern</link></emphasis>">
- <!ENTITY match_branch "<emphasis><link linkend='grammar.match_branch'>match_branch</link></emphasis>">
- <!ENTITY args "<emphasis><link linkend='grammar.args'>args</link></emphasis>">
- <!ENTITY args2 "<emphasis><link linkend='grammar.args2'>args2</link></emphasis>">
- <!ENTITY sterm "<emphasis><link linkend='grammar.sterm'>sterm</link></emphasis>">
- <!ENTITY intros-spec "<emphasis><link linkend='grammar.intros-spec'>intros-spec</link></emphasis>">
- <!ENTITY pattern "<emphasis><link linkend='grammar.pattern'>pattern</link></emphasis>">
- <!ENTITY reduction-kind "<emphasis><link linkend='grammar.reduction-kind'>reduction-kind</link></emphasis>">
- <!ENTITY path "<emphasis><link linkend='grammar.path'>path</link></emphasis>">
- <!ENTITY proofscript "<emphasis><link linkend='grammar.proofscript'>proof-script</link></emphasis>">
- <!ENTITY proofstep "<emphasis><link linkend='grammar.proofstep'>proof-step</link></emphasis>">
- <!ENTITY tactic "<emphasis><link linkend='grammar.tactic'>tactic</link></emphasis>">
- <!ENTITY LCFtactical "<emphasis><link linkend='grammar.LCFtactical'>LCF-tactical</link></emphasis>">
- <!ENTITY qstring "<emphasis><link linkend='grammar.qstring'>qstring</link></emphasis>">
- <!ENTITY interpretation "<emphasis><link linkend='grammar.interpretation'>interpretation</link></emphasis>">
- <!ENTITY autoparams "<emphasis><link linkend='grammar.autoparams'>auto_params</link></emphasis>">
+<?xml version='1.0' encoding='UTF-8'?>
+<!DOCTYPE refentry PUBLIC "-//OASIS//DTD DocBook XML V4.2//EN"
+ "http://www.oasis-open.org/docbook/xml/4.2/docbookx.dtd" [
+
+ <!ENTITY dhfirstname "<firstname>Enrico</firstname>">
+ <!ENTITY dhsurname "<surname>Tassi</surname>">
+ <!ENTITY dhdate "<date>21 Jun 2007</date>">
+ <!ENTITY dhsection "<manvolnum>1</manvolnum>">
+ <!ENTITY dhemail "<email>gareuselesinge@debian.org</email>">
+ <!ENTITY dhusername "Enrico Tassi">
+ <!ENTITY dhucpackage "<refentrytitle>matita</refentrytitle>">
+ <!ENTITY dhpackage "matita">
+
+ <!ENTITY debian "<productname>Debian</productname>">
+ <!ENTITY gnu "<acronym>GNU</acronym>">
+ <!ENTITY gpl "&gnu; <acronym>GPL</acronym>">
]>
-<?yelp:chunk-depth 3?>
-
-<book id="matita_manual" lang="en">
-
- <title>&app; V&appversion; User Manual (rev. &manrevision;)</title>
-
- <bookinfo>
-
+<refentry>
+ <refentryinfo>
+ <address>
+ &dhemail;
+ </address>
+ <author>
+ &dhfirstname;
+ &dhsurname;
+ </author>
<copyright>
- <year>2006</year>
- <holder>The HELM team.</holder>
+ <year>2007</year>
+ <holder>&dhusername;</holder>
</copyright>
+ &dhdate;
+ </refentryinfo>
+ <refmeta>
+ &dhucpackage;
+
+ &dhsection;
+ </refmeta>
+ <refnamediv>
+ <refname>&dhpackage;</refname>
+
+ <refpurpose>creates XML data file for Vim7 omni completion from
+ DTDs</refpurpose>
+ </refnamediv>
+ <refsynopsisdiv>
+ <cmdsynopsis>
+ <command>&dhpackage;</command>
+ <arg choice="req"><replaceable>filename</replaceable>.dtd</arg>
+ <arg choice="opt"><replaceable>dialectname</replaceable></arg>
+ </cmdsynopsis>
+ </refsynopsisdiv>
+
+ <refsect1>
+ <title>DESCRIPTION</title>
+
+ <para> This manual page documents brieftly the
+ <command>&dhpackage;</command> program. For more information see its HTML
+ documentation in
+ <filename>/usr/share/doc/vim-scripts/html/dtd2vim.html</filename>.
+ </para>
+
+ <para>Starting from version 7 Vim supports context aware completion of XML
+ files (and others). In particular, when the file being edited is an XML
+ file, completion can be driven by the grammar extracted from a Document
+ Type Definition (DTD). </para>
+
+ <para>For this feature to work the user should put an XML data file
+ corresponding to the desired DTD in a <filename>autoload/xml</filename>
+ directory contained in a directory belonging to Vim's
+ <varname>'runtimepath'</varname> (for example
+ <filename>~/.vim/autoload/xml/</filename>). </para>
+
+ <para><command>&dhpackage;</command> is the program that creates XML data
+ files from DTDs. Given as input a DTD
+ <filename><replaceable>file</replaceable>.dtd</filename> it will create a
+ <filename>file.vim</filename> XML data file.
+ <replaceable>dialectname</replaceable> will be part of dictionary name
+ and will be used as argument for the <command>:XMLns</command> command.
+ </para>
+
+ </refsect1>
+
+ <refsect1>
+ <title>OPTIONS</title>
+
+ <para>None. </para>
+ </refsect1>
+
+ <refsect1>
+ <title>SEE ALSO</title>
+
+ <para>vim (1).</para>
+
+ <para>In the Vim online help: <userinput>:help compl-omni</userinput>,
+ <userinput>:help ft-xml-omni</userinput>, <userinput>:help
+ :XMLns</userinput>. </para>
+
+ <para>dtd2vim is fully documented in
+ <filename>/usr/share/doc/vim-scripts/html/dtd2vim.html</filename>.
+ </para>
+ </refsect1>
+
+ <refsect1>
+ <title>AUTHOR</title>
+
+ <para>This manual page was written by &dhusername; &dhemail; for the
+ &debian; system (but may be used by others). Permission is granted to
+ copy, distribute and/or modify this document under the terms of the &gnu;
+ General Public License, Version 2 any later version published by the Free
+ Software Foundation. </para>
+
+ <para> On Debian systems, the complete text of the GNU General Public
+ License can be found in /usr/share/common-licenses/GPL. </para>
+ </refsect1>
+
+</refentry>
- <authorgroup>
- <author>
- <firstname>Andrea</firstname>
- <surname>Asperti</surname>
- <affiliation>
- <address> <email>asperti@cs.unibo.it</email> </address>
- </affiliation>
- </author>
- <author>
- <firstname>Claudio</firstname>
- <surname>Sacerdoti Coen</surname>
- <affiliation>
- <address> <email>sacerdot@cs.unibo.it</email> </address>
- </affiliation>
- </author>
- <author>
- <firstname>Ferruccio</firstname>
- <surname>Guidi</surname>
- <affiliation>
- <address> <email>fguidi@cs.unibo.it</email> </address>
- </affiliation>
- </author>
- <author>
- <firstname>Enrico</firstname>
- <surname>Tassi</surname>
- <affiliation>
- <address> <email>tassi@cs.unibo.it</email> </address>
- </affiliation>
- </author>
- <author>
- <firstname>Stefano</firstname>
- <surname>Zacchiroli</surname>
- <affiliation>
- <address> <email>zacchiro@cs.unibo.it</email> </address>
- </affiliation>
- </author>
- </authorgroup>
-
- <legalnotice>
- <para> Both &appname; and this document are free software, you can
- redistribute them and/or modify them under the terms of the GNU General
- Public License as published by the Free Software Foundation. See <xref
- linkend="sec_license" /> for more information. </para>
- </legalnotice>
-
- <revhistory>
- <revision>
- <revnumber>&manrevision;</revnumber>
- <date>&date;</date>
- </revision>
- </revhistory>
-
- </bookinfo>
-
-<!-- ============= Document Body ============================= -->
-
-&intro;
-&install;
-&gettingstarted;
-&terms;
-&usernotation;
-&tacticals;
-&tactics;
-&declarative_tactics;
-&othercommands;
-&license;
-
-</book>
-
-<!-- CSC: valid element tags
-<sect1 id="intro"> <title>Introduction</title> ...
-<sect2 id="what"> <title>What is Matita?</title>
-<para>
-<note> <title>Note:</title> <para> ...
-<footnote> <para> ...
-<itemizedlist mark="opencircle">
- <listitem>
- <para>
- The computer player for Iagno is easy to beat.
- </para>
- </listitem>
- </itemizedlist>
-
-<ulink type="http" url="http://www.gnome.org/gdp">
-<email>itp@gnu.org</email>
-<application>Matita</application>
-<command>iagno</command> on the command line
-<citetitle>Othello</citetitle>
-
-<guimenuitem>Iagno</guimenuitem>
-<guisubmenu>Games</guisubmenu>
-<guibutton>none</guibutton>
-<menuchoice> <guimenu>Settings</guimenu> <guisubmenu>Preferences </guisubmenu> </menuchoice>
-
-<xref linkend="start-shot"/>.
-<figure id="start-shot">
- <title>Starting Position</title>
- <screenshot>
- <mediaobject>
- <imageobject>
- <imagedata fileref="figures/START.png" format="PNG" srccredit="Eric Baudais"/>
- </imageobject>
- <textobject>
- <phrase>Screenshot of the starting position.</phrase>
- </textobject>
- </mediaobject>
- </screenshot>
-</figure>
-
--->
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| A.Asperti, C.Sacerdoti Coen, *)
-(* ||A|| E.Tassi, S.Zacchiroli *)
-(* \ / *)
-(* \ / Matita is distributed under the terms of the *)
-(* v GNU Lesser General Public License Version 2.1 *)
-(* *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/nat/div_and_mod".
-
-include "datatypes/constructors.ma".
-include "nat/minus.ma".
-
-let rec mod_aux t m n: nat \def
-match (leb (S m) n) with
-[ true \Rightarrow m
-| false \Rightarrow
- match t with
- [O \Rightarrow m (* if t is large enough this case never happens *)
- |(S t1) \Rightarrow mod_aux t1 (m-n) n
- ]
-].
-
-definition mod: nat \to nat \to nat \def
-\lambda m,n.mod_aux m m n.
-
-interpretation "natural remainder" 'module x y =
- (cic:/matita/nat/div_and_mod/mod.con x y).
-
-lemma O_to_mod_aux: \forall m,n. mod_aux O m n = m.
-intros.
-simplify.elim (leb (S m) n);reflexivity.
-qed.
-
-lemma lt_to_mod_aux: \forall t,m,n. m < n \to mod_aux (S t) m n = m.
-intros.
-change with
-( match (leb (S m) n) with
- [ true \Rightarrow m | false \Rightarrow mod_aux t (m-n) n] = m).
-rewrite > (le_to_leb_true ? ? H).
-reflexivity.
-qed.
-
-lemma le_to_mod_aux: \forall t,m,n. n \le m \to
-mod_aux (S t) m n = mod_aux t (m-n) n.
-intros.
-change with
-(match (leb (S m) n) with
-[ true \Rightarrow m | false \Rightarrow mod_aux t (m-n) n] = mod_aux t (m-n) n).
-apply (leb_elim (S m) n);intro
- [apply False_ind.apply (le_to_not_lt ? ? H).apply H1
- |reflexivity
- ]
-qed.
-
-let rec div_aux p m n : nat \def
-match (leb (S m) n) with
-[ true \Rightarrow O
-| false \Rightarrow
- match p with
- [O \Rightarrow O
- |(S q) \Rightarrow S (div_aux q (m-n) n)]].
-
-definition div : nat \to nat \to nat \def
-\lambda n,m.div_aux n n m.
-
-interpretation "natural divide" 'divide x y =
- (cic:/matita/nat/div_and_mod/div.con x y).
-
-theorem lt_mod_aux_m_m:
-\forall n. O < n \to \forall t,m. m \leq t \to (mod_aux t m n) < n.
-intros 3.
-elim t
- [rewrite > O_to_mod_aux.
- apply (le_n_O_elim ? H1).
- assumption
- |apply (leb_elim (S m) n);intros
- [rewrite > lt_to_mod_aux[assumption|assumption]
- |rewrite > le_to_mod_aux
- [apply H1.
- apply le_plus_to_minus.
- apply (trans_le ? ? ? H2).
- apply (lt_O_n_elim ? H).intro.
- rewrite < plus_n_Sm.
- apply le_S_S.
- apply le_plus_n_r
- |apply not_lt_to_le.
- assumption
- ]
- ]
- ]
-qed.
-
-theorem lt_mod_m_m: \forall n,m. O < m \to (n \mod m) < m.
-intros.unfold mod.
-apply lt_mod_aux_m_m[assumption|apply le_n]
-qed.
-
-lemma mod_aux_O: \forall p,n:nat. mod_aux p n O = n.
-intros.
-elim p
- [reflexivity
- |simplify.rewrite < minus_n_O.assumption
- ]
-qed.
-
-theorem div_aux_mod_aux: \forall m,p,n:nat.
-(n=(div_aux p n m)*m + (mod_aux p n m)).
-intro.
-apply (nat_case m)
- [intros.rewrite < times_n_O.simplify.apply sym_eq.apply mod_aux_O
- |intros 2.elim p
- [simplify.elim (leb n m1);reflexivity
- |simplify.apply (leb_elim n1 m1);intro
- [reflexivity
- |simplify.
- rewrite > assoc_plus.
- rewrite < (H (n1-(S m1))).
- change with (n1=(S m1)+(n1-(S m1))).
- rewrite < sym_plus.
- apply plus_minus_m_m.
- change with (m1 < n1).
- apply not_le_to_lt.exact H1.
- ]
- ]
- ]
-qed.
-
-theorem div_mod: \forall n,m:nat. O < m \to n=(n / m)*m+(n \mod m).
-intros.apply (div_aux_mod_aux m n n).
-qed.
-
-inductive div_mod_spec (n,m,q,r:nat) : Prop \def
-div_mod_spec_intro: r < m \to n=q*m+r \to (div_mod_spec n m q r).
-
-(*
-definition div_mod_spec : nat \to nat \to nat \to nat \to Prop \def
-\lambda n,m,q,r:nat.r < m \land n=q*m+r).
-*)
-
-theorem div_mod_spec_to_not_eq_O: \forall n,m,q,r.(div_mod_spec n m q r) \to m \neq O.
-intros 4.unfold Not.intros.elim H.absurd (le (S r) O)
- [rewrite < H1.assumption|exact (not_le_Sn_O r)]
-qed.
-
-theorem div_mod_spec_div_mod:
-\forall n,m. O < m \to (div_mod_spec n m (n / m) (n \mod m)).
-intros.autobatch.
-(*
-apply div_mod_spec_intro.
-apply lt_mod_m_m.assumption.
-apply div_mod.assumption.
-*)
-qed.
-
-theorem div_mod_spec_to_eq :\forall a,b,q,r,q1,r1.
-(div_mod_spec a b q r) \to (div_mod_spec a b q1 r1) \to q = q1.
-intros.elim H.elim H1.
-apply (nat_compare_elim q q1);intro
- [apply False_ind.
- cut ((q1-q)*b+r1 = r)
- [cut (b \leq (q1-q)*b+r1)
- [cut (b \leq r)
- [apply (lt_to_not_le r b H2 Hcut2)
- |elim Hcut.assumption
- ]
- |autobatch depth=4. apply (trans_le ? ((q1-q)*b))
- [apply le_times_n.
- apply le_SO_minus.exact H6
- |rewrite < sym_plus.
- apply le_plus_n
- ]
- ]
- |rewrite < sym_times.
- rewrite > distr_times_minus.
- rewrite > plus_minus
- [autobatch.
- (*
- rewrite > sym_times.
- rewrite < H5.
- rewrite < sym_times.
- apply plus_to_minus.
- apply H3
- *)
- |autobatch.
- (*
- apply le_times_r.
- apply lt_to_le.
- apply H6
- *)
- ]
- ]
-(* eq case *)
- |assumption.
-(* the following case is symmetric *)
-intro.
-apply False_ind.
-cut (eq nat ((q-q1)*b+r) r1).
-cut (b \leq (q-q1)*b+r).
-cut (b \leq r1).
-apply (lt_to_not_le r1 b H4 Hcut2).
-elim Hcut.assumption.
-apply (trans_le ? ((q-q1)*b)).
-apply le_times_n.
-apply le_SO_minus.exact H6.
-rewrite < sym_plus.
-apply le_plus_n.
-rewrite < sym_times.
-rewrite > distr_times_minus.
-rewrite > plus_minus.
-rewrite > sym_times.
-rewrite < H3.
-rewrite < sym_times.
-apply plus_to_minus.
-apply H5.
-apply le_times_r.
-apply lt_to_le.
-apply H6.
-qed.
-
-theorem div_mod_spec_to_eq2 :\forall a,b,q,r,q1,r1.
-(div_mod_spec a b q r) \to (div_mod_spec a b q1 r1) \to
-(eq nat r r1).
-intros.elim H.elim H1.
-apply (inj_plus_r (q*b)).
-rewrite < H3.
-rewrite > (div_mod_spec_to_eq a b q r q1 r1 H H1).
-assumption.
-qed.
-
-theorem div_mod_spec_times : \forall n,m:nat.div_mod_spec ((S n)*m) (S n) m O.
-intros.constructor 1.
-unfold lt.apply le_S_S.apply le_O_n.
-rewrite < plus_n_O.rewrite < sym_times.reflexivity.
-qed.
-
-(* some properties of div and mod *)
-theorem div_times: \forall n,m:nat. ((S n)*m) / (S n) = m.
-intros.
-apply (div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O).
-goal 15. (* ?11 is closed with the following tactics *)
-apply div_mod_spec_div_mod.
-unfold lt.apply le_S_S.apply le_O_n.
-apply div_mod_spec_times.
-qed.
-
-theorem div_n_n: \forall n:nat. O < n \to n / n = S O.
-intros.
-apply (div_mod_spec_to_eq n n (n / n) (n \mod n) (S O) O).
-apply div_mod_spec_div_mod.assumption.
-constructor 1.assumption.
-rewrite < plus_n_O.simplify.rewrite < plus_n_O.reflexivity.
-qed.
-
-theorem eq_div_O: \forall n,m. n < m \to n / m = O.
-intros.
-apply (div_mod_spec_to_eq n m (n/m) (n \mod m) O n).
-apply div_mod_spec_div_mod.
-apply (le_to_lt_to_lt O n m).
-apply le_O_n.assumption.
-constructor 1.assumption.reflexivity.
-qed.
-
-theorem mod_n_n: \forall n:nat. O < n \to n \mod n = O.
-intros.
-apply (div_mod_spec_to_eq2 n n (n / n) (n \mod n) (S O) O).
-apply div_mod_spec_div_mod.assumption.
-constructor 1.assumption.
-rewrite < plus_n_O.simplify.rewrite < plus_n_O.reflexivity.
-qed.
-
-theorem mod_S: \forall n,m:nat. O < m \to S (n \mod m) < m \to
-((S n) \mod m) = S (n \mod m).
-intros.
-apply (div_mod_spec_to_eq2 (S n) m ((S n) / m) ((S n) \mod m) (n / m) (S (n \mod m))).
-apply div_mod_spec_div_mod.assumption.
-constructor 1.assumption.rewrite < plus_n_Sm.
-apply eq_f.
-apply div_mod.
-assumption.
-qed.
-
-theorem mod_O_n: \forall n:nat.O \mod n = O.
-intro.elim n.simplify.reflexivity.
-simplify.reflexivity.
-qed.
-
-theorem lt_to_eq_mod:\forall n,m:nat. n < m \to n \mod m = n.
-intros.
-apply (div_mod_spec_to_eq2 n m (n/m) (n \mod m) O n).
-apply div_mod_spec_div_mod.
-apply (le_to_lt_to_lt O n m).apply le_O_n.assumption.
-constructor 1.
-assumption.reflexivity.
-qed.
-
-(* injectivity *)
-theorem injective_times_r: \forall n:nat.injective nat nat (\lambda m:nat.(S n)*m).
-change with (\forall n,p,q:nat.(S n)*p = (S n)*q \to p=q).
-intros.
-rewrite < (div_times n).
-rewrite < (div_times n q).
-apply eq_f2.assumption.
-reflexivity.
-qed.
-
-variant inj_times_r : \forall n,p,q:nat.(S n)*p = (S n)*q \to p=q \def
-injective_times_r.
-
-theorem lt_O_to_injective_times_r: \forall n:nat. O < n \to injective nat nat (\lambda m:nat.n*m).
-simplify.
-intros 4.
-apply (lt_O_n_elim n H).intros.
-apply (inj_times_r m).assumption.
-qed.
-
-variant inj_times_r1:\forall n. O < n \to \forall p,q:nat.n*p = n*q \to p=q
-\def lt_O_to_injective_times_r.
-
-theorem injective_times_l: \forall n:nat.injective nat nat (\lambda m:nat.m*(S n)).
-simplify.
-intros.
-apply (inj_times_r n x y).
-rewrite < sym_times.
-rewrite < (sym_times y).
-assumption.
-qed.
-
-variant inj_times_l : \forall n,p,q:nat. p*(S n) = q*(S n) \to p=q \def
-injective_times_l.
-
-theorem lt_O_to_injective_times_l: \forall n:nat. O < n \to injective nat nat (\lambda m:nat.m*n).
-simplify.
-intros 4.
-apply (lt_O_n_elim n H).intros.
-apply (inj_times_l m).assumption.
-qed.
-
-variant inj_times_l1:\forall n. O < n \to \forall p,q:nat.p*n = q*n \to p=q
-\def lt_O_to_injective_times_l.
-
-(* n_divides computes the pair (div,mod) *)
-
-(* p is just an upper bound, acc is an accumulator *)
-let rec n_divides_aux p n m acc \def
- match n \mod m with
- [ O \Rightarrow
- match p with
- [ O \Rightarrow pair nat nat acc n
- | (S p) \Rightarrow n_divides_aux p (n / m) m (S acc)]
- | (S a) \Rightarrow pair nat nat acc n].
-
-(* n_divides n m = <q,r> if m divides n q times, with remainder r *)
-definition n_divides \def \lambda n,m:nat.n_divides_aux n n m O.
-
-(*a simple variant of div_times theorem *)
-theorem div_times_ltO: \forall a,b:nat. O \lt b \to
-a*b/b = a.
-intros.
-rewrite > sym_times.
-rewrite > (S_pred b H).
-apply div_times.
-qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| A.Asperti, C.Sacerdoti Coen, *)
+(* ||A|| E.Tassi, S.Zacchiroli *)
+(* \ / *)
+(* \ / Matita is distributed under the terms of the *)
+(* v GNU Lesser General Public License Version 2.1 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/nat/div_and_mod_new".
+
+include "datatypes/constructors.ma".
+include "nat/minus.ma".
+
+let rec mod_aux t m n: nat \def
+match (leb (S m) n) with
+[ true \Rightarrow m
+| false \Rightarrow
+ match t with
+ [O \Rightarrow m (* if t is large enough this case never happens *)
+ |(S t1) \Rightarrow mod_aux t1 (m-n) n
+ ]
+].
+
+definition mod: nat \to nat \to nat \def
+\lambda m,n.mod_aux m m n.
+
+interpretation "natural remainder" 'module x y =
+ (cic:/matita/nat/div_and_mod_new/mod.con x y).
+
+lemma O_to_mod_aux: \forall m,n. mod_aux O m n = m.
+intros.
+simplify.elim (leb (S m) n);reflexivity.
+qed.
+
+lemma lt_to_mod_aux: \forall t,m,n. m < n \to mod_aux (S t) m n = m.
+intros.
+change with
+( match (leb (S m) n) with
+ [ true \Rightarrow m | false \Rightarrow mod_aux t (m-n) n] = m).
+rewrite > (le_to_leb_true ? ? H).
+reflexivity.
+qed.
+
+lemma le_to_mod_aux: \forall t,m,n. n \le m \to
+mod_aux (S t) m n = mod_aux t (m-n) n.
+intros.
+change with
+(match (leb (S m) n) with
+[ true \Rightarrow m | false \Rightarrow mod_aux t (m-n) n] = mod_aux t (m-n) n).
+apply (leb_elim (S m) n);intro
+ [apply False_ind.apply (le_to_not_lt ? ? H).apply H1
+ |reflexivity
+ ]
+qed.
+
+let rec div_aux p m n : nat \def
+match (leb (S m) n) with
+[ true \Rightarrow O
+| false \Rightarrow
+ match p with
+ [O \Rightarrow O
+ |(S q) \Rightarrow S (div_aux q (m-n) n)]].
+
+definition div : nat \to nat \to nat \def
+\lambda n,m.div_aux n n m.
+
+interpretation "natural divide" 'divide x y =
+ (cic:/matita/nat/div_and_mod_new/div.con x y).
+
+theorem lt_mod_aux_m_m:
+\forall n. O < n \to \forall t,m. m \leq t \to (mod_aux t m n) < n.
+intros 3.
+elim t
+ [rewrite > O_to_mod_aux.
+ apply (le_n_O_elim ? H1).
+ assumption
+ |apply (leb_elim (S m) n);intros
+ [rewrite > lt_to_mod_aux[assumption|assumption]
+ |rewrite > le_to_mod_aux
+ [apply H1.
+ apply le_plus_to_minus.
+ apply (trans_le ? ? ? H2).
+ apply (lt_O_n_elim ? H).intro.
+ rewrite < plus_n_Sm.
+ apply le_S_S.
+ apply le_plus_n_r
+ |apply not_lt_to_le.
+ assumption
+ ]
+ ]
+ ]
+qed.
+
+theorem lt_mod_m_m: \forall n,m. O < m \to (n \mod m) < m.
+intros.unfold mod.
+apply lt_mod_aux_m_m[assumption|apply le_n]
+qed.
+
+lemma mod_aux_O: \forall p,n:nat. mod_aux p n O = n.
+intros.
+elim p
+ [reflexivity
+ |simplify.rewrite < minus_n_O.assumption
+ ]
+qed.
+
+theorem div_aux_mod_aux: \forall m,p,n:nat.
+(n=(div_aux p n m)*m + (mod_aux p n m)).
+intro.
+apply (nat_case m)
+ [intros.rewrite < times_n_O.simplify.apply sym_eq.apply mod_aux_O
+ |intros 2.elim p
+ [simplify.elim (leb n m1);reflexivity
+ |simplify.apply (leb_elim n1 m1);intro
+ [reflexivity
+ |simplify.
+ rewrite > assoc_plus.
+ rewrite < (H (n1-(S m1))).
+ change with (n1=(S m1)+(n1-(S m1))).
+ rewrite < sym_plus.
+ apply plus_minus_m_m.
+ change with (m1 < n1).
+ apply not_le_to_lt.exact H1.
+ ]
+ ]
+ ]
+qed.
+
+theorem div_mod: \forall n,m:nat. O < m \to n=(n / m)*m+(n \mod m).
+intros.apply (div_aux_mod_aux m n n).
+qed.
+
+inductive div_mod_spec (n,m,q,r:nat) : Prop \def
+div_mod_spec_intro: r < m \to n=q*m+r \to (div_mod_spec n m q r).
+
+(*
+definition div_mod_spec : nat \to nat \to nat \to nat \to Prop \def
+\lambda n,m,q,r:nat.r < m \land n=q*m+r).
+*)
+
+theorem div_mod_spec_to_not_eq_O: \forall n,m,q,r.(div_mod_spec n m q r) \to m \neq O.
+intros 4.unfold Not.intros.elim H.absurd (le (S r) O)
+ [rewrite < H1.assumption|exact (not_le_Sn_O r)]
+qed.
+
+theorem div_mod_spec_div_mod:
+\forall n,m. O < m \to (div_mod_spec n m (n / m) (n \mod m)).
+intros.autobatch.
+(*
+apply div_mod_spec_intro.
+apply lt_mod_m_m.assumption.
+apply div_mod.assumption.
+*)
+qed.
+
+theorem div_mod_spec_to_eq :\forall a,b,q,r,q1,r1.
+(div_mod_spec a b q r) \to (div_mod_spec a b q1 r1) \to q = q1.
+intros.elim H.elim H1.
+apply (nat_compare_elim q q1);intro
+ [apply False_ind.
+ cut ((q1-q)*b+r1 = r)
+ [cut (b \leq (q1-q)*b+r1)
+ [cut (b \leq r)
+ [apply (lt_to_not_le r b H2 Hcut2)
+ |elim Hcut.assumption
+ ]
+ |autobatch depth=4. apply (trans_le ? ((q1-q)*b))
+ [apply le_times_n.
+ apply le_SO_minus.exact H6
+ |rewrite < sym_plus.
+ apply le_plus_n
+ ]
+ ]
+ |rewrite < sym_times.
+ rewrite > distr_times_minus.
+ rewrite > plus_minus
+ [autobatch.
+ (*
+ rewrite > sym_times.
+ rewrite < H5.
+ rewrite < sym_times.
+ apply plus_to_minus.
+ apply H3
+ *)
+ |autobatch.
+ (*
+ apply le_times_r.
+ apply lt_to_le.
+ apply H6
+ *)
+ ]
+ ]
+(* eq case *)
+ |assumption.
+(* the following case is symmetric *)
+intro.
+apply False_ind.
+cut (eq nat ((q-q1)*b+r) r1).
+cut (b \leq (q-q1)*b+r).
+cut (b \leq r1).
+apply (lt_to_not_le r1 b H4 Hcut2).
+elim Hcut.assumption.
+apply (trans_le ? ((q-q1)*b)).
+apply le_times_n.
+apply le_SO_minus.exact H6.
+rewrite < sym_plus.
+apply le_plus_n.
+rewrite < sym_times.
+rewrite > distr_times_minus.
+rewrite > plus_minus.
+rewrite > sym_times.
+rewrite < H3.
+rewrite < sym_times.
+apply plus_to_minus.
+apply H5.
+apply le_times_r.
+apply lt_to_le.
+apply H6.
+qed.
+
+theorem div_mod_spec_to_eq2 :\forall a,b,q,r,q1,r1.
+(div_mod_spec a b q r) \to (div_mod_spec a b q1 r1) \to
+(eq nat r r1).
+intros.elim H.elim H1.
+apply (inj_plus_r (q*b)).
+rewrite < H3.
+rewrite > (div_mod_spec_to_eq a b q r q1 r1 H H1).
+assumption.
+qed.
+
+theorem div_mod_spec_times : \forall n,m:nat.div_mod_spec ((S n)*m) (S n) m O.
+intros.constructor 1.
+unfold lt.apply le_S_S.apply le_O_n.
+rewrite < plus_n_O.rewrite < sym_times.reflexivity.
+qed.
+
+(* some properties of div and mod *)
+theorem div_times: \forall n,m:nat. ((S n)*m) / (S n) = m.
+intros.
+apply (div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O).
+goal 15. (* ?11 is closed with the following tactics *)
+apply div_mod_spec_div_mod.
+unfold lt.apply le_S_S.apply le_O_n.
+apply div_mod_spec_times.
+qed.
+
+theorem div_n_n: \forall n:nat. O < n \to n / n = S O.
+intros.
+apply (div_mod_spec_to_eq n n (n / n) (n \mod n) (S O) O).
+apply div_mod_spec_div_mod.assumption.
+constructor 1.assumption.
+rewrite < plus_n_O.simplify.rewrite < plus_n_O.reflexivity.
+qed.
+
+theorem eq_div_O: \forall n,m. n < m \to n / m = O.
+intros.
+apply (div_mod_spec_to_eq n m (n/m) (n \mod m) O n).
+apply div_mod_spec_div_mod.
+apply (le_to_lt_to_lt O n m).
+apply le_O_n.assumption.
+constructor 1.assumption.reflexivity.
+qed.
+
+theorem mod_n_n: \forall n:nat. O < n \to n \mod n = O.
+intros.
+apply (div_mod_spec_to_eq2 n n (n / n) (n \mod n) (S O) O).
+apply div_mod_spec_div_mod.assumption.
+constructor 1.assumption.
+rewrite < plus_n_O.simplify.rewrite < plus_n_O.reflexivity.
+qed.
+
+theorem mod_S: \forall n,m:nat. O < m \to S (n \mod m) < m \to
+((S n) \mod m) = S (n \mod m).
+intros.
+apply (div_mod_spec_to_eq2 (S n) m ((S n) / m) ((S n) \mod m) (n / m) (S (n \mod m))).
+apply div_mod_spec_div_mod.assumption.
+constructor 1.assumption.rewrite < plus_n_Sm.
+apply eq_f.
+apply div_mod.
+assumption.
+qed.
+
+theorem mod_O_n: \forall n:nat.O \mod n = O.
+intro.elim n.simplify.reflexivity.
+simplify.reflexivity.
+qed.
+
+theorem lt_to_eq_mod:\forall n,m:nat. n < m \to n \mod m = n.
+intros.
+apply (div_mod_spec_to_eq2 n m (n/m) (n \mod m) O n).
+apply div_mod_spec_div_mod.
+apply (le_to_lt_to_lt O n m).apply le_O_n.assumption.
+constructor 1.
+assumption.reflexivity.
+qed.
+
+(* injectivity *)
+theorem injective_times_r: \forall n:nat.injective nat nat (\lambda m:nat.(S n)*m).
+change with (\forall n,p,q:nat.(S n)*p = (S n)*q \to p=q).
+intros.
+rewrite < (div_times n).
+rewrite < (div_times n q).
+apply eq_f2.assumption.
+reflexivity.
+qed.
+
+variant inj_times_r : \forall n,p,q:nat.(S n)*p = (S n)*q \to p=q \def
+injective_times_r.
+
+theorem lt_O_to_injective_times_r: \forall n:nat. O < n \to injective nat nat (\lambda m:nat.n*m).
+simplify.
+intros 4.
+apply (lt_O_n_elim n H).intros.
+apply (inj_times_r m).assumption.
+qed.
+
+variant inj_times_r1:\forall n. O < n \to \forall p,q:nat.n*p = n*q \to p=q
+\def lt_O_to_injective_times_r.
+
+theorem injective_times_l: \forall n:nat.injective nat nat (\lambda m:nat.m*(S n)).
+simplify.
+intros.
+apply (inj_times_r n x y).
+rewrite < sym_times.
+rewrite < (sym_times y).
+assumption.
+qed.
+
+variant inj_times_l : \forall n,p,q:nat. p*(S n) = q*(S n) \to p=q \def
+injective_times_l.
+
+theorem lt_O_to_injective_times_l: \forall n:nat. O < n \to injective nat nat (\lambda m:nat.m*n).
+simplify.
+intros 4.
+apply (lt_O_n_elim n H).intros.
+apply (inj_times_l m).assumption.
+qed.
+
+variant inj_times_l1:\forall n. O < n \to \forall p,q:nat.p*n = q*n \to p=q
+\def lt_O_to_injective_times_l.
+
+(* n_divides computes the pair (div,mod) *)
+
+(* p is just an upper bound, acc is an accumulator *)
+let rec n_divides_aux p n m acc \def
+ match n \mod m with
+ [ O \Rightarrow
+ match p with
+ [ O \Rightarrow pair nat nat acc n
+ | (S p) \Rightarrow n_divides_aux p (n / m) m (S acc)]
+ | (S a) \Rightarrow pair nat nat acc n].
+
+(* n_divides n m = <q,r> if m divides n q times, with remainder r *)
+definition n_divides \def \lambda n,m:nat.n_divides_aux n n m O.
<!-- <key name="font_size">10</key> -->
</section>
<section name="db">
- <!-- Access parameter to the (MySql) metadata database. They are not
- needed if Matita is always run with -nodb, but this is _not_
- recommended since a lot of features wont work.
- Hint. The simplest way to create a database is:
+ <!--
+ Every metadata key must have the following fields:
+ 1) dbhost: a file:// or a mysql:// path
+ 2) database name: use extension .db for file:// dbs
+ 3) username
+ 4) password: use 'none' for no password
+ 5) dbtype: one of the following
+ 'legacy'
+ are read only dbs, used for the Coq/contribs stuff
+ 'library'
+ is the standard library, becames writable in publish (-system)
+ mode
+ 'user'
+ is the user own db (can be the same of marked as ro, tables
+ have different names and can coexist)
+
+ Note that:
+ exactly one 'user' db must be specified
+ exactly one 'library' db must be specified
+ exactly one 'legacy' db can be specified
+ -->
+
+ <!-- this snippet is what is used by the helm team, everything on mowgli.
+ note that user's tables are named diffrently from library tables, so that
+ they can coexists on the same db -->
+ <key name="metadata">@DBHOST@ matita helm none library</key>
+ <key name="metadata">@DBHOST@ matita helm none user</key>
+
+ <!-- The following snippet it what you want to use a local sqlite db
+ and acess remotely to the coq library trought mowgli
+ <key name="metadata">@DBHOST@ matita helm none legacy</key>
+ <key name="metadata">file://$(matita.rt_base_dir) metadata.db helm helm library</key>
+ <key name="metadata">file://$(matita.basedir) user.db helm helm user</key>
+ -->
+
+ <!--
+ If you have a large amount of metadata, you may be interested in using
+ MySql instead of Sqlite. The simplest way to create a MySql database is:
0) # become an user with database administration privileges
1) mysqladmin create matita
2) echo "grant all privileges on matita.* to helm;" | mysql matita
Note that this way the database will be open to anyone, apply
stricter permissions if needed.
-->
- <key name="host">@DBHOST@</key>
- <key name="user">helm</key>
- <key name="database">matita</key>
</section>
<section name="getter">
<!-- Cache dir for CIC XML documents downloaded from the net.
file:///projects/helm/library/coq_contribs/
legacy
</key>
+ <key name="prefix">
+ cic:/
+ http://mowgli.cs.unibo.it/xml/
+ legacy
+ </key>
</section>
</helm_registry>
LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri
~writable:true in
let save () =
- let metadata_fname =
- LibraryMisc.metadata_file_of_baseuri
- ~must_exist:false ~baseuri ~writable:true in
let lexicon_fname =
LibraryMisc.lexicon_file_of_baseuri
~must_exist:false ~baseuri ~writable:true
in
GrafiteMarshal.save_moo moo_fname
grafite_status.GrafiteTypes.moo_content_rev;
- LibraryNoDb.save_metadata metadata_fname
- lexicon_status.LexiconEngine.metadata;
LexiconMarshal.save_lexicon lexicon_fname
lexicon_status.LexiconEngine.lexicon_content_rev
in
let conffile = ref BuildTimeConf.matita_conf
let registry_defaults = [
- "db.nodb", "false";
"matita.debug", "false";
"matita.external_editor", "gvim -f -c 'go %p' %f";
"matita.preserve", "false";
let login = (Unix.getpwuid (Unix.getuid ())).Unix.pw_name in
Helm_registry.set "user.name" login
end;
+ let home = Helm_registry.get_string "matita.basedir" in
+ let user_conf_file = home ^ "/matita.conf.xml" in
+ if HExtlib.is_regular user_conf_file then
+ begin
+ HLog.message ("Loading additional conf file from " ^ user_conf_file);
+ try
+ Helm_registry.load_from user_conf_file
+ with exn ->
+ HLog.error
+ ("While loading conf file: " ^ snd (MatitaExcPp.to_string exn))
+ end;
ConfigurationFile::init_status
end
else
"-force",
Arg.Unit (fun () -> Helm_registry.set_bool "matita.force" true),
("Force actions that would not be executed per default");
- "-nodb", Arg.Unit (fun () -> Helm_registry.set_bool "db.nodb" true),
- ("Avoid using external database connection"
- ^ "\n WARNING: disable many features");
"-noprofile",
Arg.Unit (fun () -> Helm_registry.set_bool "matita.profile" false),
"Turns off profiling printings";
self#_loadObj obj
method private _loadDir dir =
- let content = Http_getter.ls dir in
+ let content = Http_getter.ls ~local:false dir in
let l =
List.fast_sort
Pervasives.compare
| TA.Command (_,TA.Set (_,"baseuri",u)) ->
if Http_getter_storage.is_read_only u then
raise (ActionCancelled ("baseuri " ^ u ^ " is readonly"));
- if not (Http_getter_storage.is_empty u) then
+ if not (Http_getter_storage.is_empty ~local:true u) then
(match
guistuff.ask_confirmation
~title:"Baseuri redefinition"
| End_of_file -> ()
| GrafiteEngine.Drop -> clean_exit 1
);
- let proof_status,moo_content_rev,metadata,lexicon_content_rev =
+ let proof_status,moo_content_rev,lexicon_content_rev =
match !lexicon_status,!grafite_status with
| ss::_, s::_ ->
- s.proof_status, s.moo_content_rev, ss.LexiconEngine.metadata,
+ s.proof_status, s.moo_content_rev,
ss.LexiconEngine.lexicon_content_rev
| _,_ -> assert false
in
LibraryMisc.lexicon_file_of_baseuri
~must_exist:false ~baseuri ~writable:true
in
- let metadata_fname =
- LibraryMisc.metadata_file_of_baseuri
- ~must_exist:false ~baseuri ~writable:true
- in
GrafiteMarshal.save_moo moo_fname moo_content_rev;
- LibraryNoDb.save_metadata metadata_fname metadata;
LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
exit 0
end
let hou =
if tm.Unix.tm_hour > 0 then (string_of_int tm.Unix.tm_hour ^ "h ") else ""
in
- let proof_status,moo_content_rev,metadata,lexicon_content_rev =
+ let proof_status,moo_content_rev,lexicon_content_rev =
match !lexicon_status,!grafite_status with
| Some ss, Some s ->
- s.proof_status, s.moo_content_rev, ss.LexiconEngine.metadata,
+ s.proof_status, s.moo_content_rev,
ss.LexiconEngine.lexicon_content_rev
| _,_ -> assert false
in
LibraryMisc.lexicon_file_of_baseuri
~must_exist:false ~baseuri ~writable:true
in
- let metadata_fname =
- LibraryMisc.metadata_file_of_baseuri
- ~must_exist:false ~baseuri ~writable:true
- in
GrafiteMarshal.save_moo moo_fname moo_content_rev;
- LibraryNoDb.save_metadata metadata_fname metadata;
LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
HLog.message
(sprintf "execution of %s completed in %s." fname (hou^min^sec));
let obj_file_of_baseuri writable baseuri =
try
LibraryMisc.obj_file_of_baseuri
- ~must_exist:true ~baseuri ~writable
+ ~must_exist:true ~baseuri ~writable
with
| Http_getter_types.Unresolvable_URI _
| Http_getter_types.Key_not_found _ ->
LibraryMisc.obj_file_of_baseuri
- ~must_exist:false ~baseuri ~writable:true
+ ~must_exist:false ~baseuri ~writable:true
;;
let main () =
let csc = try ["SRC=" ^ Sys.getenv "SRC"] with Not_found -> [] in
rebuild_makefile development;
let makefile = makefile_for_development development in
- let nodb =
- Helm_registry.get_opt_default Helm_registry.bool ~default:false "db.nodb"
- in
let flags = [] in
- let flags = flags @ if nodb then ["NODB=true"] else [] in
let flags =
try
flags @ [ sprintf "MATITA_FLAGS=\"%s\"" matita_flags ]
"Timeout in seconds"];
MatitaInit.parse_cmdline ();
MatitaInit.load_configuration_file ();
- Helm_registry.set_bool "db.nodb" true;
Helm_registry.set_bool "matita.nodisk" true;
HLog.set_log_callback (fun _ _ -> ());
let args = Helm_registry.get_list Helm_registry.string "matita.args" in
--- /dev/null
+#!/bin/sh
+
+TBL=`echo show tables | mysql matita -u helm | grep -v _`
+for X in $TBL; do
+ echo cleaning $X
+ echo "delete from $X where source like 'cic:/matita/%'" | mysql matita -u helm
+done
projects / helm.git / commitdiff