X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fscripts%2Ffunctions.lua;h=e6935fb5cc3c924588a4d247bdf1ae45b26b53f0;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=33b945dbde7e3ae7921a20e26d122854b056106e;hpb=1108f4fe01ea2dccd8d3b591f2cdc131dab7913e;p=helm.git

diff --git a/helm/software/matita/scripts/functions.lua b/helm/software/matita/scripts/functions.lua
index 33b945dbd..e6935fb5c 100755
--- a/helm/software/matita/scripts/functions.lua
+++ b/helm/software/matita/scripts/functions.lua
@@ -1,8 +1,8 @@
 #!/usr/bin/lua5.1
 
 local tool_re = "^([%w%.]+)"
-local test_re = "([%w%./_]+)"
-local rc_re = "([%a]+)"
+local test_re = "([%w%./_-]+)"
+local rc_re = string.char(27).."%[%d+;%d+m([%a]+)"..string.char(27).."%[0m"
 local time_re = "(%d+m%d+%.%d+s)"
 local mark_re = "(%d+)"
 local opt_re = "(gc%-%a+)$"
@@ -18,10 +18,18 @@ local re = tool_re .. sep .. test_re .. sep .. rc_re .. sep ..
 	mark_re .. sep .. opt_re 
 
 -- the string to cents of seconds function
-function convert(s)
+function s2t(s)
 	local _,_,min,sec,cents = string.find(s,"(%d+)m(%d+)%.(%d+)s")
 	return min * 6000 + sec * 100 + cents
 end
+function t2s(s)
+  s = tonumber(s)
+  local min, sec, cents
+  cents = s % 100
+  min = math.floor(s / 6000)
+  sec = math.floor((s - min * 6000 - cents) / 100)
+  return string.format("%dm%02d.%02ds",min,sec,cents)
+end
 
 -- logfile to sql conversion
 function log2sql(file)
@@ -34,7 +42,7 @@ for l in f:lines() do
 	local x,_,tool,test,rc,real,user,_,mark,opt = string.find(l,re)
 
 	if x == nil then
-		error("regex failed on " .. l)
+    error("regex failed on '"..l.."'")
 	end
 
 	-- check the result is valid
@@ -51,8 +59,8 @@ for l in f:lines() do
 	if opt ~= "gc-on" and opt ~= "gc-off" then
 		error("unknown option "..opt)
 	end
-	real = convert(real)
-	user = convert(user)
+	real = s2t(real)
+	user = s2t(user)
 
 	-- print the sql statement
 	table.insert(t,string.format(fmt,rc,tool,test,real,user,mark,opt))
@@ -60,6 +68,30 @@ end
 return table.concat(t)
 end
 
+-- proportions
+function proportion(x,y,a,b)
+  local rc
+  if x == "x" then
+    rc = y * a / b
+  elseif y == "x" then
+    rc = x * b / a
+  elseif a == "x" then
+    rc = x * b / y
+  elseif b == "x" then
+    rc = y * a / x
+  end
+  return string.format("%d",rc)
+end
+
+-- conversion from the old db to the new one
+function convertsql(file)
+  local f = io.open(file)
+  return string.gsub(f:read("*a"),time_re,
+    function(s)
+      return s2t(s)
+    end)
+end
+
 -- call the desired function and print the result
 fun = arg[1]
 table.remove(arg,1)