fix

diff --git a/helm/matita/scripts/crontab.sh b/helm/matita/scripts/crontab.sh
index f4c7b4a8e67adf341b212fe7da73ed3c3dd8d6b2..ba63e00d2d698c3414dbcedc761c935db29f2b6f 100644 (file)
--- 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 81a0565cf9faad81de5f47dc0258cf83db688cd0..10aeb8d823a025758c0a51dc349917c1fb48be84 100644 (file)
--- 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 e0ddda95e89dda6941f97159da0063dd7034d46a..a13005e551ef7e79ee6f0356ed36af0b79504889 100755 (executable)
--- 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 (executable)
index 0000000..4914fc2
--- /dev/null
+++ b/helm/matita/scripts/shell_time2cents.php
@@ -0,0 +1,4 @@
+<?php
+ require($argv[1]);
+ print(time_2_cents($argv[2]));
+?>