tools: times.sh: show more information in stdout (while still printing it to the log), compute averages of runs, automatically compile and run "times" binary after generating the log.