in lean/scripts/lint_style.py [0:0]
def regular_check(lines, path):
errors = []
copy_started = False
copy_done = False
copy_start_line_nr = 0
copy_lines = ""
for line_nr, line in enumerate(lines, 1):
if not copy_started and line == "\n":
errors += [(ERR_COP, copy_start_line_nr, path)]
continue
if not copy_started and line == "/-\n":
copy_started = True
copy_start_line_nr = line_nr
continue
if not copy_started:
errors += [(ERR_COP, line_nr, path)]
if copy_started and not copy_done:
copy_lines += line
if "Author" in line:
# Validating names is not a reasonable thing to do,
# so we just look for the two common variations:
# using ' and ' between names, and a '.' at the end of line.
if ((not line.startswith("Authors: ")) or
(" " in line) or
(" and " in line) or
(line[-2] == '.')):
errors += [(ERR_AUT, line_nr, path)]
if line == "-/\n":
if ((not "Copyright" in copy_lines) or
(not "Apache" in copy_lines) or
(not "Authors: " in copy_lines)):
errors += [(ERR_COP, copy_start_line_nr, path)]
copy_done = True
continue
if copy_done and line == "\n":
continue
words = line.split()
if words[0] != "import" and words[0] != "/-!":
# errors += [(ERR_MOD, line_nr, path)]
break
if words[0] == "/-!":
break
# final case: words[0] == "import"
if len(words) > 2:
if words[2] != "--":
errors += [(ERR_IMP, line_nr, path)]
return errors