Add timing scripts

This commit adds timing scripts from
https://github.com/JasonGross/coq-scripts/tree/master/timing into the
tools folder, and integrates them into coq_makefile and Coq's makefile.
The main added makefile targets are:

- the `TIMING` variable - when non-empty, this creates for each built
  `.v` file a `.v.timing` variable (or `.v.before-timing` or
  `.v.after-timing` for `TIMING=before` and `TIMING=after`, respectively)
- `pretty-timed TGTS=...` - runs `make $(TGTS)` and prints a table of
  sorted timings at the end, saving it to `time-of-build-pretty.log`
- `make-pretty-timed-before TGTS=...`, `make-pretty-timed-after
  TGTS=...` - runs `make $(TGTS)`, and saves the timing data to the file
  `time-of-build-before.log` or `time-of-build-after.log`, respectively
- `print-pretty-timed-diff` - prints a table with the difference between
  the logs recorded by `make-pretty-timed-before` and
  `make-pretty-timed-after`, saving the table to
  `time-of-build-both.log`
- `print-pretty-single-time-diff BEFORE=... AFTER=...` - this prints a
  table with the differences between two `.v.timing` files, and saves
  the output to `time-of-build-pretty.log`
- `*.v.timing.diff` - this saves the result of
  `print-pretty-single-time-diff` for each target to the
  `.v.timing.diff` file
- `all.timing.diff` (`world.timing.diff` and `coq.timing.diff` in Coq's
  own Makefile) - makes all `*.v.timing.diff` targets

N.B. We need to make `make pretty-timed` fail if `make` fails.  To do
this, we need to get around the fact that pipes swallow exit codes.
There are a few solutions in
https://stackoverflow.com/questions/23079651/equivalent-of-pipefail-in-gnu-make;
we choose the temporary file rather than requiring the shell of the
makefile to be bash.

5 files changed, 335 insertions, 4 deletions

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index e4f527d44..7d281977a 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -10,6 +10,7 @@
 INITIAL_VARS := $(.VARIABLES)
 # To implement recursion we save the name of the main Makefile
 SELF := $(lastword $(MAKEFILE_LIST))
+PARENT := $(firstword $(MAKEFILE_LIST))
 
 # This file is generated by coq_makefile and contains many variable
 # definitions, like the list of .v files or the path to Coq
@@ -86,6 +87,11 @@ COQDEP   ?= "$(COQBIN)coqdep"
 GALLINA  ?= "$(COQBIN)gallina"
 COQDOC   ?= "$(COQBIN)coqdoc"
 COQMKTOP ?= "$(COQBIN)coqmktop"
+COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py"
+COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py"
+COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files.py"
+BEFORE ?=
+AFTER ?=
 
 # OCaml binaries
 CAMLC       ?= "$(OCAMLFIND)" ocamlc -c -rectypes -thread
@@ -102,7 +108,15 @@ DESTDIR ?=
 CAMLDEBUG ?=
 COQDEBUG ?=
 
-
+# Option for making timing files
+TIMING?=
+# Output file names for timed builds
+TIME_OF_BUILD_FILE               ?= time-of-build.log
+TIME_OF_BUILD_BEFORE_FILE        ?= time-of-build-before.log
+TIME_OF_BUILD_AFTER_FILE         ?= time-of-build-after.log
+TIME_OF_PRETTY_BUILD_FILE        ?= time-of-build-pretty.log
+TIME_OF_PRETTY_BOTH_BUILD_FILE   ?= time-of-build-both.log
+TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line
 
 ########## End of parameters ##################################################
 # What follows may be relevant to you only if you need to
@@ -171,6 +185,21 @@ COQLIBINSTALL = $(COQLIB)user-contrib
 COQDOCINSTALL = $(DOCDIR)user-contrib
 COQTOPINSTALL = $(COQLIB)toploop
 
+ifneq (,$(TIMING))
+TIMING_ARG=-time
+ifeq (after,$(TIMING))
+TIMING_EXT=after-timing
+else
+ifeq (before,$(TIMING))
+TIMING_EXT=before-timing
+else
+TIMING_EXT=timing
+endif
+endif
+else
+TIMING_ARG=
+endif
+
 # Retro compatibility (DESTDIR is standard on Unix, DESTROOT is not)
 ifneq "$(DSTROOT)" ""
 DESTDIR := $(DSTROOT)
@@ -270,6 +299,41 @@ all:
 	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all
 .PHONY: all
 
+all.timing.diff:
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all.timing.diff TIME_OF_PRETTY_BUILD_EXTRA_FILES=""
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all
+.PHONY: all.timing.diff
+
+make-pretty-timed-before:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_BEFORE_FILE)
+make-pretty-timed-after:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_AFTER_FILE)
+make-pretty-timed make-pretty-timed-before make-pretty-timed-after::
+	$(HIDE)rm -f pretty-timed-success.ok
+	$(HIDE)($(MAKE) --no-print-directory -f "$(PARENT)" $(TGTS) TIMED=1 2>&1 && touch pretty-timed-success.ok) | tee -a $(TIME_OF_BUILD_FILE)
+	$(HIDE)rm pretty-timed-success.ok # must not be -f; must fail if the touch failed
+print-pretty-timed::
+	$(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
+print-pretty-timed-diff::
+	$(HIDE)$(COQMAKE_BOTH_TIME_FILES) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
+ifeq (,$(BEFORE))
+print-pretty-single-time-diff::
+	@echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing'
+	$(HIDE)false
+else
+ifeq (,$(AFTER))
+print-pretty-single-time-diff::
+	@echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing'
+	$(HIDE)false
+else
+print-pretty-single-time-diff::
+	$(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) $(BEFORE) $(AFTER) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
+endif
+endif
+pretty-timed:
+	$(HIDE)$(MAKE) --no-print-directory -f "$(PARENT)" make-pretty-timed
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-timed
+.PHONY: pretty-timed make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff
+
 # Extension points for actions to be performed before/after the all target
 pre-all::
 	@# Extension point
@@ -286,6 +350,9 @@ post-all::
 real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles)
 .PHONY: real-all
 
+real-all.timing.diff: $(VOFILES:.vo=.v.timing.diff)
+.PHONE: real-all.timing.diff
+
 bytefiles: $(CMOFILES) $(CMAFILES)
 .PHONY: bytefiles
 
@@ -459,13 +526,19 @@ clean::
 	$(HIDE)rm -f $(VFILES:.v=.glob)
 	$(HIDE)rm -f $(VFILES:.v=.tex)
 	$(HIDE)rm -f $(VFILES:.v=.g.tex)
+	$(HIDE)rm -f pretty-timed-success.ok
 	$(HIDE)rm -rf html mlihtml
 .PHONY: clean
 
 cleanall:: clean
 	@# Extension point
-	$(SHOW)'CLEAN *.aux'
+	$(SHOW)'CLEAN *.aux *.timing'
 	$(HIDE)rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux)
+	$(HIDE)rm -f $(TIME_OF_BUILD_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE)
+	$(HIDE)rm -f $(VOFILES:.vo=.v.timing)
+	$(HIDE)rm -f $(VOFILES:.vo=.v.before-timing)
+	$(HIDE)rm -f $(VOFILES:.vo=.v.after-timing)
+	$(HIDE)rm -f $(VOFILES:.vo=.v.timing.diff)
 .PHONY: cleanall
 
 archclean::
@@ -534,9 +607,15 @@ $(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix
 	$(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@'
 	$(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -shared -o $@ $<
 
+ifneq (,$(TIMING))
+TIMING_EXTRA = > $<.$(TIMING_EXT)
+else
+TIMING_EXTRA =
+endif
+
 $(VOFILES): %.vo: %.v
 	$(SHOW)COQC $<
-	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $<
+	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $< $(TIMING_EXTRA)
 
 # FIXME ?merge with .vo / .vio ?
 $(GLOBFILES): %.glob: %.v
@@ -546,6 +625,10 @@ $(VFILES:.v=.vio): %.vio: %.v
 	$(SHOW)COQC -quick $<
 	$(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $<
 
+$(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing
+	$(SHOW)PYTHON TIMING-DIFF $<
+	$(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-single-time-diff BEFORE=$*.before-timing AFTER=$*.after-timing TIME_OF_PRETTY_BUILD_FILE="$@"
+
 $(BEAUTYFILES): %.v.beautified: %.v
 	$(SHOW)'BEAUTIFY $<'
 	$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $<
@@ -572,7 +655,7 @@ $(GHTMLFILES): %.g.html: %.v %.glob
 
 # Dependency files ############################################################
 
-ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)
+ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),)
  -include $(ALLDFILES)
 else
  ifeq ($(MAKECMDGOALS),)
diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py
new file mode 100644
index 000000000..a207c2171
--- /dev/null
+++ b/tools/TimeFileMaker.py
@@ -0,0 +1,187 @@
+#!/usr/bin/env python
+from __future__ import with_statement
+import os, sys, re
+
+# This script parses the output of `make TIMED=1` into a dictionary
+# mapping names of compiled files to the number of minutes and seconds
+# that they took to compile.
+
+STRIP_REG = re.compile('^(coq/|contrib/|)(?:theories/|src/)?')
+STRIP_REP = r'\1'
+INFINITY  = '\xe2\x88\x9e'
+
+def reformat_time_string(time):
+    seconds, milliseconds = time.split('.')
+    seconds = int(seconds)
+    minutes, seconds = int(seconds / 60), seconds % 60
+    return '%dm%02d.%ss' % (minutes, seconds, milliseconds)
+
+def get_times(file_name):
+    '''
+    Reads the contents of file_name, which should be the output of
+    'make TIMED=1', and parses it to construct a dict mapping file
+    names to compile durations, as strings.  Removes common prefixes
+    using STRIP_REG and STRIP_REP.
+    '''
+    if file_name == '-':
+        lines = sys.stdin.read()
+    else:
+        with open(file_name, 'r') as f:
+            lines = f.read()
+    reg = re.compile(r'^([^\s]+) \([^\)]*?user: ([0-9\.]+)[^\)]*?\)$', re.MULTILINE)
+    times = reg.findall(lines)
+    if all(time in ('0.00', '0.01') for name, time in times):
+        reg = re.compile(r'^([^\s]*) \([^\)]*?real: ([0-9\.]+)[^\)]*?\)$', re.MULTILINE)
+        times = reg.findall(lines)
+    if all(STRIP_REG.search(name.strip()) for name, time in times):
+        times = tuple((STRIP_REG.sub(STRIP_REP, name.strip()), time) for name, time in times)
+    return dict((name, reformat_time_string(time)) for name, time in times)
+
+def get_single_file_times(file_name):
+    '''
+    Reads the contents of file_name, which should be the output of
+    'coqc -time', and parses it to construct a dict mapping lines to
+    to compile durations, as strings.
+    '''
+    if file_name == '-':
+        lines = sys.stdin.read()
+    else:
+        with open(file_name, 'r') as f:
+            lines = f.read()
+    reg = re.compile(r'^Chars ([0-9]+) - ([0-9]+) ([^ ]+) ([0-9\.]+) secs (.*)$', re.MULTILINE)
+    times = reg.findall(lines)
+    if len(times) == 0: return dict()
+    longest = max(max((len(start), len(stop))) for start, stop, name, time, extra in times)
+    FORMAT = 'Chars %%0%dd - %%0%dd %%s' % (longest, longest)
+    return dict((FORMAT % (int(start), int(stop), name), reformat_time_string(time)) for start, stop, name, time, extra in times)
+
+def make_sorting_key(times_dict, descending=True):
+    def get_key(name):
+        minutes, seconds = times_dict[name].replace('s', '').split('m')
+        def fix_sign(num):
+            return -num if descending else num
+        return (fix_sign(int(minutes)), fix_sign(float(seconds)), name)
+    return get_key
+
+def get_sorted_file_list_from_times_dict(times_dict, descending=True):
+    '''
+    Takes the output dict of get_times and returns the list of keys,
+    sorted by duration.
+    '''
+    return sorted(times_dict.keys(), key=make_sorting_key(times_dict, descending=descending))
+
+def to_seconds(time):
+    '''
+    Converts a string time into a number of seconds.
+    '''
+    minutes, seconds = time.replace('s', '').split('m')
+    sign = -1 if time[0] == '-' else 1
+    return sign * (abs(int(minutes)) * 60 + float(seconds))
+
+def from_seconds(seconds, signed=False):
+    '''
+    Converts a number of seconds into a string time.
+    '''
+    sign = ('-' if seconds < 0 else '+') if signed else ''
+    seconds = abs(seconds)
+    minutes = int(seconds) / 60
+    seconds -= minutes * 60
+    full_seconds = int(seconds)
+    partial_seconds = int(100 * (seconds - full_seconds))
+    return sign + '%dm%02d.%02ds' % (minutes, full_seconds, partial_seconds)
+
+def sum_times(times, signed=False):
+    '''
+    Takes the values of an output from get_times, parses the time
+    strings, and returns their sum, in the same string format.
+    '''
+    return from_seconds(sum(map(to_seconds, times)), signed=signed)
+
+def format_percentage(num, signed=True):
+    sign = ('-' if num < 0 else '+') if signed else ''
+    num = abs(num)
+    whole_part = int(num * 100)
+    frac_part = int(100 * (num * 100 - whole_part))
+    return sign + '%d.%02d%%' % (whole_part, frac_part)
+
+def make_diff_table_string(left_times_dict, right_times_dict,
+                           descending=True,
+                           left_tag="After", tag="File Name", right_tag="Before", with_percent=True,
+                           change_tag="Change", percent_change_tag="% Change"):
+    # We first get the names of all of the compiled files: all files
+    # that were compiled either before or after.
+    all_names_dict = dict()
+    all_names_dict.update(right_times_dict)
+    all_names_dict.update(left_times_dict) # do the left (after) last, so that we give precedence to those ones
+    if len(all_names_dict.keys()) == 0: return 'No timing data'
+    prediff_times = tuple((name, to_seconds(left_times_dict.get(name,'0m0.0s')), to_seconds(right_times_dict.get(name,'0m0.0s')))
+                          for name in all_names_dict.keys())
+    diff_times_dict = dict((name, from_seconds(lseconds - rseconds, signed=True))
+                           for name, lseconds, rseconds in prediff_times)
+    percent_diff_times_dict = dict((name, ((format_percentage((lseconds - rseconds) / rseconds))
+                                           if rseconds != 0 else (INFINITY if lseconds > 0 else 'N/A')))
+                                   for name, lseconds, rseconds in prediff_times)
+    # update to sort by approximate difference, first
+    get_key = make_sorting_key(all_names_dict, descending=descending)
+    all_names_dict = dict((name, (abs(int(to_seconds(diff_times_dict[name]))), get_key(name)))
+                          for name in all_names_dict.keys())
+    names = sorted(all_names_dict.keys(), key=all_names_dict.get)
+    #names = get_sorted_file_list_from_times_dict(all_names_dict, descending=descending)
+    # set the widths of each of the columns by the longest thing to go in that column
+    left_sum = sum_times(left_times_dict.values())
+    right_sum = sum_times(right_times_dict.values())
+    left_sum_float = sum(map(to_seconds, left_times_dict.values()))
+    right_sum_float = sum(map(to_seconds, right_times_dict.values()))
+    diff_sum = from_seconds(left_sum_float - right_sum_float, signed=True)
+    percent_diff_sum = (format_percentage((left_sum_float - right_sum_float) / right_sum_float)
+                        if right_sum_float > 0 else 'N/A')
+    left_width = max(max(map(len, ['N/A'] + list(left_times_dict.values()))), len(left_sum))
+    right_width = max(max(map(len, ['N/A'] + list(right_times_dict.values()))), len(right_sum))
+    far_right_width = max(max(map(len, ['N/A', change_tag] + list(diff_times_dict.values()))), len(diff_sum))
+    far_far_right_width = max(max(map(len, ['N/A', percent_change_tag] + list(percent_diff_times_dict.values()))), len(percent_diff_sum))
+    middle_width = max(map(len, names + [tag, "Total"]))
+    format_string = ("%%(left)-%ds | %%(middle)-%ds | %%(right)-%ds || %%(far_right)-%ds"
+                     % (left_width, middle_width, right_width, far_right_width))
+    if with_percent:
+        format_string += " | %%(far_far_right)-%ds" % far_far_right_width
+    header = format_string % {'left': left_tag, 'middle': tag, 'right': right_tag, 'far_right': change_tag, 'far_far_right': percent_change_tag}
+    total = format_string % {'left': left_sum, 'middle': "Total", 'right': right_sum, 'far_right': diff_sum, 'far_far_right': percent_diff_sum}
+    # separator to go between headers and body
+    sep = '-' * len(header)
+    # the representation of the default value (0), to get replaced by N/A
+    left_rep, right_rep, far_right_rep, far_far_right_rep = ("%%-%ds | " % left_width) % 0, (" | %%-%ds || " % right_width) % 0, ("|| %%-%ds" % far_right_width) % 0, ("| %%-%ds" % far_far_right_width) % 0
+    return '\n'.join([header, sep, total, sep] +
+                     [format_string % {'left': left_times_dict.get(name, 0),
+                                       'middle': name,
+                                       'right': right_times_dict.get(name, 0),
+                                       'far_right': diff_times_dict.get(name, 0),
+                                       'far_far_right': percent_diff_times_dict.get(name, 0)}
+                      for name in names]).replace(left_rep, 'N/A'.center(len(left_rep) - 3) + ' | ').replace(right_rep, ' | ' + 'N/A'.center(len(right_rep) - 7) + ' || ').replace(far_right_rep, '|| ' + 'N/A'.center(len(far_right_rep) - 3)).replace(far_far_right_rep, '| ' + 'N/A'.center(len(far_far_right_rep) - 2))
+
+def make_table_string(times_dict,
+                      descending=True,
+                      tag="Time"):
+    if len(times_dict.keys()) == 0: return 'No timing data'
+    # We first get the names of all of the compiled files, sorted by
+    # duration
+    names = get_sorted_file_list_from_times_dict(times_dict, descending=descending)
+    # compute the widths of the columns
+    times_width = max(max(map(len, times_dict.values())), len(sum_times(times_dict.values())))
+    names_width = max(map(len, names + ["File Name", "Total"]))
+    format_string = "%%-%ds | %%-%ds" % (times_width, names_width)
+    header = format_string % (tag, "File Name")
+    total = format_string % (sum_times(times_dict.values()),
+                             "Total")
+    sep = '-' * len(header)
+    return '\n'.join([header, sep, total, sep] +
+                     [format_string % (times_dict[name],
+                                       name)
+                      for name in names])
+
+def print_or_write_table(table, files):
+    if len(files) == 0 or '-' in files:
+        print(table)
+    for file_name in files:
+        if file_name != '-':
+            with open(file_name, 'w') as f:
+                f.write(table)
diff --git a/tools/make-both-single-timing-files.py b/tools/make-both-single-timing-files.py
new file mode 100755
index 000000000..2d33503c3
--- /dev/null
+++ b/tools/make-both-single-timing-files.py
@@ -0,0 +1,18 @@
+#!/usr/bin/env python
+import sys
+from TimeFileMaker import *
+
+if __name__ == '__main__':
+    USAGE = 'Usage: %s AFTER_FILE_NAME BEFORE_FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0]
+    HELP_STRING = r'''Formats timing information from the output of two invocations of `coqc -time` into a sorted table'''
+    if len(sys.argv) < 3 or '--help' in sys.argv[1:] or '-h' in sys.argv[1:]:
+        print(USAGE)
+        if '--help' in sys.argv[1:] or '-h' in sys.argv[1:]:
+            print(HELP_STRING)
+            if len(sys.argv) == 2: sys.exit(0)
+        sys.exit(1)
+    else:
+        left_dict = get_single_file_times(sys.argv[1])
+        right_dict = get_single_file_times(sys.argv[2])
+        table = make_diff_table_string(left_dict, right_dict, tag="Code")
+        print_or_write_table(table, sys.argv[3:])
diff --git a/tools/make-both-time-files.py b/tools/make-both-time-files.py
new file mode 100755
index 000000000..69ec5a663
--- /dev/null
+++ b/tools/make-both-time-files.py
@@ -0,0 +1,22 @@
+#!/usr/bin/env python
+import sys
+from TimeFileMaker import *
+
+if __name__ == '__main__':
+    USAGE = 'Usage: %s AFTER_FILE_NAME BEFORE_FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0]
+    HELP_STRING = r'''Formats timing information from the output of two invocations of `make TIMED=1` into a sorted table.
+
+The input is expected to contain lines in the format:
+FILE_NAME (...user: NUMBER_IN_SECONDS...)
+'''
+    if len(sys.argv) < 3 or '--help' in sys.argv[1:] or '-h' in sys.argv[1:]:
+        print(USAGE)
+        if '--help' in sys.argv[1:] or '-h' in sys.argv[1:]:
+            print(HELP_STRING)
+            if len(sys.argv) == 2: sys.exit(0)
+        sys.exit(1)
+    else:
+        left_dict = get_times(sys.argv[1])
+        right_dict = get_times(sys.argv[2])
+        table = make_diff_table_string(left_dict, right_dict)
+        print_or_write_table(table, sys.argv[3:])
diff --git a/tools/make-one-time-file.py b/tools/make-one-time-file.py
new file mode 100755
index 000000000..e66136df9
--- /dev/null
+++ b/tools/make-one-time-file.py
@@ -0,0 +1,21 @@
+#!/usr/bin/env python
+import sys
+from TimeFileMaker import *
+
+if __name__ == '__main__':
+    USAGE = 'Usage: %s FILE_NAME [OUTPUT_FILE_NAME ..]' % sys.argv[0]
+    HELP_STRING = r'''Formats timing information from the output of `make TIMED=1` into a sorted table.
+
+The input is expected to contain lines in the format:
+FILE_NAME (...user: NUMBER_IN_SECONDS...)
+'''
+    if len(sys.argv) < 2 or '--help' in sys.argv[1:] or '-h' in sys.argv[1:]:
+        print(USAGE)
+        if '--help' in sys.argv[1:] or '-h' in sys.argv[1:]:
+            print(HELP_STRING)
+            if len(sys.argv) == 2: sys.exit(0)
+        sys.exit(1)
+    else:
+        times_dict = get_times(sys.argv[1])
+        table = make_table_string(times_dict)
+        print_or_write_table(table, sys.argv[2:])