lint(scripts/lint-style.py): add indentation linter (#10257)

scripts/lint-style.py

@@ -30,6 +30,7 @@
 
 from pathlib import Path
 import sys
+import re
 
 ERR_COP = 0 # copyright header
 ERR_IMP = 1 # import statements
@@ -41,6 +42,7 @@
 ERR_AUT = 7 # malformed authors list
 ERR_OME = 8 # imported tactic.omega
 ERR_TAC = 9 # imported tactic
+WRN_IND = 10 # indentation
 
 exceptions = []
 
@@ -73,6 +75,8 @@
             exceptions += [(ERR_OME, path)]
         if errno == "ERR_TAC":
             exceptions += [(ERR_TAC, path)]
+        if errno == "WRN_IND":
+            exceptions += [(WRN_IND, path)]
 
 new_exceptions = False
 
@@ -149,6 +153,63 @@ def long_lines_check(lines, path):
             errors += [(ERR_LIN, line_nr, path)]
     return errors
 
+def indent_check(lines, path):
+    """Check that tactic blocks are indented correctly.
+    
+    This linter warns whenever a `{` symbol starting a subproof appears wrongly indented in a tactic block.
+    It does not do much parsing, so to avoid false positives it skips some blocks with complicated syntax
+    like nested `begin`/`end` or containing the keywords `calc` or `match`.
+    """
+    errors = []
+    indent_lvl = 0
+    in_prf = 0  # counter for nested proof blocks
+    check_rest_of_block = True  # we only check uncomplicated syntax
+    ended_with_comma = False  # track whether the previous line ends with a comma
+    inside_special = 0  # track whether we are inside ⟨⟩ or []
+    for line_nr, line in enumerate(lines, 1):
+        line = line.split('--')[0] # discard any commented out part of this line
+        if len(line) == 0 or line[-1] != '\n':
+            line += '\n' # add back newline if it just got removed
+        # `lstr` is the line with starting whitespace removed.
+        # Therefore, `len(line) - len(lstr)` is the line's indentation depth.
+        lstr = line.lstrip(' ')
+
+        # Check that `{` starting a subproof has the expected indentation.
+        if in_prf > 0 and check_rest_of_block and ended_with_comma and not inside_special:
+            if lstr[0] == '{' and len(line) - len(lstr) != indent_lvl:
+                errors += [(WRN_IND, line_nr, path)]
+
+        # Update state for next line.
+        ended_with_comma = line.endswith(",\n")
+        # We don't want to lint inside `⟨..⟩` (anonymous constructor) or `[..]` tactic blocks.
+        inside_special += line.count('⟨') + line.count('[') - line.count('⟩') - line.count(']')
+        if line[0] != ' ':
+            # This is either the `end` line of a tactic proof, or the first line of a new declaration.
+            # Reset the state:
+            indent_lvl = 0
+            in_prf = 0
+            check_rest_of_block = True
+            ended_with_comma = False
+            inside_special = 0
+        if re.match("\b(match|calc)\b", line) is not None:
+            check_rest_of_block = False
+        if re.match("\bbegin\b", line) is not None:
+            # Don't check complicated proof block syntax (note, one if uses `line.find` the other `lstr.find`)
+            # in this case, we ignore proof blocks whose outermost-block doesn't begin flush-left
+            if line.find("begin") > 0 and in_prf == 0:
+                check_rest_of_block = False
+            # in this case, we ignore proof blocks where begin is not the first word on the line
+            if lstr.find("begin") > 0:
+                check_rest_of_block = False
+            indent_lvl += 2
+            in_prf += 1
+        if re.match("\bend\b", line) is not None:
+            indent_lvl -= 2
+            in_prf -= 1
+        indent_lvl += 2 * line.count('{') # potential innocent(?) clash with set-builder notation
+        indent_lvl -= 2 * line.count('}') # there can be multiple closing braces on one line
+    return errors
+
 def import_only_check(lines, path):
     import_only_file = True
     errors = []
@@ -232,8 +293,12 @@ def output_message(path, line_nr, code, msg):
         # filename first, then line so that we can call "sort" on the output
         print(f"{path} : line {line_nr} : {code} : {msg}")
     else:
+        if code.startswith("ERR"):
+            msg_type = "error"
+        if code.startswith("WRN"):
+            msg_type = "warning"
         # We are outputting for github. It doesn't appear to surface code, so show it in the message too
-        print(f"::error file={path},line={line_nr},code={code}::{code}: {msg}")
+        print(f"::{msg_type} file={path},line={line_nr},code={code}::{code}: {msg}")
 
 def format_errors(errors):
     global new_exceptions
@@ -261,6 +326,8 @@ def format_errors(errors):
             output_message(path, line_nr, "ERR_OME", "Files in mathlib cannot import tactic.omega")
         if errno == ERR_TAC:
             output_message(path, line_nr, "ERR_TAC", "Files in mathlib cannot import the whole tactic folder")
+        if errno == WRN_IND:
+            output_message(path, line_nr, "WRN_IND", "Probable indentation mistake in proof")
 
 def lint(path):
     with path.open(encoding="utf-8") as f:
@@ -281,6 +348,8 @@ def lint(path):
         format_errors(errs)
         errs = import_omega_check(lines, path)
         format_errors(errs)
+        errs = indent_check(lines, path)
+        format_errors(errs)
 
 for filename in sys.argv[1:]:
     lint(Path(filename))