one more step toward release and bench reorganization

diff --git a/components/binaries/Makefile b/components/binaries/Makefile
new file mode 100644 (file)
index 0000000..523fce7
--- /dev/null
+++ b/components/binaries/Makefile
@@ -0,0 +1,15 @@
+H=@
+
+BINARIES=extractor  table_creator  utilities
+
+all: $(BINARIES:%=rec@all@%) 
+opt: $(BINARIES:%=rec@opt@%)
+depend: $(BINARIES:%=rec@depend@%)
+depend.opt: $(BINARIES:%=rec@depend.opt@%)
+install: $(BINARIES:%=rec@install@%)
+uninstall: $(BINARIES:%=rec@uninstall@%)
+clean: $(BINARIES:%=rec@clean@%) 
+
+rec@%:
+       $(H)$(MAKE) -C $(word 2, $(subst @, ,$*)) $(word 1, $(subst @, ,$*))
+

diff --git a/components/binaries/utilities/.depend b/components/binaries/utilities/.depend
new file mode 100644 (file)
index 0000000..e69de29

diff --git a/matita/library/makefile b/matita/library/makefile
new file mode 100644 (file)
index 0000000..39d64a9
--- /dev/null
+++ b/matita/library/makefile
@@ -0,0 +1,33 @@
+H=@
+
+RT_BASEDIR=../
+OPTIONS=-bench
+MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS)
+CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) 
+MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS)
+CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS) 
+
+devel:=$(shell basename `pwd`)
+
+all: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel)
+clean: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel)
+cleanall: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all
+
+all.opt opt: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel)
+clean.opt: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel)
+cleanall.opt: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all
+
+%.mo: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@
+%.mo.opt: preall
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@
+       
+preall:
+       $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel)
+

diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml
index 7efad77212b3191d2d490253e8559f5e9e945385..923354cbda7058c4a7c4635594b301cc5564ee81 100644 (file)
--- a/matita/matitacLib.ml
+++ b/matita/matitacLib.ml
@@ -83,7 +83,9 @@ let run_script is eval_function  =
 let fname () =
   match Helm_registry.get_list Helm_registry.string "matita.args" with
   | [x] -> x
-  | _ -> MatitaInit.die_usage ()
+  | l -> 
+      prerr_endline ("Wrong commands: " ^ String.concat " " l);
+      MatitaInit.die_usage ()
 
 let pp_ocaml_mode () = 
   HLog.message "";
@@ -160,7 +162,7 @@ let pp_times fname bench_mode rc big_bang =
       let r = Unix.gettimeofday () -. big_bang in
       let extra = try Sys.getenv "BENCH_EXTRA_TEXT" with Not_found -> "" in
       let cc = 
-        if Str.string_match (Str.regexp "opt$") Sys.argv.(0) 0 then 
+        if Str.string_match (Str.regexp ".*opt$") Sys.argv.(0) 0 then 
           "matitac.opt" 
         else 
           "matitac" 
@@ -172,7 +174,7 @@ let pp_times fname bench_mode rc big_bang =
           let cents = int_of_float ((t -. floor t) *. 100.0) in
           let minutes = seconds / 60 in
           let seconds = seconds mod 60 in
-          Printf.sprintf "%2dm%02d.%02ds" minutes seconds cents
+          Printf.sprintf "%dm%02d.%02ds" minutes seconds cents
         in
         Printf.sprintf "%s %s %s" (fmt r) (fmt u) (fmt s)
       in
@@ -186,7 +188,7 @@ let pp_times fname bench_mode rc big_bang =
             String.sub fname rootlen (fnamelen - rootlen)           
       in
       let s = 
-        Printf.sprintf "%s\t%-30s   %s\t%s\t%s" cc fname rc times extra 
+        Printf.sprintf "%s %-35s %-4s %s %s" cc fname rc times extra 
       in
       print_endline s;
       flush stdout

diff --git a/matita/matitamakeLib.ml b/matita/matitamakeLib.ml
index 6af0414afd4aca056425187b13863b69cb2eb172..490e753e86abd853d37b672a424c8d7f21e581b9 100644 (file)
--- a/matita/matitamakeLib.ml
+++ b/matita/matitamakeLib.ml
@@ -175,11 +175,13 @@ let make chdir args =
       
 let call_make ?matita_flags development target make =
   let matita_flags = 
-    match matita_flags with 
-    | None -> 
-        (try Sys.getenv "MATITA_FLAGS" with Not_found -> 
-           if Helm_registry.get_bool "matita.bench" then "-bench" else "")
-    | Some s -> s 
+    let already_defined = 
+      match matita_flags with 
+      | None -> (try Sys.getenv "MATITA_FLAGS" with Not_found -> "")
+      | Some s -> s 
+    in
+    already_defined ^ 
+      if Helm_registry.get_bool "matita.bench" then "-bench" else ""
   in
   rebuild_makefile development;
   let makefile = makefile_for_development development in
@@ -190,15 +192,11 @@ let call_make ?matita_flags development target make =
   let flags = flags @ if nodb then ["NODB=true"] else [] in
   let flags =
     try
-      flags @ [ sprintf "MATITA_FLAGS=%s" matita_flags ]
+      flags @ [ sprintf "MATITA_FLAGS=\"%s\"" matita_flags ]
     with Not_found -> flags in
   let args = 
     ["--no-print-directory"; "-s"; "-k"; "-f"; makefile; target] @ flags 
   in
-(*
-  prerr_endline 
-    ("callink make from "^development.root^" args: "^String.concat " " args);
-*)
   make development.root args
       
 let build_development ?matita_flags ?(target="all") development =
@@ -240,7 +238,7 @@ let mk_maker refresh_cb =
     let err_r,err_w = Unix.pipe () in
     let pid = ref ~-1 in
     ignore(Sys.signal Sys.sigchld (Sys.Signal_ignore));
-    try 
+    try
       let argv = Array.of_list ("make"::args) in
       pid := Unix.create_process "make" argv Unix.stdin out_w err_w;
       Unix.close out_w;

diff --git a/matita/scripts/bench.sql b/matita/scripts/bench.sql
index a45508548bab6b7ba929cb3e624332234ba597cf..2a49a2d01cd327111c199c9bd7b75d63dbd4af58 100644 (file)
--- a/matita/scripts/bench.sql
+++ b/matita/scripts/bench.sql
@@ -1,9 +1,9 @@
 DROP TABLE bench;
 
 CREATE TABLE bench (
-       mark VARCHAR(100) NOT NULL,
-       time VARCHAR(8) NOT NULL,
-       timeuser VARCHAR(8) NOT NULL,
+       mark VARCHAR(30) NOT NULL,
+       time BIGINT NOT NULL,
+       timeuser BIGINT NOT NULL,
        compilation ENUM('byte','opt') NOT NULL,
        test VARCHAR(100) NOT NULL,
        result ENUM('ok','fail') NOT NULL,

diff --git a/matita/scripts/functions.lua b/matita/scripts/functions.lua
new file mode 100755 (executable)
index 0000000..33b945d
--- /dev/null
+++ b/matita/scripts/functions.lua
@@ -0,0 +1,69 @@
+#!/usr/bin/lua5.1
+
+local tool_re = "^([%w%.]+)"
+local test_re = "([%w%./_]+)"
+local rc_re = "([%a]+)"
+local time_re = "(%d+m%d+%.%d+s)"
+local mark_re = "(%d+)"
+local opt_re = "(gc%-%a+)$"
+local sep = "%s+"
+
+local fmt = "INSERT bench "..
+       "(result, compilation, test, time, timeuser, mark, options) "..
+       "VALUES ('%s', '%s', '%s', %d, %d, '%s', '%s');\n"
+
+-- build the huge regex
+local re = tool_re .. sep .. test_re .. sep .. rc_re .. sep .. 
+       time_re .. sep ..time_re .. sep ..time_re .. sep .. 
+       mark_re .. sep .. opt_re 
+
+-- the string to cents of seconds function
+function convert(s)
+       local _,_,min,sec,cents = string.find(s,"(%d+)m(%d+)%.(%d+)s")
+       return min * 6000 + sec * 100 + cents
+end
+
+-- logfile to sql conversion
+function log2sql(file)
+local t = {}
+local f = io.stdin
+if file ~= "-" then 
+       f = io.open(file,"r")
+end
+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)
+       end
+
+       -- check the result is valid
+       if tool ~= "matitac" and tool ~= "matitac.opt" then
+               error("unknown tool " .. tool)
+       else
+               if tool == "matitac" then tool = "byte" else tool = "opt" end
+       end
+       if rc ~= "OK" and rc ~= "FAIL" then
+               error("unknown result " .. rc)
+       else
+               rc = string.lower(rc)
+       end
+       if opt ~= "gc-on" and opt ~= "gc-off" then
+               error("unknown option "..opt)
+       end
+       real = convert(real)
+       user = convert(user)
+
+       -- print the sql statement
+       table.insert(t,string.format(fmt,rc,tool,test,real,user,mark,opt))
+end
+return table.concat(t)
+end
+
+-- call the desired function and print the result
+fun = arg[1]
+table.remove(arg,1)
+f = _G[fun] or error("no " .. fun .. " defined")
+print(f(unpack(arg)) or "")
+
+-- eof