File: make-both-single-timing-files.py

package info (click to toggle)
coq 8.16.1%2Bdfsg-1
  • links: PTS, VCS
  • area: main
  • in suites: bookworm
  • size: 40,596 kB
  • sloc: ml: 219,376; sh: 3,545; python: 3,231; ansic: 2,529; makefile: 767; lisp: 279; javascript: 63; xml: 24; sed: 2
file content (20 lines) | stat: -rwxr-xr-x 891 bytes parent folder | download | duplicates (2)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
#!/usr/bin/python3

import sys
sys.path.insert(1, '/usr/lib/coq-core/tools')
from TimeFileMaker import *

if __name__ == '__main__':
    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)