Python script taking a log of `make` on stdin, which adds imports to fix numeral notations
#!/usr/bin/env python2 | |
from __future__ import with_statement | |
import sys, re | |
MODULES = {'string': 'Coq.Strings.String', | |
'ascii': 'Coq.Strings.Ascii', | |
'Z': 'Coq.ZArith.BinIntDef', | |
'positive': 'Coq.PArith.BinPosDef', | |
'N': 'Coq.NArith.BinNatDef', | |
'R': 'Coq.Reals.Rdefinitions', | |
'int31': 'Coq.Numbers.Cyclic.Int31.Int31'} | |
def get_file_name(err): | |
return re.findall(r'^"([^"]*)"', err)[0] | |
def norm_type(ty): | |
return ty.split('.')[-1] | |
def get_type(err): | |
if 'No interpretation for string' in err: return 'string' | |
for pat in (r'Found a constructor of inductive type [^ ]* while a constructor of ([^ ]*) is expected', | |
r'expected to have type "([^"]*)"'): | |
found = re.findall(pat, err) | |
if found: return found[0] | |
return tuple()[0] | |
if __name__ == '__main__': | |
log = sys.stdin.read() | |
errors = [i for i in log.split('\nFile ')[1:] if 'Error:' in i] | |
for err in errors: | |
try: | |
err_oneline = err.replace('\n', ' ').replace(' ', ' ') | |
fname = get_file_name(err_oneline) | |
ty = norm_type(get_type(err_oneline)) | |
imp = 'Import ' + MODULES[ty] + '.' | |
req = 'Require ' + imp + '\n' | |
# we add an extra newline at the beginning to catch 'Require ...' at the beginning of the file | |
with open(fname, 'r') as f: contents = '\n' + f.read() | |
if req not in contents: | |
if '\nRequire ' in contents: | |
contents = contents.split('\nRequire ') | |
contents = '\nRequire '.join([contents[0], imp] + contents[1:]) | |
contents = contents[1:] # strip extra \n added at the beginning | |
else: | |
contents = contents[1:] # strip extra \n added at the beginning | |
contents = req + contents | |
with open(fname, 'w') as f: f.write(contents) | |
except IndexError: | |
print('Could not interpret error message:\n' + err) | |
except IOError as e: | |
print('On ' + fname + ':\n' + repr(e)) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment