def format_time(decimal_seconds):
    """Format seconds into HH:MM:SS.mmm format.
    e.g. 100.5 => 00:01:40.500
    """
    seconds = int(decimal_seconds)
    milliseconds = int((decimal_seconds - seconds) * 1000)
    hours = seconds // 3600
    minutes = (seconds % 3600) // 60
    seconds = seconds % 60
    return '%d:%02d:%02d.%03d' % (hours, minutes, seconds, milliseconds)