From: Enrico Tassi Date: Thu, 16 Mar 2006 09:39:00 +0000 (+0000) Subject: one more step toward release and bench reorganization X-Git-Tag: 0.4.95@7852~1603 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6e81ede3341e2e4c748068038daece21cfff431f;p=helm.git one more step toward release and bench reorganization --- diff --git a/components/binaries/Makefile b/components/binaries/Makefile new file mode 100644 index 000000000..523fce7e7 --- /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 index 000000000..e69de29bb diff --git a/matita/library/makefile b/matita/library/makefile new file mode 100644 index 000000000..39d64a952 --- /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 7efad7721..923354cbd 100644 --- 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 6af0414af..490e753e8 100644 --- 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 a45508548..2a49a2d01 100644 --- 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 index 000000000..33b945dbd --- /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