]> matita.cs.unibo.it Git - helm.git/blob - matita/scripts/public_html/bench.php
more static libs for matitaprover
[helm.git] / matita / scripts / public_html / bench.php
1 <?php require("common.php"); 
2   
3 // syntax
4 //
5 // queries ::= query | query "###" queries
6 // query ::= name "@@@" sql
7 //
8 $limits = array("20","50","100");
9   
10 $quey_all = urlencode("
11 Whole content:
12 @@@
13 select * from bench order by mark desc***");
14
15 $query_fail = urlencode("
16 Number of failures
17 @@@
18 select 
19   mark, count(distinct test) as fail_no 
20 from bench 
21 where result = 'fail' group by mark order by mark desc***
22 ###
23 Tests failed
24 @@@
25 select distinct mark, test, result 
26 from bench 
27 where result = 'fail' order by mark desc***");
28
29 $query_gc = urlencode("
30 GC usage 
31 @@@
32 select 
33   bench.mark, SUM(bench.time) - SUM(bench1.time) as gc_hoverhead 
34 from bench, bench as bench1 
35 where 
36   bench.mark = bench1.mark and 
37   bench.test = bench1.test and 
38   bench.options = 'gc-on' and
39   bench1.options = 'gc-off' and 
40   bench.compilation = bench1.compilation 
41 group by mark***
42 ###
43 GC usage (opt)
44 @@@
45 select 
46   bench.mark, SUM(bench.time) - SUM(bench1.time) as gc_hoverhead 
47 from bench, bench as bench1
48 where 
49   bench.mark = bench1.mark and 
50   bench.test = bench1.test and 
51   bench.options = 'gc-on' and 
52   bench1.options = 'gc-off' and 
53   bench.compilation = bench1.compilation and 
54   bench.compilation = 'opt' 
55 group by mark***
56 ###
57 GC usage (byte)
58 @@@
59 select 
60   bench.mark, SUM(bench.time) - SUM(bench1.time) as gc_hoverhead 
61 from bench, bench as bench1 
62 where 
63   bench.mark = bench1.mark and
64   bench.test = bench1.test and 
65   bench.options = 'gc-on' and 
66   bench1.options = 'gc-off' and 
67   bench.compilation = bench1.compilation and 
68   bench.compilation = 'byte' 
69 group by mark***");
70
71 $query_auto = urlencode("
72 Auto (with GC)
73 @@@
74 select 
75   mark, SUM(bench.time) as time 
76 from 
77   bench 
78 where 
79   test='auto.ma' and options = 'gc-on' 
80 group by mark 
81 order by mark desc***
82 ### 
83 Auto (without GC)
84 @@@
85 select 
86   mark, SUM(bench.time) as time 
87 from 
88   bench 
89 where 
90   test='auto.ma' and options = 'gc-off' 
91 group by mark 
92 order by mark desc
93 ***
94 ### 
95 GC overhead
96 @@@
97 select 
98   bench.mark, SUM(bench.time) - SUM(bench1.time) as gc_hoverhead 
99 from 
100   bench, bench as bench1 
101 where 
102   bench.mark = bench1.mark and 
103   bench.test = bench1.test and 
104   bench.options = 'gc-on' and 
105   bench1.options = 'gc-off' and 
106   bench.compilation = bench1.compilation and 
107   bench.test = 'auto.ma' 
108 group by mark
109 ***");
110
111 $query_csc = urlencode("
112 Performances (byte and GC) per mark
113 @@@
114 select 
115   bench.mark,
116   bench_svn.revision as revision, 
117   SUM(bench.time) as sum_time,
118   SUM(bench.timeuser) as sum_timeuser, 
119   COUNT(DISTINCT bench.test) as performed_tests,
120   COUNT(DISTINCT bench1.test) as failed_tests
121 from 
122   bench, bench_svn,bench as bench1 
123 where 
124   bench.options = 'gc-on' and 
125   bench.compilation = 'byte' and 
126   bench_svn.mark = bench.mark and
127   bench1.result = 'fail' and
128   bench1.mark = bench.mark and
129   bench1.compilation = 'byte' and
130   bench1.options = 'gc-on'
131 group by bench.mark
132 order by bench.mark desc
133 ***");
134
135 $query_csc_opt = urlencode("
136 Performances (opt and GC) per mark
137 @@@
138 select 
139   bench.mark,
140   bench_svn.revision as revision, 
141   SUM(bench.time) as sum_time,
142   SUM(bench.timeuser) as sum_timeuser, 
143   COUNT(DISTINCT bench.test) as performed_tests,
144   COUNT(DISTINCT bench1.test) as failed_tests
145 from 
146   bench, bench_svn,bench as bench1 
147 where 
148   bench.options = 'gc-on' and 
149   bench.compilation = 'opt' and 
150   bench_svn.mark = bench.mark and
151   bench1.result = 'fail' and
152   bench1.mark = bench.mark and
153   bench1.compilation = 'opt' and
154   bench1.options = 'gc-on'
155 group by bench.mark
156 order by bench.mark desc
157 ***");
158
159 $query_total = urlencode("
160 Max N
161 @@@
162 select 
163   COUNT(DISTINCT test) as MAX 
164 from 
165   bench 
166 group by mark 
167 order by MAX desc 
168 LIMIT 0,1;
169 ###
170 Number of compiled tests
171 @@@
172 select 
173   mark, 
174   COUNT(DISTINCT test) as N 
175 from 
176   bench 
177 group by mark 
178 order by mark desc
179 ***");
180
181 function minus1_to_all($s){
182   if ($s == "-1") 
183     return "all";
184   else 
185     return $s;
186 }
187
188 function links_of($name,$q,$limits){
189   echo "<li>$name :&nbsp;&nbsp;&nbsp;";
190   if (strpos($q, urlencode("***")) === false) {
191     echo "<a href=\"showquery.php?query=$q;\">all</a>";
192   } else {
193     foreach($limits as $l) {
194       $q1 = str_replace(urlencode("***"), " LIMIT 0,$l", $q);
195       echo "<a href=\"showquery.php?query=$q1;\">" . 
196             minus1_to_all($l) . "</a>&nbsp;&nbsp;";
197     }
198       $q1 = str_replace(urlencode("***"), " ", $q);
199       echo "<a href=\"showquery.php?query=$q1;\">" . 
200             minus1_to_all("-1") . "</a>&nbsp;&nbsp;";
201   }
202   echo "</li>";
203 }
204
205 ?>
206
207 <html>
208   <head>
209   <link type="text/css" rel="stylesheet" href="style.css"/>
210   </head>
211   <body>
212     <h1>QUERY the benchmark system</h1>
213     <h2>Common Queries</h2>
214     <p>
215       <ul>
216       <? links_of("Broken tests",$query_fail,$limits) ?>
217       <? links_of("Garbage collector killer",$query_gc,$limits) ?>
218       <? links_of("Auto performances",$query_auto,$limits) ?>
219       <? links_of("Global performances (bytecode)",$query_csc,$limits) ?>
220       <? links_of("Global performances (nativecode)",$query_csc_opt,$limits) ?>
221       <? links_of("Number of compiled tests",$query_total,$limits) ?>
222       <? links_of("All table contents",$quey_all,$limits) ?>
223       </ul>
224     </p>
225     <h2>Custom Query - Simple Interface</h2>
226     <form action="composequery.php" method="get">
227     <table>
228   <tr>
229     <td>Marks:</td>
230     <td> 
231       <select name="mark">";
232         <option value="--">--</option>";
233         <?query("select distinct mark from bench order by mark desc;",
234             "array_to_combo");?>
235       </select>      
236     </td>
237   </tr>
238   <tr>
239     <td>Compilations:</td>
240     <td> 
241       <select name="compilation">";
242         <option value="--">--</option>";
243           <?query("select distinct compilation from bench;","array_to_combo");?>
244       </select>      
245     </td>
246   </tr>
247   <tr>
248     <td>Options:</td>
249     <td>  
250       <select name="options">";
251         <option value="--">--</option>";
252           <?query("select distinct options from bench;","array_to_combo");?>
253       </select>      
254     </td>
255   </tr>
256   <tr>
257     <td>Tests:</td>
258     <td>    
259       <select name="test">";
260         <option value="--">--</option>";
261           <?query("select distinct test from bench;","array_to_combo");?>
262       </select>      
263     </td>
264   </tr>
265   <tr>
266     <td>Test results:</td>
267     <td>
268       <select name="result">";
269         <option value="--">--</option>";
270           <?query("select distinct result from bench;","array_to_combo"); ?>
271       </select>      
272     </td>
273   </tr>
274   <tr>
275     <td>Group By: </td>
276     <td>
277       <select name="groupby">";
278         <option value="--">--</option>";
279         <? array_to_combo(array("mark"));array_to_combo(array("options")); ?>
280       </select>      
281     </td>
282   </tr>
283   <tr>
284     <td>Limit: </td>
285     <td>
286       <select name="limit">";
287         <option value="--">--</option>";
288       <? foreach(array($limits) as $l) {array_to_combo($l);} ?>
289       </select>      
290     </td>
291   </tr>
292   <tr>
293     <td><input type="submit" value="Submit" class="button" /></td>
294   </tr>
295  </table>
296 </form>
297 <h2>Custom Query - raw SQL</h2>
298 <form action="showquery.php" method="get">
299 <table>
300 <tr><td>'bench' table description:</td></tr>
301 </tr>
302 <? query("describe bench","printer"); ?>
303 </tr>
304 <tr><td></td></tr>
305 <tr><td colspan="7">
306 SQL (only one query, ';' if present must terminate the query, no characters allowed after it):</td></tr>
307 <tr><td colspan="7">
308 <textarea rows="10" cols="120" name="query"/>
309 select 
310   b1.test as test, b1.timeuser as oldtime, b2.timeuser as newtime, b1.compilation as comp, b1.options as opts
311 from 
312   bench as b1, bench as b2 
313 where 
314   b1.test = b2.test and 
315   b1.options = b2.options and
316   b1.compilation = b2.compilation and 
317   b1.mark = '' and b2.mark= '' and
318   ABS(b1.timeuser - b2.timeuser) &gt; 100;</textarea>
319 </td>
320 </tr>
321 <tr><td>
322 <input type="submit" value="Submit" class="button" /></td>
323 </tr>
324 </table>
325 </form>
326
327 </body>
328 </html>