Handy short cut for formatting elapsed time in floating point seconds

[Paul McGuire]

I am doing some simple timing of some elements of Python scripts, and
the simplest is to just call time.time() before and after key elements
of the script:

t1 = time.time()

# do lengthy operation

t2 = time.time()
print "That took %f seconds" % (t2-t1)

Unfortunately, this gives very ugly timing output, as just a floating
point number of seconds.  After several iterations of writing a
formatter (strftime is not straightforward to use - it omits
milliseconds for one thing), I came up with this:

def secondsToStr(t):
    rediv = lambda ll,b : list(divmod(ll[0],b)) + ll[1:]
    return "%d:%02d:%02d.%03d" % tuple(reduce(rediv,[[t*1000,],
1000,60,60]))

Now I can write:

print "That took", secondsToStr(t2-t1),"seconds"

and get nicely-formatted 0:00:12.345 style output.

(I also posted this to the Python Cookbook.)

-- Paul