mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 10:24:07 +00:00
49715fe63c
The tests need to run with certain environment variables set that only cmake really knows and that differ between stages. Cmake could just set the variables directly when running the tests and benchmarks, but that would leave no good way to manually run a single benchmark. So cmake generates some stage-specific scripts instead that set the required environment variables. Previously, those scripts were sourced directly by the individual `run_*` scripts, so the env scripts of different stages would overwrite each other. This PR changes the setup so they can instead be generated next to each other. This also simplifies the `run_*` scripts themselves a bit, and makes `tests/bench/build` less of a hack.
180 lines
4.0 KiB
Python
Executable File
180 lines
4.0 KiB
Python
Executable File
#!/usr/bin/env python3
|
|
|
|
import os
|
|
import sys
|
|
from pathlib import Path
|
|
|
|
# Run in repo root
|
|
os.chdir(Path(__file__).parent.parent)
|
|
|
|
|
|
ERROR = False
|
|
|
|
|
|
def nag(reason: str, path: Path, fatal: bool = True) -> None:
|
|
print(f"{reason:>16}: {path}")
|
|
if fatal:
|
|
global ERROR
|
|
ERROR = True
|
|
|
|
|
|
# Files and directories that will no longer work.
|
|
|
|
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",
|
|
"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",
|
|
):
|
|
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)
|
|
|
|
|
|
# Files that use the old naming convention in the new directories.
|
|
|
|
for dir in (
|
|
"doc/examples",
|
|
"tests/compile",
|
|
"tests/compile_bench",
|
|
"tests/docparse",
|
|
"tests/elab",
|
|
"tests/elab_bench",
|
|
"tests/elab_fail",
|
|
"tests/misc",
|
|
"tests/misc_bench",
|
|
"tests/server",
|
|
"tests/server_interactive",
|
|
):
|
|
for pattern in (
|
|
f"{dir}/*.no_interpreter",
|
|
f"{dir}/*.expected.out",
|
|
f"{dir}/*.expected.ret",
|
|
):
|
|
for file in Path().glob(pattern):
|
|
nag("old suffix", file)
|
|
|
|
|
|
# Files that expect a corresponding base file
|
|
|
|
for pattern, drop in (
|
|
("**/*.no_test", 1),
|
|
("**/*.no_bench", 1),
|
|
("**/*.do_compile", 1),
|
|
("**/*.do_compile", 1),
|
|
("**/*.do_compile_test", 1),
|
|
("**/*.do_compile_bench", 1),
|
|
("**/*.do_interpret", 1),
|
|
("**/*.do_interpret_test", 1),
|
|
("**/*.do_interpret_bench", 1),
|
|
("**/*.no_compile", 1),
|
|
("**/*.no_compile", 1),
|
|
("**/*.no_compile_test", 1),
|
|
("**/*.no_compile_bench", 1),
|
|
("**/*.no_interpret", 1),
|
|
("**/*.no_interpret_test", 1),
|
|
("**/*.no_interpret_bench", 1),
|
|
("**/*.init.sh", 2),
|
|
("**/*.before.sh", 2),
|
|
("**/*.after.sh", 2),
|
|
("**/*.out.expected", 2),
|
|
("**/*.out.ignored", 2),
|
|
):
|
|
for file in Path().glob(pattern):
|
|
basefile = file
|
|
for _ in range(drop):
|
|
basefile = basefile.with_suffix("")
|
|
if basefile.exists():
|
|
continue
|
|
if basefile == Path(
|
|
"tests/pkg/leanchecker/LeanCheckerTests/PrivateConflictC.lean.fresh"
|
|
):
|
|
continue
|
|
nag("missing base", file)
|
|
|
|
|
|
# Files that shouldn't be empty
|
|
|
|
for pattern in (
|
|
"**/*.init.sh",
|
|
"**/*.before.sh",
|
|
"**/*.after.sh",
|
|
):
|
|
for file in Path().glob(pattern):
|
|
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"):
|
|
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():
|
|
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():
|
|
nag("has .no_test", file)
|
|
if file.with_suffix(".out.ignored").exists():
|
|
nag("has .no_test", file)
|
|
|
|
|
|
# Special rules for certain directories
|
|
|
|
for pattern in (
|
|
"tests/compile_bench/*.no_bench",
|
|
"tests/elab_bench/*.no_bench",
|
|
"tests/misc_bench/*.no_bench",
|
|
):
|
|
for file in Path().glob(pattern):
|
|
nag("forbidden", file)
|
|
|
|
|
|
# File confusion by case insensitive filesystems
|
|
|
|
seen: set[str] = set()
|
|
for file in Path().glob("**/*"):
|
|
path = str(file).lower()
|
|
if path in seen:
|
|
nag("case sensitive", file)
|
|
seen.add(path)
|
|
|
|
|
|
if ERROR:
|
|
sys.exit(1)
|