From: Enrico Tassi Date: Fri, 8 Jul 2005 09:55:48 +0000 (+0000) Subject: added query X-Git-Tag: pre_notation~78 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=34104f5a2b1ba5c2a795cd5c8502f8944de23b20;p=helm.git added query --- diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index bb2e3c1a6..354ecd9e8 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -523,7 +523,7 @@ let eval_command status cmd = match obj with Cic.CurrentProof (_,metasenv',bo,ty,_,_) -> let name = UriManager.name_of_uri uri in - if not(CicPp.check name ty) then + if not(CicPp.check name ty) then MatitaLog.warn ("Bad name: " ^ name); assert (metasenv = metasenv'); let goalno = diff --git a/helm/matita/scripts/public_html/bench.php b/helm/matita/scripts/public_html/bench.php index 656569a1e..015e7c4c1 100644 --- a/helm/matita/scripts/public_html/bench.php +++ b/helm/matita/scripts/public_html/bench.php @@ -33,6 +33,8 @@ $query_auto = urlencode( "GC overhead@@@select bench.mark, SEC_TO_TIME(SUM(TIME_TO_SEC(bench.time)) - SUM(TIME_TO_SEC(bench1.time))) as gc_hoverhead from bench, bench as bench1 where bench.mark = bench1.mark and bench.test = bench1.test and bench.options = 'gc-on' and bench1.options = 'gc-off' and bench.compilation = bench1.compilation and bench.test = 'auto.ma' group by mark;" ); +$query_csc = urlencode("Performances (byte and GC) per mark@@@select mark, SEC_TO_TIME(SUM(TIME_TO_SEC(time))) as sum_time, SEC_TO_TIME(SUM(TIME_TO_SEC(timeuser))) as sum_timeuser from bench where options = 'gc-on' and compilation = 'byte'group by mark;"); + ?> @@ -47,6 +49,7 @@ $query_auto = urlencode(
  • Broken tests
  • Garbage collector killer
  • Auto performances
    • +
  • Global performances
  • All table contents