aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/CoqMakefile.in6
-rw-r--r--tools/TimeFileMaker.py23
-rwxr-xr-xtools/make-both-single-timing-files.py2
-rwxr-xr-xtools/make-both-time-files.py2
-rwxr-xr-xtools/make-one-time-file.py2
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 *