diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 6 | ||||
| -rw-r--r-- | tools/TimeFileMaker.py | 23 | ||||
| -rwxr-xr-x | tools/make-both-single-timing-files.py | 2 | ||||
| -rwxr-xr-x | tools/make-both-time-files.py | 2 | ||||
| -rwxr-xr-x | tools/make-one-time-file.py | 2 |
5 files changed, 19 insertions, 16 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 7aa2d0a5a..2ebe4aba7 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -91,9 +91,9 @@ COQDOC ?= "$(COQBIN)coqdoc" COQMKFILE ?= "$(COQBIN)coq_makefile" # Timing scripts -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" +COQMAKE_ONE_TIME_FILE ?= PYTHONIOENCODING=UTF-8 "$(COQLIB)/tools/make-one-time-file.py" +COQMAKE_BOTH_TIME_FILES ?= PYTHONIOENCODING=UTF-8 "$(COQLIB)/tools/make-both-time-files.py" +COQMAKE_BOTH_SINGLE_TIMING_FILES ?= PYTHONIOENCODING=UTF-8 "$(COQLIB)/tools/make-both-single-timing-files.py" BEFORE ?= AFTER ?= diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py index 0d24332f1..ad001012a 100644 --- a/tools/TimeFileMaker.py +++ b/tools/TimeFileMaker.py @@ -1,6 +1,8 @@ -#!/usr/bin/env python from __future__ import with_statement +from __future__ import division +from __future__ import unicode_literals import os, sys, re +from io import open # This script parses the output of `make TIMED=1` into a dictionary # mapping names of compiled files to the number of minutes and seconds @@ -8,7 +10,7 @@ import os, sys, re STRIP_REG = re.compile('^(coq/|contrib/|)(?:theories/|src/)?') STRIP_REP = r'\1' -INFINITY = '\xe2\x88\x9e' +INFINITY = '\u221e' def parse_args(argv, USAGE, HELP_STRING): sort_by = 'auto' @@ -27,7 +29,7 @@ def parse_args(argv, USAGE, HELP_STRING): def reformat_time_string(time): seconds, milliseconds = time.split('.') seconds = int(seconds) - minutes, seconds = int(seconds / 60), seconds % 60 + minutes, seconds = divmod(seconds, 60) return '%dm%02d.%ss' % (minutes, seconds, milliseconds) def get_times(file_name): @@ -40,7 +42,7 @@ def get_times(file_name): if file_name == '-': lines = sys.stdin.read() else: - with open(file_name, 'r') as f: + with open(file_name, 'r', encoding="utf-8") as f: lines = f.read() reg = re.compile(r'^([^\s]+) \([^\)]*?user: ([0-9\.]+)[^\)]*?\)\s*$', re.MULTILINE) times = reg.findall(lines) @@ -60,7 +62,7 @@ def get_single_file_times(file_name): if file_name == '-': lines = sys.stdin.read() else: - with open(file_name, 'r') as f: + with open(file_name, 'r', encoding="utf-8") as f: lines = f.read() reg = re.compile(r'^Chars ([0-9]+) - ([0-9]+) ([^ ]+) ([0-9\.]+) secs (.*)$', re.MULTILINE) times = reg.findall(lines) @@ -101,7 +103,7 @@ def from_seconds(seconds, signed=False): ''' sign = ('-' if seconds < 0 else '+') if signed else '' seconds = abs(seconds) - minutes = int(seconds) / 60 + minutes = int(seconds) // 60 seconds -= minutes * 60 full_seconds = int(seconds) partial_seconds = int(100 * (seconds - full_seconds)) @@ -112,7 +114,8 @@ 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) + # sort the times before summing because floating point addition is not associative + return from_seconds(sum(sorted(map(to_seconds, times))), signed=signed) def format_percentage(num, signed=True): sign = ('-' if num < 0 else '+') if signed else '' @@ -153,8 +156,8 @@ def make_diff_table_string(left_times_dict, right_times_dict, # 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())) + left_sum_float = sum(sorted(map(to_seconds, left_times_dict.values()))) + right_sum_float = sum(sorted(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') @@ -206,5 +209,5 @@ def print_or_write_table(table, files): print(table) for file_name in files: if file_name != '-': - with open(file_name, 'w') as f: + with open(file_name, 'w', encoding="utf-8") as f: f.write(table) diff --git a/tools/make-both-single-timing-files.py b/tools/make-both-single-timing-files.py index c6af2ff1f..32c52c7a1 100755 --- a/tools/make-both-single-timing-files.py +++ b/tools/make-both-single-timing-files.py @@ -1,4 +1,4 @@ -#!/usr/bin/env python2 +#!/usr/bin/env python import sys from TimeFileMaker import * diff --git a/tools/make-both-time-files.py b/tools/make-both-time-files.py index 643429679..f730a8d6b 100755 --- a/tools/make-both-time-files.py +++ b/tools/make-both-time-files.py @@ -1,4 +1,4 @@ -#!/usr/bin/env python2 +#!/usr/bin/env python import sys from TimeFileMaker import * diff --git a/tools/make-one-time-file.py b/tools/make-one-time-file.py index c9905249e..e66136df9 100755 --- a/tools/make-one-time-file.py +++ b/tools/make-one-time-file.py @@ -1,4 +1,4 @@ -#!/usr/bin/env python2 +#!/usr/bin/env python import sys from TimeFileMaker import * |