def format_errors()

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")