first snapshot of the night-profiling

[helm.git] / helm / matita / scripts / insert.awk

diff --git a/helm/matita/scripts/insert.awk b/helm/matita/scripts/insert.awk
new file mode 100644 (file)
index 0000000..267e893
--- /dev/null
+++ b/helm/matita/scripts/insert.awk
@@ -0,0 +1,18 @@
+
+
+/^[^#]/ {
+       result=tolower($1);
+       if( $2 ~ "\.opt$" )
+               compilation="opt"
+       else
+               compilation="byte"
+       test=$3 
+       time="0:" $4
+       mark=$7
+       if ( $8 ~ "^GC=off$") 
+               options="'no-gc'"
+       else
+               options="''"
+               
+       printf "INSERT bench (result, compilation, test, time, mark, options) VALUES ('%s', '%s', '%s', '%s', '%s', %s);\n", result, compilation, test, time, mark, options;
+       }