From f81860fd2d2c23d53b58873a1d0e3feaa0247b92 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 24 Jun 2005 08:57:54 +0000
Subject: [PATCH] added a getter maps updater

---
 helm/matita/Makefile.in            |  3 +++
 helm/matita/scripts/do_tests.sh    |  2 +-
 helm/matita/scripts/profile_cvs.sh | 35 +++++++++++++++++++-----------
 helm/matita/updater.ml             | 10 +++++++++
 4 files changed, 36 insertions(+), 14 deletions(-)
 create mode 100644 helm/matita/updater.ml

diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in
index 428492209..67a7fabc8 100644
--- 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 b95ca578c..737ea7c5e 100755
--- 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 63eeee22d..7f2d4308f 100755
--- 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
index 000000000..4a777e4d0
--- /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 ()
+
-- 
2.39.2