| """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: |
| 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")) |
| 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")) |
| 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() |
|
|
