helm/software/matita/scripts/functions.lua

   1 #!/usr/bin/lua5.1
   2
   3 local tool_re = "^([%w%.]+)"
   4 local test_re = "([%w%./_]+)"
   5 local rc_re = "([%a]+)"
   6 local time_re = "(%d+m%d+%.%d+s)"
   7 local mark_re = "(%d+)"
   8 local opt_re = "(gc%-%a+)$"
   9 local sep = "%s+"
  10
  11 local fmt = "INSERT bench "..
  12         "(result, compilation, test, time, timeuser, mark, options) "..
  13         "VALUES ('%s', '%s', '%s', %d, %d, '%s', '%s');\n"
  14
  15 -- build the huge regex
  16 local re = tool_re .. sep .. test_re .. sep .. rc_re .. sep ..
  17         time_re .. sep ..time_re .. sep ..time_re .. sep ..
  18         mark_re .. sep .. opt_re
  19
  20 -- the string to cents of seconds function
  21 function convert(s)
  22         local _,_,min,sec,cents = string.find(s,"(%d+)m(%d+)%.(%d+)s")
  23         return min * 6000 + sec * 100 + cents
  24 end
  25
  26 -- logfile to sql conversion
  27 function log2sql(file)
  28 local t = {}
  29 local f = io.stdin
  30 if file ~= "-" then
  31         f = io.open(file,"r")
  32 end
  33 for l in f:lines() do
  34         local x,_,tool,test,rc,real,user,_,mark,opt = string.find(l,re)
  35
  36         if x == nil then
  37                 error("regex failed on " .. l)
  38         end
  39
  40         -- check the result is valid
  41         if tool ~= "matitac" and tool ~= "matitac.opt" then
  42                 error("unknown tool " .. tool)
  43         else
  44                 if tool == "matitac" then tool = "byte" else tool = "opt" end
  45         end
  46         if rc ~= "OK" and rc ~= "FAIL" then
  47                 error("unknown result " .. rc)
  48         else
  49                 rc = string.lower(rc)
  50         end
  51         if opt ~= "gc-on" and opt ~= "gc-off" then
  52                 error("unknown option "..opt)
  53         end
  54         real = convert(real)
  55         user = convert(user)
  56
  57         -- print the sql statement
  58         table.insert(t,string.format(fmt,rc,tool,test,real,user,mark,opt))
  59 end
  60 return table.concat(t)
  61 end
  62
  63 -- call the desired function and print the result
  64 fun = arg[1]
  65 table.remove(arg,1)
  66 f = _G[fun] or error("no " .. fun .. " defined")
  67 print(f(unpack(arg)) or "")
  68
  69 -- eof