in lean/scripts/lint_style.py [0:0]
def format_errors(errors):
global new_exceptions
for errno, line_nr, path in errors:
if (errno, path.resolve()) in exceptions:
continue
new_exceptions = True
if errno == ERR_COP:
output_message(path, line_nr, "ERR_COP",
"Malformed or missing copyright header")
if errno == ERR_IMP:
output_message(path, line_nr, "ERR_IMP",
"More than one file imported per line")
if errno == ERR_MOD:
output_message(path, line_nr, "ERR_MOD",
"Module docstring missing, or too late")
if errno == ERR_LIN:
output_message(path, line_nr, "ERR_LIN",
"Line has more than 100 characters")
if errno == ERR_SAV:
output_message(path, line_nr, "ERR_SAV",
"File contains the character ᾰ")
if errno == ERR_RNT:
output_message(path, line_nr, "ERR_RNT",
"Reserved notation outside tactic.reserved_notation")
if errno == ERR_OPT:
output_message(path, line_nr, "ERR_OPT",
"Forbidden set_option command")
if errno == ERR_AUT:
output_message(path, line_nr, "ERR_AUT",
"Authors line should look like: 'Authors: Jean Dupont, Иван Иванович Иванов'")
if errno == ERR_TSP:
output_message(path, line_nr, "ERR_TSP",
"Tailing space detected")
if errno == ERR_SOR:
output_message(path, line_nr, "ERR_SOR",
"Sorry should not be followed by comma")
if errno == ERR_PSP:
output_message(path, line_nr, "ERR_PSP",
"'( ' or ' )' detected")
if errno == ERR_EOF:
output_message(path, line_nr, "ERR_EOF",
"missing \\n at the end of file")