lint_style_sanity_test.py
#!/usr/bin/env python3
from pathlib import Path
from shutil import copy
from tempfile import NamedTemporaryFile, TemporaryDirectory
from textwrap import dedent
import subprocess
import unittest
SCRIPTS_DIR = Path(__file__).parent.resolve()
ROOT_DIR = SCRIPTS_DIR.parent
class TestLinterIntegration(unittest.TestCase):
def test_path_combinations(self):
"""
The linter can be run with absolute or relative paths.
This works both for the executable itself as well as any provided
files.
"""
new_file = ROOT_DIR / "src/somenewfile.lean"
self.assertFalse(new_file.is_file())
new_file.write_text("example : 2 = 2\n")
self.addCleanup(new_file.unlink)
exceptions = SCRIPTS_DIR.joinpath("style-exceptions.txt")
self.assertTrue(exceptions.is_file)
self.addCleanup(exceptions.write_text, exceptions.read_text())
subprocess.run(
["./scripts/update-style-exceptions.sh"],
check=True,
capture_output=True,
cwd=ROOT_DIR,
)
combinations = [
(
("relative", "./lint-style.py"),
("relative", "../src/somenewfile.lean"),
("cwd", SCRIPTS_DIR),
), (
("relative", "./lint-style.py"),
("absolute", (ROOT_DIR / "src/somenewfile.lean").resolve()),
("cwd", SCRIPTS_DIR),
), (
("absolute", (SCRIPTS_DIR / "lint-style.py").resolve()),
("relative", "../src/somenewfile.lean"),
("cwd", SCRIPTS_DIR),
), (
("absolute", (SCRIPTS_DIR / "lint-style.py").resolve()),
("absolute", (ROOT_DIR / "src/somenewfile.lean").resolve()),
("cwd", SCRIPTS_DIR),
), (
("absolute", (SCRIPTS_DIR / "lint-style.py").resolve()),
("absolute", (ROOT_DIR / "src/somenewfile.lean").resolve()),
("cwd", Path.home()),
),
]
for (
(linter_kind, linter_path),
(file_kind, file_path),
(_, cwd),
) in combinations:
with self.subTest(
linter_kind=linter_kind,
file_kind=file_kind,
cwd=cwd,
):
subprocess.run([linter_path, file_path], check=True, cwd=cwd)
def test_it_fails_for_missing_copyright_headers(self):
"""
Failing to include a copyright header at the top of a file warns.
"""
with NamedTemporaryFile(suffix=".lean") as file:
file.write(b"example : 37 = 37\n")
file.flush()
result = subprocess.run(
[SCRIPTS_DIR / "lint-style.py", file.name],
capture_output=True,
)
self.assertIn(b"ERR_COP", result.stdout)
def test_reserved_notation_is_allowed_in_reserved_notation(self):
"""
reserved_notation.lean is the one file that may reserve notation.
"""
result = subprocess.run(
[
SCRIPTS_DIR / "lint-style.py",
ROOT_DIR / "src/tactic/reserved_notation.lean",
],
check=True,
capture_output=True,
)
self.assertNotIn(b"reserved notation", result.stdout)
self.assertNotIn(b"reserved notation", result.stderr)
self.assertNotIn(b"ERR_RNT", result.stdout)
self.assertNotIn(b"ERR_RNT", result.stderr)
def test_reserved_notation_is_allowed_in_relative_reserved_notation(self):
"""
reserved_notation.lean should allow reserving notation even when
checked via a relative path.
"""
result = subprocess.run(
[
"./scripts/lint-style.py",
"src/tactic/reserved_notation.lean",
],
capture_output=True,
cwd=ROOT_DIR,
)
self.assertNotIn(b"reserved notation", result.stdout)
self.assertNotIn(b"reserved notation", result.stderr)
self.assertNotIn(b"ERR_RNT", result.stdout)
self.assertNotIn(b"ERR_RNT", result.stderr)
def test_updating_style_exceptions_uses_relative_paths(self):
"""
The scripts/update-style-exceptions.sh file updates style exceptions.
It emits relative paths when doing so, since the file will be synced
with other remote machines with different filesystems.
"""
exceptions = SCRIPTS_DIR.joinpath("style-exceptions.txt")
self.assertTrue(exceptions.is_file)
current_contents = exceptions.read_text()
self.assertNotIn(str(ROOT_DIR), current_contents)
self.addCleanup(exceptions.write_text, current_contents)
subprocess.run(
["./scripts/update-style-exceptions.sh"],
check=True,
capture_output=True,
cwd=ROOT_DIR,
)
self.assertNotIn(
str(ROOT_DIR),
SCRIPTS_DIR.joinpath("style-exceptions.txt").read_text(),
)
def test_running_the_shell_script_does_not_error(self):
"""
Normally, users will run scripts/lint-style.sh, which will run the
linter on all files within mathlib.
Running it exits with successful return code.
This test will execute in a separate directory tree to make sure
it doesn't fail if there are current style warnings.
"""
with TemporaryDirectory() as tmpdir:
root = Path(tmpdir)
for each in "scripts", "src", "archive", "counterexamples":
root.joinpath(each).mkdir()
copy(SCRIPTS_DIR / "lint-style.sh", root / "scripts")
copy(SCRIPTS_DIR / "lint-style.py", root / "scripts")
# Give us at least one file to check
root.joinpath("src", "unittesting123.lean").write_text(
dedent(
"""\
/-
Copyright (c) 2021 Someone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Someone
-/
example : 37 = 37 := rfl
""",
)
)
subprocess.run(["./scripts/lint-style.sh"], check=True, cwd=root)
if __name__ == "__main__":
unittest.main(verbosity=2)