File size: 4,007 Bytes
243a534 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 | #!/usr/bin/env python3
"""Run the official FPS/DFPS sources under their pinned Mathlib environment.
The audit deliberately uses the archived project and its Lake manifest. It
does not replace Mathlib with a shim or reimplement the examples. With no
argument it creates a temporary checkout, fetches the manifest-pinned
dependencies, builds them, and runs the three official Lean files. The
``--project`` option is useful for rerunning the same checks in an already
built checkout without rebuilding it.
"""
from __future__ import annotations
import argparse
import hashlib
import json
import os
import shutil
import subprocess
import tarfile
import tempfile
from pathlib import Path
REPO = Path(__file__).resolve().parents[1]
ARCHIVE = REPO / "source" / "official-current.tar.gz"
EXPECTED_BASIC_SHA256 = "a908c060d1031506ac5844b838b819391a001474eee88a5df184fa9bdac97dc4"
FILES = (
"FormalProblemSolving/Basic.lean",
"FormalProblemSolving/FPS_Example.lean",
"FormalProblemSolving/DFPS_Example.lean",
)
def run(command: list[str], cwd: Path, env: dict[str, str]) -> subprocess.CompletedProcess[str]:
return subprocess.run(
command,
cwd=cwd,
env=env,
capture_output=True,
text=True,
check=False,
)
def project_from_archive(destination: Path) -> Path:
with tarfile.open(ARCHIVE, "r:gz") as archive:
archive.extractall(destination)
top = archive.getnames()[0].split("/", 1)[0]
project = destination / top / "data" / "formal_problem_solving"
packages = project / ".lake" / "packages"
if packages.is_symlink():
packages.unlink()
packages.mkdir(parents=True, exist_ok=True)
return project
def main() -> None:
parser = argparse.ArgumentParser()
parser.add_argument(
"--project",
type=Path,
help="already prepared formal_problem_solving project; skips extraction and Lake update/build",
)
args = parser.parse_args()
lake = os.environ.get("LAKE", "/Users/sshpro/.elan/bin/lake")
if not Path(lake).exists():
lake = shutil.which("lake") or lake
if not Path(lake).exists():
raise SystemExit("lake executable is unavailable")
basic_bytes = None
project = args.project.resolve() if args.project else None
with tempfile.TemporaryDirectory(prefix="fps-full-audit-") as temporary:
if project is None:
project = project_from_archive(Path(temporary))
update = run([lake, "update", "-v"], project, os.environ.copy())
if update.returncode:
raise SystemExit(update.stdout + update.stderr)
build = run([lake, "build"], project, os.environ.copy())
if build.returncode:
raise SystemExit(build.stdout + build.stderr)
basic = project / FILES[0]
basic_bytes = basic.read_bytes()
if hashlib.sha256(basic_bytes).hexdigest() != EXPECTED_BASIC_SHA256:
raise SystemExit("archived Basic.lean hash does not match the pinned source")
results = {}
environment = os.environ.copy()
for relative in FILES:
completed = run([lake, "env", "lean", relative], project, environment)
results[relative] = {
"exit_status": completed.returncode,
"stdout": completed.stdout,
"stderr": completed.stderr,
}
if completed.returncode:
raise SystemExit(json.dumps(results, indent=2, sort_keys=True))
print(
json.dumps(
{
"basic_sha256": hashlib.sha256(basic_bytes).hexdigest(),
"lake_project": str(project),
"manifest": "lake-manifest.json",
"official_files": results,
"full_dependency_environment": True,
},
indent=2,
sort_keys=True,
)
)
if __name__ == "__main__":
main()
|