From: Enrico Tassi Date: Fri, 6 Jul 2007 14:49:47 +0000 (+0000) Subject: maxipatch for support of multiple DBs. X-Git-Tag: make_still_working~6214 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=111df95ac03f2ee21dfa2422a7f531f675b1c16d;p=helm.git maxipatch for support of multiple DBs. new 3 different kind of BD can coexist: user) the user db, where his stuff is stored tables are named foo_user library) the library db, a read only database where the standard library should be installed and that is the target of the publish act legacy) a legacy database (not mandatory) where really read only data is stored every db can be implement with an sqlite file or a mysql database. the default configuration file sets 1 and 2 to be the mysql matita database on mowgli, thus nothing should change for mowgli users. database 3 is not used if you are on mowgli. the way it should be used by matita users out of the unibo network is commented in the config file: 1) file://~/.matita/user.db for his development 2) file:///usr/share/matita/metadata.db for the matita precompiled standard library 3) mysql://mowgli.cs.unibo.it for the legacy coq stuff, both queries and xml are fetched trough the net this allows us to really distribute matita in a rather sane way, with a precompiled library visible systemwide and having all per user data and metadata in ~/.matita. There is no need for the user to install and configure mysql, and can use mowgli just decommenting few lines in the config file. --- diff --git a/helm/software/components/binaries/extractor/Makefile b/helm/software/components/binaries/extractor/Makefile index eae5c635d..323f405d4 100644 --- a/helm/software/components/binaries/extractor/Makefile +++ b/helm/software/components/binaries/extractor/Makefile @@ -11,22 +11,22 @@ clean: 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 \ diff --git a/helm/software/components/binaries/extractor/extractor.conf.xml b/helm/software/components/binaries/extractor/extractor.conf.xml index 8dbc9a935..d82b16028 100644 --- a/helm/software/components/binaries/extractor/extractor.conf.xml +++ b/helm/software/components/binaries/extractor/extractor.conf.xml @@ -4,9 +4,8 @@ .tmp/
- localhost - helm - mowgli + mysql://mowgli.cs.unibo.it mowgli helm helm library + file:///tmp/ user.db helm helm user
diff --git a/helm/software/components/binaries/extractor/extractor.ml b/helm/software/components/binaries/extractor/extractor.ml index 832fc0cb3..981900c3c 100644 --- a/helm/software/components/binaries/extractor/extractor.ml +++ b/helm/software/components/binaries/extractor/extractor.ml @@ -29,14 +29,11 @@ let path = Sys.argv.(1) 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 diff --git a/helm/software/components/binaries/extractor/extractor_manager.ml b/helm/software/components/binaries/extractor/extractor_manager.ml index 05393b63e..13e92777f 100644 --- a/helm/software/components/binaries/extractor/extractor_manager.ml +++ b/helm/software/components/binaries/extractor/extractor_manager.ml @@ -36,18 +36,18 @@ let create_all dbd = (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 = @@ -61,15 +61,16 @@ 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 @@ -182,12 +183,8 @@ let main () = 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; @@ -258,7 +255,7 @@ let main () = (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); @@ -284,22 +281,14 @@ let main () = 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 ;; diff --git a/helm/software/components/binaries/table_creator/table_creator.ml b/helm/software/components/binaries/table_creator/table_creator.ml index 423edfb27..c735fe67f 100644 --- a/helm/software/components/binaries/table_creator/table_creator.ml +++ b/helm/software/components/binaries/table_creator/table_creator.ml @@ -50,10 +50,14 @@ let main () = 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 diff --git a/helm/software/components/cic/.depend b/helm/software/components/cic/.depend index a1a32d457..538d4b10d 100644 --- a/helm/software/components/cic/.depend +++ b/helm/software/components/cic/.depend @@ -3,6 +3,7 @@ deannotate.cmi: cic.cmo 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 @@ -20,8 +21,8 @@ cicUtil.cmo: cicUniv.cmi cic.cmo cicUtil.cmi 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 diff --git a/helm/software/components/cic/cicUtil.ml b/helm/software/components/cic/cicUtil.ml index 22dcb298c..d26d422d5 100644 --- a/helm/software/components/cic/cicUtil.ml +++ b/helm/software/components/cic/cicUtil.ml @@ -541,7 +541,7 @@ let alpha_equivalence = | 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 diff --git a/helm/software/components/cic_proof_checking/cicEnvironment.ml b/helm/software/components/cic_proof_checking/cicEnvironment.ml index e64370bf1..8ae5c1b13 100644 --- a/helm/software/components/cic_proof_checking/cicEnvironment.ml +++ b/helm/software/components/cic_proof_checking/cicEnvironment.ml @@ -366,7 +366,7 @@ let get_object_to_add uri = 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 @@ -527,7 +527,7 @@ let in_cache uri = 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 diff --git a/helm/software/components/getter/http_getter.ml b/helm/software/components/getter/http_getter.ml index 3f5cb2e5c..b41c4788f 100644 --- a/helm/software/components/getter/http_getter.ml +++ b/helm/software/components/getter/http_getter.ml @@ -132,9 +132,9 @@ let resolve_remote ~writable uri = | 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 @@ -143,53 +143,53 @@ let deref_index_theory 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 @@ -256,7 +256,7 @@ let collect_ls_items dirs_set objs_tbl = 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 @@ -269,7 +269,7 @@ let rec dumb_ls uri_prefix = 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 @@ -291,12 +291,12 @@ let rec dumb_ls uri_prefix = 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 _ -> ()); @@ -304,9 +304,9 @@ let rec dumb_ls uri_prefix = 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 @@ -337,12 +337,12 @@ let merge_results results = 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 @@ -355,7 +355,7 @@ let getalluris () = | 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 @@ -364,9 +364,13 @@ let getalluris () = (* 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 diff --git a/helm/software/components/getter/http_getter.mli b/helm/software/components/getter/http_getter.mli index 845a17a10..5cf5cd38e 100644 --- a/helm/software/components/getter/http_getter.mli +++ b/helm/software/components/getter/http_getter.mli @@ -40,13 +40,13 @@ val help: unit -> string (** @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 @@ -56,14 +56,14 @@ val getalluris: unit -> string list (** @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} *) diff --git a/helm/software/components/getter/http_getter_storage.ml b/helm/software/components/getter/http_getter_storage.ml index 77bfe138d..c17435f6a 100644 --- a/helm/software/components/getter/http_getter_storage.ml +++ b/helm/software/components/getter/http_getter_storage.ml @@ -100,25 +100,45 @@ let prefix_map_ref = ref (lazy ( 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 ] @@ -154,11 +174,14 @@ let ls_file_single _ path_prefix = 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 @@ -168,7 +191,8 @@ let get_file _ path = 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 @@ -204,31 +228,31 @@ let remove_http _ _ = (**************************** 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 @@ -251,6 +275,7 @@ type 'a storage_method = { name: string; write: bool; exists: bool; + local: bool; file: string -> string -> 'a; (* unresolved uri, resolved uri *) http: string -> string -> 'a; (* unresolved uri, resolved uri *) } @@ -268,11 +293,17 @@ let invoke_method storage_method uri url = 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 -> @@ -283,21 +314,25 @@ let dispatch_multi storage_method uri = 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 @@ -305,31 +340,35 @@ let resolve ?(must_exists=true) ~writable = { 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 @@ -355,23 +394,25 @@ let list_writable_prefixes _ = 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 diff --git a/helm/software/components/getter/http_getter_storage.mli b/helm/software/components/getter/http_getter_storage.mli index 04af29f0c..cc0ff46c4 100644 --- a/helm/software/components/getter/http_getter_storage.mli +++ b/helm/software/components/getter/http_getter_storage.mli @@ -43,7 +43,7 @@ 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 @@ -53,20 +53,21 @@ val ls: string -> string list * 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 diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index ad4ae40c6..a31f3990e 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -728,20 +728,21 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status 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,[] @@ -762,7 +763,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status | 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 diff --git a/helm/software/components/hmysql/.depend b/helm/software/components/hmysql/.depend index d0d29cbd2..16e6e9da7 100644 --- a/helm/software/components/hmysql/.depend +++ b/helm/software/components/hmysql/.depend @@ -1,2 +1,2 @@ -hSql.cmo: hSql.cmi -hSql.cmx: hSql.cmi +hSql.cmo: hSqlite3.cmo hMysql.cmo hSql.cmi +hSql.cmx: hSqlite3.cmx hMysql.cmx hSql.cmi diff --git a/helm/software/components/hmysql/Makefile b/helm/software/components/hmysql/Makefile index 7474507e3..356e6e068 100644 --- a/helm/software/components/hmysql/Makefile +++ b/helm/software/components/hmysql/Makefile @@ -4,6 +4,8 @@ PREDICATES = INTERFACE_FILES = \ hSql.mli IMPLEMENTATION_FILES = \ + hSqlite3.ml \ + hMysql.ml \ $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = diff --git a/helm/software/components/hmysql/hMysql.ml b/helm/software/components/hmysql/hMysql.ml index 374ccc600..b9ace8e83 100644 --- a/helm/software/components/hmysql/hMysql.ml +++ b/helm/software/components/hmysql/hMysql.ml @@ -39,18 +39,12 @@ exception Error of string 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 -> () @@ -59,7 +53,7 @@ let disconnect = function let escape s = profiler.HExtlib.profile Mysql.escape s -let exec dbd s = +let exec s dbd = match dbd with | None -> None | Some dbd -> diff --git a/helm/software/components/hmysql/hSql.ml b/helm/software/components/hmysql/hSql.ml deleted file mode 120000 index 3230ae532..000000000 --- a/helm/software/components/hmysql/hSql.ml +++ /dev/null @@ -1 +0,0 @@ -hMysql.ml \ No newline at end of file diff --git a/helm/software/components/hmysql/hSql.ml b/helm/software/components/hmysql/hSql.ml new file mode 100644 index 000000000..329dd2205 --- /dev/null +++ b/helm/software/components/hmysql/hSql.ml @@ -0,0 +1,175 @@ +(* 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] +;; diff --git a/helm/software/components/hmysql/hSql.mli b/helm/software/components/hmysql/hSql.mli index fb678fa59..6cfc88655 100644 --- a/helm/software/components/hmysql/hSql.mli +++ b/helm/software/components/hmysql/hSql.mli @@ -23,16 +23,6 @@ * 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 = @@ -43,27 +33,38 @@ 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 diff --git a/helm/software/components/hmysql/hSqlite3.ml b/helm/software/components/hmysql/hSqlite3.ml index 20e494511..3693e445b 100644 --- a/helm/software/components/hmysql/hSqlite3.ml +++ b/helm/software/components/hmysql/hSqlite3.ml @@ -47,36 +47,35 @@ let prerr_endline s = ()(*HLog.debug s;;*) 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 @@ -137,7 +136,7 @@ let string_of_rc = function 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 = diff --git a/helm/software/components/lexicon/lexiconEngine.ml b/helm/software/components/lexicon/lexiconEngine.ml index a0792d228..1966251ad 100644 --- a/helm/software/components/lexicon/lexiconEngine.ml +++ b/helm/software/components/lexicon/lexiconEngine.ml @@ -38,7 +38,6 @@ type 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; } let initial_status = { @@ -46,7 +45,6 @@ let initial_status = { multi_aliases = DisambiguateTypes.Environment.empty; lexicon_content_rev = []; notation_ids = []; - metadata = []; } let add_lexicon_content cmds status = @@ -60,23 +58,6 @@ 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 @@ -85,14 +66,6 @@ let set_proof_aliases mode status new_aliases = 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 @@ -111,7 +84,6 @@ let set_proof_aliases mode status new_aliases = let status = add_lexicon_content (commands_of_aliases aliases) new_status in - let status = add_metadata (deps_of_aliases aliases) status in status @@ -135,21 +107,7 @@ let rec eval_command ?(mode=LexiconAst.WithPreferences) status cmd = 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 @@ -168,17 +126,11 @@ let rec eval_command ?(mode=LexiconAst.WithPreferences) status cmd = 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 diff --git a/helm/software/components/lexicon/lexiconEngine.mli b/helm/software/components/lexicon/lexiconEngine.mli index eab7e53e7..b69495f4e 100644 --- a/helm/software/components/lexicon/lexiconEngine.mli +++ b/helm/software/components/lexicon/lexiconEngine.mli @@ -30,7 +30,6 @@ type 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 diff --git a/helm/software/components/library/.depend b/helm/software/components/library/.depend index 5f391bc0f..e99436e05 100644 --- a/helm/software/components/library/.depend +++ b/helm/software/components/library/.depend @@ -1,4 +1,4 @@ -cicCoercion.cmi: refinementTool.cmo coercDb.cmi +cicCoercion.cmi: coercDb.cmi librarySync.cmi: refinementTool.cmo cicElim.cmo: cicElim.cmi cicElim.cmx: cicElim.cmi @@ -10,15 +10,13 @@ libraryDb.cmo: libraryDb.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 diff --git a/helm/software/components/library/.depend.opt b/helm/software/components/library/.depend.opt index eacb26990..190aaf9b7 100644 --- a/helm/software/components/library/.depend.opt +++ b/helm/software/components/library/.depend.opt @@ -1,4 +1,4 @@ -cicCoercion.cmi: refinementTool.cmx coercDb.cmi +cicCoercion.cmi: coercDb.cmi librarySync.cmi: refinementTool.cmx cicElim.cmo: cicElim.cmi cicElim.cmx: cicElim.cmi @@ -10,15 +10,13 @@ libraryDb.cmo: libraryDb.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 diff --git a/helm/software/components/library/Makefile b/helm/software/components/library/Makefile index 013f5f4a0..a484846a9 100644 --- a/helm/software/components/library/Makefile +++ b/helm/software/components/library/Makefile @@ -9,7 +9,6 @@ INTERFACE_FILES = \ coercDb.mli \ cicCoercion.mli \ librarySync.mli \ - libraryNoDb.mli \ libraryClean.mli \ $(NULL) IMPLEMENTATION_FILES = \ diff --git a/helm/software/components/library/libraryClean.ml b/helm/software/components/library/libraryClean.ml index 1b378e6c2..e137c1873 100644 --- a/helm/software/components/library/libraryClean.ml +++ b/helm/software/components/library/libraryClean.ml @@ -36,7 +36,7 @@ module UM = UriManager;; 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) @@ -49,9 +49,9 @@ let one_step_depend 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 @@ -67,7 +67,7 @@ let one_step_depend suri = 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 -> @@ -88,11 +88,15 @@ let safe_buri_of_suri suri = 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 @@ -109,7 +113,7 @@ let db_uris_of_baseuri buri = 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 -> @@ -124,6 +128,10 @@ let db_uris_of_baseuri buri = ;; 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 @@ -143,7 +151,7 @@ let close_uri_list uri_to_remove = 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 @@ -171,7 +179,7 @@ let close_uri_list uri_to_remove = (* 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) @@ -201,63 +209,17 @@ let moo_root_dir = lazy ( 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:"; @@ -270,9 +232,6 @@ let clean_baseuris ?(verbose=true) buris = 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) ; @@ -294,15 +253,15 @@ let clean_baseuris ?(verbose=true) buris = 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()] diff --git a/helm/software/components/library/libraryDb.ml b/helm/software/components/library/libraryDb.ml index e6af1eb81..9e5a13bdb 100644 --- a/helm/software/components/library/libraryDb.ml +++ b/helm/software/components/library/libraryDb.ml @@ -27,16 +27,36 @@ 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://" @@ -52,14 +72,18 @@ let clean_owner_environment () = (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 @@ -70,15 +94,15 @@ let clean_owner_environment () = (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; () @@ -106,28 +130,28 @@ let create_owner_environment () = (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 @@ -147,14 +171,20 @@ let remove_uri uri = 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 *) ) @@ -164,15 +194,19 @@ let remove_uri uri = 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 diff --git a/helm/software/components/library/libraryDb.mli b/helm/software/components/library/libraryDb.mli index ce653795a..d279f15ee 100644 --- a/helm/software/components/library/libraryDb.mli +++ b/helm/software/components/library/libraryDb.mli @@ -24,6 +24,7 @@ *) val instance: unit -> HSql.dbd +val parse_dbd_conf: unit -> HSql.dbspec val create_owner_environment: unit -> unit val clean_owner_environment: unit -> unit diff --git a/helm/software/components/library/libraryMisc.ml b/helm/software/components/library/libraryMisc.ml index e971c52d4..7c82e27c4 100644 --- a/helm/software/components/library/libraryMisc.ml +++ b/helm/software/components/library/libraryMisc.ml @@ -25,16 +25,14 @@ (* $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" diff --git a/helm/software/components/library/libraryMisc.mli b/helm/software/components/library/libraryMisc.mli index d834dbd1a..2c6bfd193 100644 --- a/helm/software/components/library/libraryMisc.mli +++ b/helm/software/components/library/libraryMisc.mli @@ -23,9 +23,8 @@ * 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 diff --git a/helm/software/components/library/libraryNoDb.ml b/helm/software/components/library/libraryNoDb.ml deleted file mode 100644 index 9ac42a5ea..000000000 --- a/helm/software/components/library/libraryNoDb.ml +++ /dev/null @@ -1,51 +0,0 @@ -(* 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 - diff --git a/helm/software/components/library/libraryNoDb.mli b/helm/software/components/library/libraryNoDb.mli deleted file mode 100644 index 1521f456f..000000000 --- a/helm/software/components/library/libraryNoDb.mli +++ /dev/null @@ -1,35 +0,0 @@ -(* 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 - diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml index 8ecabbbb6..1e60133a7 100644 --- a/helm/software/components/library/librarySync.ml +++ b/helm/software/components/library/librarySync.ml @@ -44,7 +44,7 @@ let uris_of_obj uri = 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 @@ -164,7 +164,7 @@ let remove_single_obj uri = 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 _ -> ()); diff --git a/helm/software/components/metadata/metadataConstraints.ml b/helm/software/components/metadata/metadataConstraints.ml index c2dee6f5e..a4267c5fc 100644 --- a/helm/software/components/metadata/metadataConstraints.ml +++ b/helm/software/components/metadata/metadataConstraints.ml @@ -153,7 +153,7 @@ let add_constraint ?(start=0) ?(tables=default_tables) (n,from,where) metadata = 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 = @@ -166,12 +166,14 @@ let exec ~(dbd:HSql.dbd) ?rating (n,from,where) = 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 @@ -187,7 +189,7 @@ let at_least ~(dbd:HSql.dbd) ?concl_card ?full_card ?diff ?rating tables 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 @@ -195,13 +197,26 @@ 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 *) @@ -447,24 +462,30 @@ let get_constants (dbd:HSql.dbd) ~where uri = [ 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 = diff --git a/helm/software/components/metadata/metadataConstraints.mli b/helm/software/components/metadata/metadataConstraints.mli index a76c1fed7..bc83f65d7 100644 --- a/helm/software/components/metadata/metadataConstraints.mli +++ b/helm/software/components/metadata/metadataConstraints.mli @@ -101,6 +101,7 @@ val add_all_constr: int * string list * string list val exec: + HSql.dbtype -> dbd:HSql.dbd -> ?rating:[ `Hits ] -> int * string list * string list -> diff --git a/helm/software/components/metadata/metadataDb.ml b/helm/software/components/metadata/metadataDb.ml index 7678cd0b3..844a08347 100644 --- a/helm/software/components/metadata/metadataDb.ml +++ b/helm/software/components/metadata/metadataDb.ml @@ -29,8 +29,8 @@ open MetadataTypes 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 -> @@ -60,26 +60,29 @@ let execute_insert dbd uri (sort_cols, rel_cols, obj_cols) = | _ -> 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 @@ -116,21 +119,27 @@ let insert_const_no ~dbd l = (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 @@ -143,11 +152,11 @@ let analyze_index = ref 0 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 @@ -171,7 +180,7 @@ let tables_to_clean = 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 @@ -181,16 +190,16 @@ let clean ~(dbd:HSql.dbd) = 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; @@ -200,15 +209,16 @@ let unindex ~dbd ~uri = 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 diff --git a/helm/software/components/metadata/metadataDeps.ml b/helm/software/components/metadata/metadataDeps.ml index 13e1d23b4..d34bd1c83 100644 --- a/helm/software/components/metadata/metadataDeps.ml +++ b/helm/software/components/metadata/metadataDeps.ml @@ -64,14 +64,17 @@ let direct_deps ~dbd uri = 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 = @@ -82,14 +85,17 @@ let inverse_deps ~dbd uri = 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 = @@ -105,21 +111,26 @@ let sorted_uris_of_baseuri ~dbd baseuri = 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 = diff --git a/helm/software/components/metadata/sqlStatements.ml b/helm/software/components/metadata/sqlStatements.ml index 5ba5429b7..2164f5724 100644 --- a/helm/software/components/metadata/sqlStatements.ml +++ b/helm/software/components/metadata/sqlStatements.ml @@ -110,29 +110,30 @@ sprintf "CREATE INDEX %s_statement ON %s (statement);" name name] 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 @@ -168,14 +169,14 @@ let get_table_drop t named = | `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 @@ -186,8 +187,8 @@ let create_indexes 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 @@ -201,20 +202,20 @@ let fill_hits refObj hits = 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) diff --git a/helm/software/components/metadata/sqlStatements.mli b/helm/software/components/metadata/sqlStatements.mli index 72433c811..ca780ee15 100644 --- a/helm/software/components/metadata/sqlStatements.mli +++ b/helm/software/components/metadata/sqlStatements.mli @@ -36,7 +36,7 @@ type tbl = [ `RefObj| `RefSort| `RefRel| `ObjectName| `Hits| `Count] 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 @@ -46,13 +46,14 @@ val fill_hits: string -> string -> string list (** 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 diff --git a/helm/software/components/tactics/.depend b/helm/software/components/tactics/.depend index b52cdc6b3..bb3e16d8e 100644 --- a/helm/software/components/tactics/.depend +++ b/helm/software/components/tactics/.depend @@ -31,7 +31,6 @@ setoids.cmi: proofEngineTypes.cmi 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 @@ -63,8 +62,6 @@ metadataQuery.cmo: proofEngineTypes.cmi primitiveTactics.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 @@ -73,6 +70,8 @@ autoCache.cmo: universe.cmi autoCache.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 \ @@ -211,7 +210,7 @@ tactics.cmx: variousTactics.cmx tacticals.cmx substTactic.cmx setoids.cmx \ 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 diff --git a/helm/software/components/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml index 898946ad6..d9dc679b3 100644 --- a/helm/software/components/tactics/closeCoercionGraph.ml +++ b/helm/software/components/tactics/closeCoercionGraph.ml @@ -316,8 +316,8 @@ let number_if_already_defined buri name l = 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 @@ -357,8 +357,7 @@ let close_coercion_graph src tgt uri baseuri = [] [] 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 diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli index f46d53af9..fb62b85fc 100644 --- a/helm/software/components/tactics/tactics.mli +++ b/helm/software/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* 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 : diff --git a/helm/software/components/whelp/fwdQueries.ml b/helm/software/components/whelp/fwdQueries.ml index 67cc46941..5453c544e 100644 --- a/helm/software/components/whelp/fwdQueries.ml +++ b/helm/software/components/whelp/fwdQueries.ml @@ -89,9 +89,9 @@ let fwd_simpl ~dbd t = 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 @@ -111,5 +111,5 @@ let decomposables ~dbd = 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 diff --git a/helm/software/components/whelp/whelp.ml b/helm/software/components/whelp/whelp.ml index 4a863eba8..ef544f850 100644 --- a/helm/software/components/whelp/whelp.ml +++ b/helm/software/components/whelp/whelp.ml @@ -43,22 +43,30 @@ let sqlpat_of_shellglob = 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)); *) @@ -181,7 +189,7 @@ let instance ~dbd t = 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 @@ -202,11 +210,15 @@ let instance ~dbd t = 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 = diff --git a/helm/software/configure.ac b/helm/software/configure.ac index 2f6738bcd..5e02650a3 100644 --- a/helm/software/configure.ac +++ b/helm/software/configure.ac @@ -3,7 +3,7 @@ AC_INIT(matita/matitaTypes.ml) # 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 diff --git a/helm/software/daemons/http_getter/main.ml b/helm/software/daemons/http_getter/main.ml index 199a8b463..f708dc529 100644 --- a/helm/software/daemons/http_getter/main.ml +++ b/helm/software/daemons/http_getter/main.ml @@ -147,7 +147,7 @@ let return_all_xml_uris fmt outchan = | `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 -> @@ -194,7 +194,8 @@ let return_help outchan = return_html_raw (Http_getter.help ()) outchan let return_resolve writable uri outchan = try return_xml_raw - (sprintf "\n" (Http_getter.resolve ~writable uri)) + (sprintf "\n" + (Http_getter.resolve ~writable ~local:false uri)) outchan with | Unresolvable_URI _ -> return_xml_raw "\n" outchan @@ -273,7 +274,9 @@ let callback (req: Http_types.request) 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 diff --git a/helm/software/daemons/whelp/searchEngine.ml b/helm/software/daemons/whelp/searchEngine.ml index dd3c8f2c4..f2ec31ac1 100644 --- a/helm/software/daemons/whelp/searchEngine.ml +++ b/helm/software/daemons/whelp/searchEngine.ml @@ -507,11 +507,8 @@ let _ = 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 (); diff --git a/helm/software/matita/.depend b/helm/software/matita/.depend index f5fc89d54..9c5ccf8af 100644 --- a/helm/software/matita/.depend +++ b/helm/software/matita/.depend @@ -36,8 +36,10 @@ matitaGui.cmo: matitaprover.cmi matitamakeLib.cmi matitaTypes.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.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 diff --git a/helm/software/matita/.depend.opt b/helm/software/matita/.depend.opt index 2afb3c14f..d4b23c34c 100644 --- a/helm/software/matita/.depend.opt +++ b/helm/software/matita/.depend.opt @@ -36,8 +36,10 @@ matitaGui.cmo: matitaprover.cmi matitamakeLib.cmi matitaTypes.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 diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile index 15a3a8c2c..1c11060d4 100644 --- a/helm/software/matita/Makefile +++ b/helm/software/matita/Makefile @@ -31,8 +31,8 @@ MLI = \ matitaTypes.mli \ matitaMisc.mli \ matitamakeLib.mli \ - matitaInit.mli \ matitaExcPp.mli \ + matitaInit.mli \ matitaEngine.mli \ applyTransformation.mli \ matitacLib.mli \ @@ -46,8 +46,8 @@ CMLI = \ matitaTypes.mli \ matitaMisc.mli \ matitamakeLib.mli \ - matitaInit.mli \ matitaExcPp.mli \ + matitaInit.mli \ matitaEngine.mli \ applyTransformation.mli \ matitacLib.mli \ @@ -296,7 +296,7 @@ endif 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: diff --git a/helm/software/matita/help/C/matita.xml b/helm/software/matita/help/C/matita.xml index e20e17ad8..0b52d39e5 100644 --- a/helm/software/matita/help/C/matita.xml +++ b/helm/software/matita/help/C/matita.xml @@ -1,178 +1,117 @@ - - - - - - - - - - - - - - - - - - - Matita"> - - - - TODO"> - MySQL "> - - - id"> - uri"> - char"> - uri-step"> - nat"> - term"> - rec_def"> - match_pattern"> - match_branch"> - args"> - args2"> - sterm"> - intros-spec"> - pattern"> - reduction-kind"> - path"> - proof-script"> - proof-step"> - tactic"> - LCF-tactical"> - qstring"> - interpretation"> - auto_params"> + +Enrico"> + Tassi"> + 21 Jun 2007"> + 1"> + gareuselesinge@debian.org"> + + matita"> + + + Debian"> + GNU"> + GPL"> ]> - - - - - &app; V&appversion; User Manual (rev. &manrevision;) - - - + + +
+ &dhemail; +
+ + &dhfirstname; + &dhsurname; + - 2006 - The HELM team. + 2007 + &dhusername; + &dhdate; + + + &dhucpackage; + + &dhsection; + + + &dhpackage; + + creates XML data file for Vim7 omni completion from + DTDs + + + + &dhpackage; + filename.dtd + dialectname + + + + + DESCRIPTION + + This manual page documents brieftly the + &dhpackage; program. For more information see its HTML + documentation in + /usr/share/doc/vim-scripts/html/dtd2vim.html. + + + 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). + + For this feature to work the user should put an XML data file + corresponding to the desired DTD in a autoload/xml + directory contained in a directory belonging to Vim's + 'runtimepath' (for example + ~/.vim/autoload/xml/). + + &dhpackage; is the program that creates XML data + files from DTDs. Given as input a DTD + file.dtd it will create a + file.vim XML data file. + dialectname will be part of dictionary name + and will be used as argument for the :XMLns command. + + + + + + OPTIONS + + None. + + + + SEE ALSO + + vim (1). + + In the Vim online help: :help compl-omni, + :help ft-xml-omni, :help + :XMLns. + + dtd2vim is fully documented in + /usr/share/doc/vim-scripts/html/dtd2vim.html. + + + + + AUTHOR + + 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. + + On Debian systems, the complete text of the GNU General Public + License can be found in /usr/share/common-licenses/GPL. + + + - - - Andrea - Asperti - -
asperti@cs.unibo.it
- - - - Claudio - Sacerdoti Coen - -
sacerdot@cs.unibo.it
- - - - Ferruccio - Guidi - -
fguidi@cs.unibo.it
- - - - Enrico - Tassi - -
tassi@cs.unibo.it
- - - - Stefano - Zacchiroli - -
zacchiro@cs.unibo.it
- - - - - - 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 for more information. - - - - - &manrevision; - &date; - - - - - - - -&intro; -&install; -&gettingstarted; -&terms; -&usernotation; -&tacticals; -&tactics; -&declarative_tactics; -&othercommands; -&license; - - - - diff --git a/helm/software/matita/library/nat/div_and_mod_new.ma b/helm/software/matita/library/nat/div_and_mod_new.ma deleted file mode 100644 index f08a5f94e..000000000 --- a/helm/software/matita/library/nat/div_and_mod_new.ma +++ /dev/null @@ -1,369 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 = 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. diff --git a/helm/software/matita/library/nat/div_and_mod_new.ma.dontcompile b/helm/software/matita/library/nat/div_and_mod_new.ma.dontcompile new file mode 100644 index 000000000..546e92e17 --- /dev/null +++ b/helm/software/matita/library/nat/div_and_mod_new.ma.dontcompile @@ -0,0 +1,360 @@ +(**************************************************************************) +(* ___ *) +(* ||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 = if m divides n q times, with remainder r *) +definition n_divides \def \lambda n,m:nat.n_divides_aux n n m O. diff --git a/helm/software/matita/matita.conf.xml.in b/helm/software/matita/matita.conf.xml.in index 7d81977b6..62f69ac61 100644 --- a/helm/software/matita/matita.conf.xml.in +++ b/helm/software/matita/matita.conf.xml.in @@ -24,19 +24,50 @@
- + + + @DBHOST@ matita helm none library + @DBHOST@ matita helm none user + + + + - @DBHOST@ - helm - matita