File size: 3,804 Bytes
201dc77 | 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 | """build_valid's elaboration step: grader ceiling test first, exceptions stop the build.
THE DEFECTS (2026-10-14 review). (1) ReplPool.map returns a crashed item's exception IN PLACE, and
the old loop unpacked every result as (ok, why): one worker crash raised TypeError after the whole
Lean run, writing nothing. (2) No ceiling test: a broken toolchain/header fails every statement,
which the old code recorded as "elaboration failures" and wrote an empty dev split with exit 0.
A fake pool stands in for Lean; `check_elaborates` is replaced so no REPL is needed.
"""
from __future__ import annotations
import importlib.util
import sys
from pathlib import Path
import pytest
ROOT = Path(__file__).resolve().parents[1]
def _load():
spec = importlib.util.spec_from_file_location("build_valid_under_test", ROOT / "scripts" / "p2" / "build_valid.py")
mod = importlib.util.module_from_spec(spec)
spec.loader.exec_module(mod)
return mod
BV = _load()
BP = BV._load_sibling("build_problems")
class FakePool:
"""map() semantics of ReplPool: exceptions are returned in place, never raised."""
def __init__(self, verdict):
self.verdict = verdict
def map(self, fn, items):
out = []
for it in items:
try:
out.append(fn(None, it))
except BaseException as e: # noqa: BLE001
out.append(e)
return out
def _rec(i, stmt):
return {"problem_id": f"p{i}", "formal_statement": stmt}
@pytest.fixture
def patch_check(monkeypatch):
def install(fn):
monkeypatch.setattr(BP, "check_elaborates", lambda w, s, t: fn(s))
return install
def _sane(s):
if s == BP.SELF_TEST_GOOD:
return True, "ok"
if s == BP.SELF_TEST_BAD:
return False, "type error"
return ("bad" not in s), ("ok" if "bad" not in s else "elab error")
def test_good_and_bad_statements_are_split(patch_check):
patch_check(_sane)
good, bad = BV.elaborate(FakePool(None), [_rec(0, "fine"), _rec(1, "bad one"), _rec(2, "fine2")], 1.0)
assert [g["problem_id"] for g in good] == ["p0", "p2"]
assert bad == [{"id": "p1", "reason": "elab error"}]
def test_broken_instrument_is_refused(patch_check):
patch_check(lambda s: (False, "header_error")) # every statement fails, including the known-good probe
with pytest.raises(RuntimeError, match="ceiling test"):
BV.elaborate(FakePool(None), [_rec(0, "fine")], 1.0)
def test_lenient_instrument_is_refused(patch_check):
patch_check(lambda s: (True, "ok")) # accepts the known-bad probe
with pytest.raises(RuntimeError, match="known-bad"):
BV.elaborate(FakePool(None), [_rec(0, "fine")], 1.0)
def test_worker_crash_stops_the_build(patch_check):
def crashy(s):
if s == "boom":
raise OSError("REPL died")
return _sane(s)
patch_check(crashy)
with pytest.raises(OSError, match="REPL died"):
BV.elaborate(FakePool(None), [_rec(0, "fine"), _rec(1, "boom")], 1.0)
def test_loader_does_not_cache_failed_import(tmp_path, monkeypatch):
bad = tmp_path / "broken_sib.py"
bad.write_text("raise ImportError('nope')\n")
monkeypatch.setattr(BV, "__file__", str(tmp_path / "build_valid.py"))
with pytest.raises(ImportError):
BV._load_sibling("broken_sib")
assert "broken_sib" not in sys.modules
def test_loader_ignores_a_foreign_module_with_the_same_name(tmp_path, monkeypatch):
import types
impostor = types.ModuleType("p2_common")
impostor.__file__ = str(tmp_path / "elsewhere" / "p2_common.py")
monkeypatch.setitem(sys.modules, "p2_common", impostor)
mod = BV._load_sibling("p2_common")
assert mod is not impostor and Path(mod.__file__).resolve() == (ROOT / "scripts" / "p2" / "p2_common.py").resolve()
|