diff options
Diffstat (limited to 'tools/make-both-single-timing-files.py')
| -rwxr-xr-x | tools/make-both-single-timing-files.py | 21 |
1 files changed, 13 insertions, 8 deletions
diff --git a/tools/make-both-single-timing-files.py b/tools/make-both-single-timing-files.py index fddf75f39f..a28da43043 100755 --- a/tools/make-both-single-timing-files.py +++ b/tools/make-both-single-timing-files.py @@ -1,12 +1,17 @@ #!/usr/bin/env python3 -import sys from TimeFileMaker import * if __name__ == '__main__': - USAGE = 'Usage: %s [--sort-by=auto|absolute|diff] 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''' - sort_by, args = parse_args(sys.argv, USAGE, HELP_STRING) - left_dict = get_single_file_times(args[1]) - right_dict = get_single_file_times(args[2]) - table = make_diff_table_string(left_dict, right_dict, tag="Code", sort_by=sort_by) - print_or_write_table(table, args[3:]) + parser = argparse.ArgumentParser(description=r'''Formats timing information from the output of two invocations of `coqc -time` into a sorted table''') + add_sort_by(parser) + add_user(parser, single_timing=True) + add_fuzz(parser) + add_after_file_name(parser) + add_before_file_name(parser) + add_output_file_name(parser) + args = parser.parse_args() + left_dict = get_single_file_times(args.AFTER_FILE_NAME, use_real=args.real) + right_dict = get_single_file_times(args.BEFORE_FILE_NAME, use_real=args.real) + left_dict, right_dict = adjust_fuzz(left_dict, right_dict, fuzz=args.fuzz) + table = make_diff_table_string(left_dict, right_dict, tag="Code", sort_by=args.sort_by) + print_or_write_table(table, args.OUTPUT_FILE_NAME) |