From: Enrico Tassi Date: Mon, 7 Jan 2008 15:06:22 +0000 (+0000) Subject: more fixes to the cleanu phase X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=a37b9f70260a625c93b148fd51b3314639c954ec more fixes to the cleanu phase --- diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index dfe0c019f..409c0921a 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -681,7 +681,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status status,[] | GrafiteAst.Print (_,"proofterm") -> let _,_,_,p,_, _ = GrafiteTypes.get_current_proof status in - print_endline (Auto.pp_proofterm p); + prerr_endline (Auto.pp_proofterm p); status,[] | GrafiteAst.Print (_,_) -> status,[] | GrafiteAst.Qed loc -> diff --git a/components/library/libraryClean.ml b/components/library/libraryClean.ml index 6998c1cbf..9a3b17245 100644 --- a/components/library/libraryClean.ml +++ b/components/library/libraryClean.ml @@ -34,14 +34,17 @@ module HGT = Http_getter_types;; module HG = Http_getter;; module UM = UriManager;; -let cache_of_processed_baseuri = Hashtbl.create 1024 -let one_step_depend suri dbtype dbd = - let buri = - try - UM.buri_of_uri (UM.uri_of_string suri) - with UM.IllFormedUri _ -> suri - in +let strip_xpointer s = Pcre.replace ~pat:"#.*$" s ;; + +let safe_buri_of_suri suri = + try + UM.buri_of_uri (UM.uri_of_string suri) + with + UM.IllFormedUri _ -> suri + +let one_step_depend cache_of_processed_baseuri suri dbtype dbd = + let buri = safe_buri_of_suri suri in if Hashtbl.mem cache_of_processed_baseuri buri then [] else @@ -53,18 +56,22 @@ let one_step_depend suri dbtype dbd = let obj_tbl = MetadataTypes.obj_tbl () in if HSql.isMysql dbtype dbd then sprintf ("SELECT source, h_occurrence FROM %s WHERE " - ^^ "h_occurrence REGEXP '^%s[^/]*$'") obj_tbl buri + ^^ "h_occurrence REGEXP '"^^ + "^%s\\([^/]+\\|[^/]+#xpointer.*\\)$"^^"'") + obj_tbl buri else - begin + begin sprintf ("SELECT source, h_occurrence FROM %s WHERE " - ^^ "REGEXP(h_occurrence, '^%s[^/]*$')") obj_tbl buri - (* implementation with vanilla ocaml-sqlite3 - HLog.debug "Warning SELECT without REGEXP"; - sprintf - ("SELECT source, h_occurrence FROM %s WHERE " ^^ - "h_occurrence LIKE '%s%%' " ^^ HSql.escape_string_for_like) - obj_tbl buri*) - end + ^^ "REGEXP(h_occurrence, '"^^ + "^%s\\([^/]+\\|[^/]+#xpointer.*\\)$"^^"')") + obj_tbl buri + (* implementation with vanilla ocaml-sqlite3 + HLog.debug "Warning SELECT without REGEXP"; + sprintf + ("SELECT source, h_occurrence FROM %s WHERE " ^^ + "h_occurrence LIKE '%s%%' " ^^ HSql.escape_string_for_like) + obj_tbl buri*) + end in try let rc = HSql.exec dbtype dbd query in @@ -72,8 +79,9 @@ let one_step_depend suri dbtype dbd = HSql.iter rc ( fun row -> match row.(0), row.(1) with - | Some uri, Some occ when Filename.dirname occ = buri -> - l := uri :: !l + | Some uri, Some occ when + Filename.dirname (strip_xpointer occ) = buri -> + l := uri :: !l | _ -> ()); let l = List.sort Pervasives.compare !l in HExtlib.list_uniq l @@ -81,12 +89,6 @@ let one_step_depend suri dbtype dbd = exn -> raise exn (* no errors should be accepted *) end -let safe_buri_of_suri suri = - try - UM.buri_of_uri (UM.uri_of_string suri) - with - UM.IllFormedUri _ -> suri - let db_uris_of_baseuri buri = let dbd = LibraryDb.instance () in let dbtype = @@ -107,22 +109,20 @@ let db_uris_of_baseuri buri = in try let rc = HSql.exec dbtype dbd query in - let strip_xpointer s = Pcre.replace ~pat:"#.*$" s in let l = ref [] in HSql.iter rc ( fun row -> match row.(0) with | Some uri when Filename.dirname (strip_xpointer uri) = buri -> l := uri :: !l - | _ -> - ()); + | _ -> ()); let l = List.sort Pervasives.compare !l in HExtlib.list_uniq l with exn -> raise exn (* no errors should be accepted *) ;; -let close_uri_list uri_to_remove = +let close_uri_list cache_of_processed_baseuri uri_to_remove = let dbd = LibraryDb.instance () in let dbtype = if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User @@ -176,17 +176,22 @@ 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 dbtype dbd @ acc) [] uri_to_remove + (fun acc u -> one_step_depend cache_of_processed_baseuri u dbtype dbd @ acc) + [] uri_to_remove in let depend = HExtlib.list_uniq (List.fast_sort Pervasives.compare depend) in uri_to_remove, depend +;; -let rec close_db uris next = +let rec close_db cache_of_processed_baseuri uris next = match next with | [] -> uris - | l -> let uris, next = close_uri_list l in close_db uris next @ uris + | l -> + let uris, next = close_uri_list cache_of_processed_baseuri l in + close_db cache_of_processed_baseuri uris next @ uris +;; let cleaned_no = ref 0;; @@ -203,10 +208,11 @@ let moo_root_dir = lazy ( | _ -> assert false) (Helm_registry.get_list Helm_registry.string "getter.prefix")) in - String.sub url 7 (String.length url - 7) (* remove heading "file:///" *) -) + String.sub url 7 (String.length url - 7)) +;; let clean_baseuris ?(verbose=true) buris = + let cache_of_processed_baseuri = Hashtbl.create 1024 in let dbd = LibraryDb.instance () in let dbtype = if Helm_registry.get_bool "matita.system" then HSql.Library else HSql.User @@ -216,7 +222,7 @@ let clean_baseuris ?(verbose=true) buris = debug_prerr "clean_baseuris called on:"; if debug then List.iter debug_prerr buris; - let l = close_db [] buris in + let l = close_db cache_of_processed_baseuri [] 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:"; diff --git a/matita/Makefile b/matita/Makefile index b3fbd5906..29d5b35ef 100644 --- a/matita/Makefile +++ b/matita/Makefile @@ -225,12 +225,10 @@ ifeq ($(DISTRIBUTED),yes) dist_library: install_preliminaries dist_library@standard-library dist_library@%: - $(H)echo "MATITAMAKE init $*" - $(H)(HOME=$(WHERE) USER=builder MATITA_RT_BASE_DIR=$(WHERE) MATITA_FLAGS='$(MATITA_CFLAGS)' $(WHERE)/matitamake init $* $(WHERE)/ma/$*) - $(H)echo "MATITAMAKE publish $*" - $(H)(HOME=$(WHERE) USER=builder MATITA_RT_BASE_DIR=$(WHERE) MATITA_FLAGS='$(MATITA_CFLAGS)' $(WHERE)/matitamake publish $*) - $(H)echo "MATITAMAKE destroy $*" - $(H)(HOME=$(WHERE) USER=builder MATITA_RT_BASE_DIR=$(WHERE) MATITA_FLAGS='$(MATITA_CFLAGS)' $(WHERE)/matitamake destroy $*) + $(H)echo "publish $*" + $(H)cd $*;(HOME=$(WHERE) USER=builder MATITA_RT_BASE_DIR=$(WHERE) MATITA_FLAGS='$(MATITA_CFLAGS)' $(WHERE)/matitac -system) + $(H)echo "destroy $*" + $(H)cd $*;(HOME=$(WHERE) USER=builder MATITA_RT_BASE_DIR=$(WHERE) MATITA_FLAGS='$(MATITA_CFLAGS)' $(WHERE)/matitacclean) # sqlite3 only $(H)cp $(WHERE)/.matita/matita.db $(WHERE)/metadata.db || true #$(H)rm -rf $(WHERE)/.matita/ diff --git a/matita/legacy/makefile b/matita/legacy/makefile deleted file mode 100644 index a1dd3ca33..000000000 --- a/matita/legacy/makefile +++ /dev/null @@ -1,39 +0,0 @@ -H=@ - -RT_BASEDIR=../ -OPTIONS=-bench -onepass -system -MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS) -CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) -MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS) -CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS) - -devel:=$(shell basename `pwd`) - -ifneq "$(SRC)" "" - XXX="SRC=$(SRC)" -endif - -all: preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel) -clean: preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel) -cleanall: preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all - -all.opt opt: preall.opt - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel) -clean.opt: preall.opt - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel) -cleanall.opt: preall.opt - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all - -%.mo: preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@ -%.mo.opt: preall.opt - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $(@:.opt=) - -preall: - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel) - -preall.opt: - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) init $(devel)