mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
Update lint.py
This commit is contained in:
@@ -20,8 +20,17 @@ def nag(reason: str, path: Path, fatal: bool = True) -> None:
|
||||
|
||||
# Files and directories that will no longer work.
|
||||
|
||||
for file in Path().glob("tests/speedcenter.exec.velcom.yaml"):
|
||||
nag("removed file", file)
|
||||
for pattern in (
|
||||
"**/*.exit.expected",
|
||||
"**/*.expected.out",
|
||||
"**/*.expected.ret",
|
||||
"**/*.no_interpreter",
|
||||
"**/run_bench",
|
||||
"**/run_test",
|
||||
"tests/speedcenter.exec.velcom.yaml",
|
||||
):
|
||||
for file in Path().glob(pattern):
|
||||
nag("removed file", file)
|
||||
|
||||
for dir in (
|
||||
"tests/bench-radar",
|
||||
@@ -39,12 +48,12 @@ for dir in (
|
||||
nag("removed dir", file)
|
||||
|
||||
for dir in ("tests/lean",):
|
||||
for glob in (
|
||||
for pattern in (
|
||||
f"{dir}/*.lean",
|
||||
f"{dir}/*.expected.out",
|
||||
f"{dir}/*.expected.ret",
|
||||
):
|
||||
for file in Path().glob(glob):
|
||||
for file in Path().glob(pattern):
|
||||
nag("removed dir", file)
|
||||
|
||||
|
||||
@@ -63,18 +72,18 @@ for dir in (
|
||||
"tests/server",
|
||||
"tests/server_interactive",
|
||||
):
|
||||
for glob in (
|
||||
for pattern in (
|
||||
f"{dir}/*.no_interpreter",
|
||||
f"{dir}/*.expected.out",
|
||||
f"{dir}/*.expected.ret",
|
||||
):
|
||||
for file in Path().glob(glob):
|
||||
for file in Path().glob(pattern):
|
||||
nag("old suffix", file)
|
||||
|
||||
|
||||
# Files that expect a corresponding base file
|
||||
|
||||
for glob, drop in (
|
||||
for pattern, drop in (
|
||||
("**/*.no_test", 1),
|
||||
("**/*.no_bench", 1),
|
||||
("**/*.do_compile", 1),
|
||||
@@ -96,13 +105,8 @@ for glob, drop in (
|
||||
("**/*.after.sh", 2),
|
||||
("**/*.out.expected", 2),
|
||||
("**/*.out.ignored", 2),
|
||||
("**/*.exit.expected", 2),
|
||||
# Old naming convention
|
||||
("**/*.no_interpreter", 1),
|
||||
("**/*.expected.out", 2),
|
||||
("**/*.expected.ret", 2),
|
||||
):
|
||||
for file in Path().glob(glob):
|
||||
for file in Path().glob(pattern):
|
||||
basefile = file
|
||||
for _ in range(drop):
|
||||
basefile = basefile.with_suffix("")
|
||||
@@ -117,13 +121,12 @@ for glob, drop in (
|
||||
|
||||
# Files that shouldn't be empty
|
||||
|
||||
for glob in (
|
||||
for pattern in (
|
||||
"**/*.init.sh",
|
||||
"**/*.before.sh",
|
||||
"**/*.after.sh",
|
||||
"**/*.exit.expected",
|
||||
):
|
||||
for file in Path().glob(glob):
|
||||
for file in Path().glob(pattern):
|
||||
if file.read_text().strip():
|
||||
continue
|
||||
nag("empty", file)
|
||||
@@ -153,40 +156,14 @@ for file in Path().glob("**/*.no_test"):
|
||||
|
||||
# Special rules for certain directories
|
||||
|
||||
for glob in (
|
||||
for pattern in (
|
||||
"tests/compile_bench/*.no_bench",
|
||||
"tests/elab/*.exit.expected",
|
||||
"tests/elab_bench/*.no_bench",
|
||||
"tests/misc_bench/*.no_bench",
|
||||
):
|
||||
for file in Path().glob(glob):
|
||||
for file in Path().glob(pattern):
|
||||
nag("forbidden", file)
|
||||
|
||||
for file in Path().glob("tests/elab_fail/*.exit.expected"):
|
||||
if file.read_text().strip() == "0":
|
||||
nag("must be != 0", file)
|
||||
|
||||
|
||||
# Run scripts sourcing incorrectly
|
||||
|
||||
for file in Path().glob("**/run_test"):
|
||||
if file.is_symlink():
|
||||
continue
|
||||
text = file.read_text()
|
||||
if "env_test.sh" not in text:
|
||||
nag("no env_test.sh", file)
|
||||
if "env_bench.sh" in text:
|
||||
nag("has env_bench.sh", file)
|
||||
|
||||
for file in Path().glob("**/run_bench"):
|
||||
if file.is_symlink():
|
||||
continue
|
||||
text = file.read_text()
|
||||
if "env_bench.sh" not in text:
|
||||
nag("no env_bench.sh", file)
|
||||
if "env_test.sh" in text:
|
||||
nag("has env_test.sh", file)
|
||||
|
||||
|
||||
# File confusion by case insensitive filesystems
|
||||
|
||||
|
||||
Reference in New Issue
Block a user