chore: speed up lint.py and run in parallel with other tests (#14172)

This PR modifies `lint.py` to only look at files tracked by git, not all
files. Previously, the old lint script would occasionally fail when
running in parallel with the other tests, but this change should prevent
those failures.

Also, this PR improves the performance by roughly an order of magnitude.

Author: Garmelon

tests/CMakeLists.txt

@@ -302,9 +302,7 @@ foreach(T ${LEANLAKETESTS})
 endforeach(T)
 
 # Lint test suite and parts of the repository.
-# Must not run in parallel with any other tests that may create or delete files.
 add_test(NAME lint.py COMMAND python3 lint.py WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}")
-set_tests_properties(lint.py PROPERTIES RUN_SERIAL TRUE)
 
 add_test_pile(../doc/examples *.lean)
 add_test_pile(compile *.lean BENCH PART2)

tests/lint.py

@@ -1,13 +1,44 @@
 #!/usr/bin/env python3
 
+import glob as glob_
 import os
+import re
+import subprocess
 import sys
 from pathlib import Path
 
 # Run in repo root
 os.chdir(Path(__file__).parent.parent)
 
 
+# We only inspect files tracked by git, and those should never be modified by
+# tests, so this should safely run in parallel with other tests.
+TRACKED_LIST = sorted(
+    name
+    for name in subprocess.run(
+        ["git", "ls-files", "-z"],
+        capture_output=True,
+        text=True,
+        check=True,
+    ).stdout.split("\0")
+    if name
+)
+TRACKED_SET = {Path(name) for name in TRACKED_LIST}
+
+
+def glob(*patterns: str):
+    # `Path.full_match` recompiles the pattern on every call, which makes this
+    # script a lot slower than it needs to be.
+    compiled = [
+        re.compile(glob_.translate(pattern, recursive=True, include_hidden=True))
+        for pattern in patterns
+    ]
+
+    for name in TRACKED_LIST:
+        if any(regex.match(name) for regex in compiled):
+            yield Path(name)
+
+
 ERROR = False
 
 
@@ -20,7 +51,7 @@ def nag(reason: str, path: Path, fatal: bool = True) -> None:
 
 # Files and directories that will no longer work.
 
-for pattern in (
+for file in glob(
     "**/*.exit.expected",
     "**/*.expected.out",
     "**/*.expected.ret",
@@ -29,32 +60,24 @@ def nag(reason: str, path: Path, fatal: bool = True) -> None:
     "**/run_test",
     "tests/speedcenter.exec.velcom.yaml",
 ):
-    for file in Path().glob(pattern):
-        nag("removed file", file)
-
-for dir in (
-    "tests/bench-radar",
-    "tests/bench/cbv",
-    "tests/bench/inundation",
-    "tests/compiler",
-    "tests/lean/docparse",
-    "tests/lean/interactive",
-    "tests/lean/run",
-    "tests/lean/server",
-    "tests/lean/trust0",
-    "tests/plugin",
+    nag("removed file", file)
+
+for file in glob(
+    "tests/bench-radar/*",
+    "tests/bench/cbv/*",
+    "tests/bench/inundation/*",
+    "tests/compiler/*",
+    "tests/lean/docparse/*",
+    "tests/lean/interactive/*",
+    "tests/lean/run/*",
+    "tests/lean/server/*",
+    "tests/lean/trust0/*",
+    "tests/plugin/*",
+    "tests/lean/*.lean",
+    "tests/lean/*.expected.out",
+    "tests/lean/*.expected.ret",
 ):
-    for file in Path().glob(f"{dir}/*"):
-        nag("removed dir", file)
-
-for dir in ("tests/lean",):
-    for pattern in (
-        f"{dir}/*.lean",
-        f"{dir}/*.expected.out",
-        f"{dir}/*.expected.ret",
-    ):
-        for file in Path().glob(pattern):
-            nag("removed dir", file)
+    nag("removed dir", file)
 
 
 # Files that use the old naming convention in the new directories.
@@ -72,13 +95,12 @@ def nag(reason: str, path: Path, fatal: bool = True) -> None:
     "tests/server",
     "tests/server_interactive",
 ):
-    for pattern in (
+    for file in glob(
         f"{dir}/*.no_interpreter",
         f"{dir}/*.expected.out",
         f"{dir}/*.expected.ret",
     ):
-        for file in Path().glob(pattern):
-            nag("old suffix", file)
+        nag("old suffix", file)
 
 
 # Files that expect a corresponding base file
@@ -106,11 +128,11 @@ def nag(reason: str, path: Path, fatal: bool = True) -> None:
     ("**/*.out.expected", 2),
     ("**/*.out.ignored", 2),
 ):
-    for file in Path().glob(pattern):
+    for file in glob(pattern):
         basefile = file
         for _ in range(drop):
             basefile = basefile.with_suffix("")
-        if basefile.exists():
+        if basefile in TRACKED_SET:
             continue
         if basefile == Path(
             "tests/pkg/leanchecker/LeanCheckerTests/PrivateConflictC.lean.fresh"
@@ -121,54 +143,52 @@ def nag(reason: str, path: Path, fatal: bool = True) -> None:
 
 # Files that shouldn't be empty
 
-for pattern in (
+for file in glob(
     "**/*.init.sh",
     "**/*.before.sh",
     "**/*.after.sh",
 ):
-    for file in Path().glob(pattern):
-        if file.read_text().strip():
-            continue
-        nag("empty", file)
+    if file.read_text().strip():
+        continue
+    nag("empty", file)
 
 # We need to be a bit more peculiar about whitespace here
-for file in Path().glob("**/*.out.expected"):
+for file in glob("**/*.out.expected"):
     if file.read_bytes():
         continue
     nag("empty", file)
 
 
 # .out.ignored and .out.expected collision
 
-for file in Path().glob("**/*.out.ignored"):
-    if file.with_suffix(".expected").exists():
+for file in glob("**/*.out.ignored"):
+    if file.with_suffix(".expected") in TRACKED_SET:
         nag("has .expected", file)
 
 
 # .no_test but .out.expected/.out.ignored
 
-for file in Path().glob("**/*.no_test"):
-    if file.with_suffix(".out.expected").exists():
+for file in glob("**/*.no_test"):
+    if file.with_suffix(".out.expected") in TRACKED_SET:
         nag("has .no_test", file)
-    if file.with_suffix(".out.ignored").exists():
+    if file.with_suffix(".out.ignored") in TRACKED_SET:
         nag("has .no_test", file)
 
 
 # Special rules for certain directories
 
-for pattern in (
+for file in glob(
     "tests/compile_bench/*.no_bench",
     "tests/elab_bench/*.no_bench",
     "tests/misc_bench/*.no_bench",
 ):
-    for file in Path().glob(pattern):
-        nag("forbidden", file)
+    nag("forbidden", file)
 
 
 # File confusion by case insensitive filesystems
 
 seen: set[str] = set()
-for file in Path().glob("**/*"):
+for file in glob("**/*"):
     path = str(file).lower()
     if path in seen:
         nag("case sensitive", file)