more fixes to the cleanu phase

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index dfe0c019f4833a06d2cf8fe309249455473b2ff5..409c0921aeb3f41b1876511fb95d2a2100921527 100644 (file)
--- 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 6998c1cbf1ceee98a6d84e4e43c9307b5a8f98df..9a3b172454c00268bd0a4320030bee9711b76a6a 100644 (file)
--- 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 b3fbd5906d94123fc5ce6daf8d2e29568cbfab62..29d5b35ef47ef4f8eb200b4c6c79f7b937dd72e1 100644 (file)
--- 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 (file)
index a1dd3ca..0000000
--- 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)