Skip to content

Instantly share code, notes, and snippets.

@JasonGross JasonGross/

Last active May 20, 2020
What would you like to do?
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 =
errors = [i for i in log.split('\nFile ')[1:] if 'Error:' in i]
for err in errors:
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' +
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
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
You can’t perform that action at this time.