added a getter maps updater

diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in
index 428492209c6f4baacd421db3541c560eec715636..67a7fabc8c552a5b3c7600dab01c0d4a4a3ff2e8 100644 (file)
--- a/helm/matita/Makefile.in
+++ b/helm/matita/Makefile.in
@@ -45,6 +45,9 @@ CCMOS =                               \
 
 all: matita matitac cicbrowser
 
+updater:
+       $(OCAMLC) $(PKGS) -linkpkg -o $@ updater.ml
+
 ifeq ($(HAVE_OCAMLOPT),yes)
 CMXS = $(patsubst %.cmo,%.cmx,$(CMOS))
 CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS))

diff --git a/helm/matita/scripts/do_tests.sh b/helm/matita/scripts/do_tests.sh
index b95ca578cdbababbe0bfd9908e42f962c446b7c9..737ea7c5efd42de28d6359f0126f56ba96ee5068 100755 (executable)
--- a/helm/matita/scripts/do_tests.sh
+++ b/helm/matita/scripts/do_tests.sh
@@ -29,7 +29,7 @@ TMP=.__temp.txt
 
 for T in $TODO; do
   echo -en "$COMPILER\t$T\t"
-  /usr/bin/time -o $TMP -f "%E\t%U\t%S" $COMPILER $T >> $LOGFILE 2>&1
+  /usr/bin/time --quiet -o $TMP -f "%E\t%U\t%S" $COMPILER $T >> $LOGFILE 2>&1
   if [ $? = 0 ]; then
     echo -e "$OK\t`cat $TMP`\t$DO_TESTS_EXTRA"
   else

diff --git a/helm/matita/scripts/profile_cvs.sh b/helm/matita/scripts/profile_cvs.sh
index 63eeee22d34147be0f34f7aa364d42f306aca422..7f2d4308f904e7ec9eb156c36f70c9125665c130 100755 (executable)
--- a/helm/matita/scripts/profile_cvs.sh
+++ b/helm/matita/scripts/profile_cvs.sh
@@ -9,33 +9,42 @@ function testit {
   LOGTOBYTE=/dev/null
   export DO_TESTS_EXTRA="$MARK\t$n"
   ls
-  scripts/do_tests.sh -nocolor ./matitac.opt $LOGTOOPT tests/*.ma
-  scripts/do_tests.sh -nocolor ./matitac $LOGTOBYTE tests/*.ma
+  scripts/do_tests.sh -no-color ./matitac.opt $LOGTOOPT tests/*.ma
+  #scripts/do_tests.sh -nocolor ./matitac $LOGTOBYTE tests/*.ma
 }
 
 function compile {
-  make -C $1 all opt 1>/dev/null 2>/dev/null
-  make -C $2 matitac matitac.opt 1>/dev/null 2>/dev/null
+  OLD=$PWD
+  cd $1
+  autoconf 1>/dev/null
+  ./configure 1>/dev/null
+  make all opt 1>/dev/null
+  cd $2
+  autoconf 1>/dev/null
+  ./configure 1>/dev/null
+  make matitac matitac.opt updater 1>/dev/null
+  ./updater
+  cd $OLD
 }
 
 function run_tests {
-  OLD=`pwd`
+  OLD=$PWD
   cd $1
   export OCAMLRUNPARAM='o=1000000'
-  testit $IMPL "off" 1>/dev/null 2>/dev/null
+  #testit $IMPL "off" 1>/dev/null 2>/dev/null
   testit $IMPL "off"
   export OCAMLRUNPARAM=''
-  testit $IMPL "on" 1>/dev/null 2>/dev/null
-  testit $IMPL "on"
+  #testit $IMPL "on" 1>/dev/null 2>/dev/null
+  #testit $IMPL "on"
   cd $OLD
 }
 
-rm -rf $TMPDIRNAME
-mkdir $TMPDIRNAME
+#rm -rf $TMPDIRNAME
+#mkdir $TMPDIRNAME
 cd $TMPDIRNAME
-
-cvs -d $CVSROOT co helm/ocaml 1>/dev/null 2>/dev/null
-cvs -d $CVSROOT co helm/matita 1>/dev/null 2>/dev/null
+#cvs -d $CVSROOT co helm/ocaml 1>/dev/null 2>/dev/null
+#cvs -d $CVSROOT co helm/matita 1>/dev/null 2>/dev/null
 compile $PWD/helm/ocaml $PWD/helm/matita
 run_tests $PWD/helm/matita #> LOG
+#rm -rf $TMPDIRNAME
 

diff --git a/helm/matita/updater.ml b/helm/matita/updater.ml
new file mode 100644 (file)
index 0000000..4a777e4
--- /dev/null
+++ b/helm/matita/updater.ml
@@ -0,0 +1,10 @@
+let main () = 
+  Helm_registry.load_from "matita.conf.xml";
+  Http_getter.init ();
+  MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
+  Http_getter.update ();
+  Http_getter.sync_dump_file ()
+;;
+
+main ()
+