From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 28 Oct 2005 16:59:07 +0000 (+0000)
Subject: fix
X-Git-Tag: V_0_7_2_3~172
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d6b38a5565abd0efa64578639a097761ea298dbc;p=helm.git

fix
---

diff --git a/helm/matita/scripts/crontab.sh b/helm/matita/scripts/crontab.sh
index f4c7b4a8e..ba63e00d2 100644
--- a/helm/matita/scripts/crontab.sh
+++ b/helm/matita/scripts/crontab.sh
@@ -11,20 +11,20 @@ cd $TMPDIRNAME
 cvs -d $CVSROOT co helm/matita/scripts 1>/dev/null 2>/dev/null
 helm/matita/scripts/profile_cvs.sh 2> LOG
 
-CUR_TIME=`echo "select mark, SUM(TIME_TO_SEC(time)) from bench where mark = \"$MARK\" group by mark;" | mysql -u helm -h mowgli.cs.unibo.it matita | tail -n 1 | awk '{print $2}'`
-OLD_TIME=`echo "select mark, SUM(TIME_TO_SEC(time)) from bench where mark = \"$LASTMARK\" group by mark;" | mysql -u helm -h mowgli.cs.unibo.it matita | tail -n 1 | awk '{print $2}'`
+CUR_TIME=`/usr/bin/php4 -c /etc/php4/apache/php.ini - shell_adder.php -- public_html/common.php "select SEC_TO_TIME(SUM(TIME_TO_SEC(time))) from bench where mark = \"$MARK\" group by mark;"`
+OLD_TIME=`/usr/bin/php4 -c /etc/php4/apache/php.ini - shell_adder.php -- public_html/common.php  "select mark, SEC_TO_TIME(SUM(TIME_TO_SEC(time))) from bench where mark = \"$LASTMARK\" group by mark;"`
 
 if [ -z "$CUR_TIME" -o -z "$OLD_TIME" ]; then
   echo "No benchamks records for $MARK"
   exit 1
 fi
 
-((DELTA=$CUR_TIME - $OLD_TIME))
+((DELTA=`/usr/bin/php4 -c /etc/php4/apache/php.ini - shell_time2cents.php -- public_html/common.php $CUR_TIME` - `/usr/bin/php4 -c /etc/php4/apache/php.ini - shell_time2cents.php -- public_html/common.php $OLD_TIME`))
 if [ $DELTA -lt 0 ]; then
   PERC=0
 else
   ((PERC=100 * $DELTA))
-  ((PERC=$PERC / $OLD_TIME))
+  ((PERC=$PERC / `/usr/bin/php4 -c /etc/php4/apache/php.ini - shell_time2cents.php -- public_html/common.php $OLD_TIME`))
 fi
 if [ $PERC -ge 5 ]; then
   cat <<EOT
@@ -38,8 +38,8 @@ if [ $PERC -ge 5 ]; then
 EOT
 fi
 
-CUR_FAIL=`echo "select count(distinct test) from bench where mark = \"$MARK\" and result = 'fail';" | mysql -u helm -h mowgli.cs.unibo.it matita | tail -n 1`
-OLD_FAIL=`echo "select count(distinct test) from bench where mark = \"$LASTMARK\" and result = 'fail';" | mysql -u helm -h mowgli.cs.unibo.it matita | tail -n 1`
+CUR_FAIL=`/usr/bin/php4 -c /etc/php4/apache/php.ini - shell_adder.php -- public_html/common.php "select count(distinct test) from bench where mark = \"$MARK\" and result = 'fail';"`
+OLD_FAIL=`/usr/bin/php4 -c /etc/php4/apache/php.ini - shell_adder.php -- public_html/common.php "select count(distinct test) from bench where mark = \"$LASTMARK\" and result = 'fail';"`
 
 if [ $CUR_FAIL -gt $OLD_FAIL ]; then
   cat <<EOT
@@ -50,7 +50,7 @@ if [ $CUR_FAIL -gt $OLD_FAIL ]; then
   now broken:
   `echo "select distinct test from bench where mark = \"$MARK\" and result = 'fail';" | mysql -u helm -h mowgli.cs.unibo.it matita`
   were broken:
-  `echo "select distinct test from bench where mark = \"$OLDMARK\" and result = 'fail';" | mysql -u helm -h mowgli.cs.unibo.it matita`
+  `echo "select distinct test from bench where mark = \"$LASTMARK\" and result = 'fail';" | mysql -u helm -h mowgli.cs.unibo.it matita`
   
 EOT
 
diff --git a/helm/matita/scripts/public_html/common.php b/helm/matita/scripts/public_html/common.php
index 81a0565cf..10aeb8d82 100644
--- a/helm/matita/scripts/public_html/common.php
+++ b/helm/matita/scripts/public_html/common.php
@@ -25,6 +25,17 @@ function query($q) {
   }
 }
 
+function time_2_cents($t) {
+  $matches = array();
+  $rex = "/^(\d+)m(\d{2})\.(\d{2})s$/";
+  $m = preg_match($rex,$t,$matches);
+  if ( $m == 0 ) exit 1;
+  $t_minutes = $matches[1];
+  $t_secs = $matches[2];
+  $t_cents = $matches[3];
+  return ((int) $t_cents) + ((int) $t_secs) * 100 + ((int)$t_minutes) * 6000 ;
+}
+
 function sum_time($t1, $t2) {
   $matches1 = array();
   $matches2 = array();
diff --git a/helm/matita/scripts/shell_adder.php b/helm/matita/scripts/shell_adder.php
index e0ddda95e..a13005e55 100755
--- a/helm/matita/scripts/shell_adder.php
+++ b/helm/matita/scripts/shell_adder.php
@@ -1,5 +1,6 @@
-#!/usr/bin/php4
 <?php
  require($argv[1]);
- print(sum_time($argv[2], $argv[3])); 
+ $rc = query($argv[2]);
+ $a = array_values($rc[0]); 
+ print($a[0]);
 ?>
diff --git a/helm/matita/scripts/shell_time2cents.php b/helm/matita/scripts/shell_time2cents.php
new file mode 100755
index 000000000..4914fc24f
--- /dev/null
+++ b/helm/matita/scripts/shell_time2cents.php
@@ -0,0 +1,4 @@
+<?php
+ require($argv[1]);
+ print(time_2_cents($argv[2]));
+?>