diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 3 | ||||
| -rw-r--r-- | tools/TimeFileMaker.py | 39 | ||||
| -rw-r--r-- | tools/coqdep.ml | 3 |
3 files changed, 29 insertions, 16 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index bd9d8c9221..0236c549d5 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -468,6 +468,9 @@ beautify: $(BEAUTYFILES) # Extensions can't assume when they run. install: + $(HIDE)code=0; for f in $(FILESTOINSTALL); do\ + if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \ + done; exit $$code $(HIDE)for f in $(FILESTOINSTALL); do\ df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ if [ "$$?" != "0" -o -z "$$df" ]; then\ diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py index 854dd25b75..3d07661d56 100644 --- a/tools/TimeFileMaker.py +++ b/tools/TimeFileMaker.py @@ -34,6 +34,24 @@ def reformat_time_string(time): minutes, seconds = divmod(seconds, 60) return '%dm%02d.%ss' % (minutes, seconds, milliseconds) +def get_file_lines(file_name): + if file_name == '-': + if hasattr(sys.stdin, 'buffer'): + lines = sys.stdin.buffer.readlines() + else: + lines = sys.stdin.readlines() + else: + with open(file_name, 'rb') as f: + lines = f.readlines() + for line in lines: + try: + yield line.decode('utf-8') + except UnicodeDecodeError: # invalid utf-8 + pass + +def get_file(file_name): + return ''.join(get_file_lines(file_name)) + def get_times(file_name): ''' Reads the contents of file_name, which should be the output of @@ -41,11 +59,7 @@ def get_times(file_name): names to compile durations, as strings. Removes common prefixes using STRIP_REG and STRIP_REP. ''' - if file_name == '-': - lines = sys.stdin.read() - else: - with open(file_name, 'r', encoding="utf-8") as f: - lines = f.read() + lines = get_file(file_name) reg = re.compile(r'^([^\s]+) \([^\)]*?user: ([0-9\.]+)[^\)]*?\)\s*$', re.MULTILINE) times = reg.findall(lines) if all(time in ('0.00', '0.01') for name, time in times): @@ -61,11 +75,7 @@ def get_single_file_times(file_name): 'coqc -time', and parses it to construct a dict mapping lines to to compile durations, as strings. ''' - if file_name == '-': - lines = sys.stdin.read() - else: - with open(file_name, 'r', encoding="utf-8") as f: - lines = f.read() + lines = get_file(file_name) reg = re.compile(r'^Chars ([0-9]+) - ([0-9]+) ([^ ]+) ([0-9\.]+) secs (.*)$', re.MULTILINE) times = reg.findall(lines) if len(times) == 0: return dict() @@ -209,11 +219,10 @@ def make_table_string(times_dict, def print_or_write_table(table, files): if len(files) == 0 or '-' in files: - try: - binary_stdout = sys.stdout.buffer - except AttributeError: - binary_stdout = sys.stdout - print(table.encode("utf-8"), file=binary_stdout) + if hasattr(sys.stdout, 'buffer'): + sys.stdout.buffer.write(table.encode("utf-8")) + else: + sys.stdout.write(table.encode("utf-8")) for file_name in files: if file_name != '-': with open(file_name, 'w', encoding="utf-8") as f: diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 66f1f257b8..7114965a11 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -563,4 +563,5 @@ let _ = try coqdep () with CoqlibError msg -> - eprintf "*** Error: %s@\n%!" msg + eprintf "*** Error: %s@\n%!" msg; + exit 1 |