diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 39c0674..4c25256 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -34,7 +34,7 @@ jobs: - name: Install the package with pinned SymPy and dev tools run: python -m pip install -e '.[sympy,dev]' - name: Run unit tests - run: python -m pytest reasoning/tests -q + run: python -m pytest reasoning/tests tests -q - name: Type check run: python -m mypy - name: Check the vendored known facts are up to date @@ -75,7 +75,7 @@ jobs: continue-on-error: true run: | set -o pipefail - python validation/compare_backends.py --timings 0 | tee validation.txt + python validation/compare_backends.py --timings 0 --output validation.json | tee validation.txt - name: Add the validation progress to the job summary if: always() && hashFiles('validation.txt') != '' run: | @@ -98,4 +98,5 @@ jobs: path: | benchmark.json validation.txt + validation.json if-no-files-found: ignore diff --git a/.gitignore b/.gitignore index c993ca9..d92024e 100644 --- a/.gitignore +++ b/.gitignore @@ -8,3 +8,6 @@ __pycache__/ env/ results/ html/ + +# Container benchmark artifacts +bench-results/ diff --git a/README.md b/README.md index 588425c..99eb3f1 100644 --- a/README.md +++ b/README.md @@ -70,9 +70,13 @@ lightweight formulas. Legacy substitution helpers remain available for callers. ## Validation and performance -Run `python -m pytest reasoning/tests` and +Run `python -m pytest reasoning/tests tests` and `python -m benchmarks.satask --repeat 25`. +For fixed-workload ASV timings with answer checks, phase measurements, and +scaling cases, see [benchmarks/README.md](benchmarks/README.md). Upstream validation +tracks correctness separately; its wall time measures test execution cost. + To compare answers against the pinned SymPy `satask`, run `python -m benchmarks.compare_satask --include-early-return`. Saved original modules remain supported with `--baseline-satask` and `--baseline-handlers`. diff --git a/asv.conf.json b/asv.conf.json index d3c10dd..6d18163 100644 --- a/asv.conf.json +++ b/asv.conf.json @@ -2,10 +2,23 @@ "version": 1, "project": "reasoning", "repo": ".", - "branches": ["HEAD"], + "branches": [ + "HEAD" + ], "environment_type": "virtualenv", - "pythons": ["3.14"], + "pythons": [ + "3.14" + ], "benchmark_dir": "asvbench", "install_command": "python -m pip install '{wheel_file}[sympy,dev]'", - "plugins": [".asvbench.loadcheck"] + "plugins": [ + ".asvbench.loadcheck" + ], + "matrix": { + "env_nobuild": { + "PYTHONHASHSEED": [ + "0" + ] + } + } } diff --git a/asvbench/_workloads.py b/asvbench/_workloads.py new file mode 100644 index 0000000..1fbb4bd --- /dev/null +++ b/asvbench/_workloads.py @@ -0,0 +1,62 @@ +"""Fixed workloads and answer contracts; independent of validation test flow.""" +from collections.abc import Callable +from dataclasses import dataclass + +from sympy import MatrixSymbol, Q, symbols + +# Bump when inputs, expected answers, or cache policy change. This also versions +# timings whose function source does not include the workload definitions. +VERSION = "1" +NAMES = ("simple", "nested", "sum10", "matrix", "contradiction", + "upstream_integer", "upstream_zero", "upstream_unknown") +CONSISTENT_NAMES = tuple(name for name in NAMES if name != "contradiction") + + +@dataclass(frozen=True) +class Case: + proposition: object + assumptions: object + expected: bool | str | None + + +def sum_case(arity: int) -> Case: + xs = symbols(f"x:{arity}") + return Case(Q.integer(sum(xs)), Q.integer(xs[0]), None) + + +def case(name: str) -> Case: + x, y = symbols("x y") + matrix = MatrixSymbol("A", 2, 2) + # First five inputs match benchmarks.satask.cases(). The remaining cases + # are individual assertions from pinned SymPy test_query.py's test_integer + # and test_zero. Extracting assertions fixes the workload even when an + # earlier assertion in the upstream test starts passing or failing. + return { + "simple": Case(Q.real(x), Q.positive(x), True), + "nested": Case(Q.zero(x*(x+y)), Q.positive(x) & Q.positive(y), False), + "sum10": sum_case(10), + "matrix": Case(Q.invertible(matrix), Q.fullrank(matrix) & Q.square(matrix), True), + "contradiction": Case(Q.real(x), Q.real(x) & ~Q.real(x), "inconsistent"), + "upstream_integer": Case(Q.integer(x), Q.even(x) | Q.odd(x), True), + "upstream_zero": Case(Q.zero(x), Q.negative(x) | Q.positive(x), False), + "upstream_unknown": Case(Q.integer(x), ~Q.positive(x), None), + }[name] + + +def answer(call: Callable[[], bool | None]) -> bool | str | None: + try: + return call() + except ValueError as error: + if str(error) != "Inconsistent assumptions": + raise + return "inconsistent" + + +def check(actual: bool | str | None, expected: bool | str | None) -> None: + if type(actual) is not type(expected) or actual != expected: + raise AssertionError(f"answer changed: expected {expected!r}, got {actual!r}") + + +def answer_code(value: bool | str | None) -> int: + """-1 unknown, 0 false, 1 true, 2 inconsistent; never a speed score.""" + return {None: -1, False: 0, True: 1, "inconsistent": 2}[value] diff --git a/asvbench/pipeline.py b/asvbench/pipeline.py new file mode 100644 index 0000000..5401d78 --- /dev/null +++ b/asvbench/pipeline.py @@ -0,0 +1,128 @@ +"""Warm-cache timings with fixed queries and explicit answer contracts. + +Inputs are built and answers checked outside timing. Mutable databases/engines +are recreated for each call; Solve additionally disables timeit's inner loop +and warmup so its engine has not already answered the query. See benchmarks/README.md. +""" +from typing import ClassVar + +from reasoning.clauses import assert_formula, compile_formula +from reasoning.engine import ReasoningEngine +from reasoning.satask import get_all_relevant_facts, satask +from reasoning.sympy_adapter import normalize + +from ._workloads import ( + CONSISTENT_NAMES, + NAMES, + VERSION, + answer, + answer_code, + case, + check, + sum_case, +) + + +def _database(workload): + prop, assumptions = normalize(workload.proposition), normalize(workload.assumptions) + db = get_all_relevant_facts(prop, assumptions) + assert_formula(assumptions, db) + return db, compile_formula(prop, db) + + +class Pipeline: + params = NAMES + param_names: ClassVar[list[str]] = ["case"] + version = VERSION + + def setup(self, name): + self.workload = case(name) + check(answer(lambda: satask(self.workload.proposition, self.workload.assumptions)), + self.workload.expected) + + def time_satask(self, name): + # Keep the result check in the timed path too: a behavior change on a + # repeated call must not produce a misleading successful measurement. + check(answer(lambda: satask(self.workload.proposition, self.workload.assumptions)), + self.workload.expected) + + +class Phases: + params = CONSISTENT_NAMES + param_names: ClassVar[list[str]] = ["case"] + version = VERSION + + def setup(self, name): + self.workload = case(name) + self.prop = normalize(self.workload.proposition) + self.assumptions = normalize(self.workload.assumptions) + self.db, self.query = _database(self.workload) + check(ReasoningEngine(self.db).ask(self.query), self.workload.expected) + + def time_discovery_encoding(self, name): + db = get_all_relevant_facts(self.prop, self.assumptions) + assert_formula(self.assumptions, db) + compile_formula(self.prop, db) + + def time_engine_ctor(self, name): + ReasoningEngine(self.db) + + def track_clauses(self, name): + return len(self.db.data) + + def track_variables(self, name): + return len(self.db.variables) + + +class Solve: + params = CONSISTENT_NAMES + param_names: ClassVar[list[str]] = ["case"] + version = VERSION + number = 1 + warmup_time = 0 + repeat = 10 + + def setup(self, name): + self.workload = case(name) + db, self.query = _database(self.workload) + check(ReasoningEngine(db).ask(self.query), self.workload.expected) + self.engine = ReasoningEngine(db) + + def time_solve(self, name): + check(self.engine.ask(self.query), self.workload.expected) + + +class Outcomes: + """Record actual behavior even when a timing's answer contract fails.""" + params = NAMES + param_names: ClassVar[list[str]] = ["case"] + version = VERSION + + def setup(self, name): + self.workload = case(name) + + def track_answer(self, name): + return answer_code(answer(lambda: satask(self.workload.proposition, + self.workload.assumptions))) + + +class SumScaling: + params: ClassVar[list[int]] = [10, 20, 40, 80] + param_names: ClassVar[list[str]] = ["arity"] + version = VERSION + + def setup(self, arity): + self.workload = sum_case(arity) + check(answer(lambda: satask(self.workload.proposition, self.workload.assumptions)), + self.workload.expected) + self.db, _ = _database(self.workload) + + def time_satask(self, arity): + check(answer(lambda: satask(self.workload.proposition, self.workload.assumptions)), + self.workload.expected) + + def track_clauses(self, arity): + return len(self.db.data) + + def track_variables(self, arity): + return len(self.db.variables) diff --git a/asvbench/validation_progress.py b/asvbench/validation_progress.py index cf2567d..8304d6a 100644 --- a/asvbench/validation_progress.py +++ b/asvbench/validation_progress.py @@ -13,14 +13,14 @@ backend. Control series: it measures the pinned SymPy suite against itself, so it should stay near-flat at a high count; movement there reflects a changed environment or pin, not progress in this project. -- ``track_suite_wall_time``: whole-suite wall-clock seconds per backend. - -A full run costs ~50 s per backend, so the work happens once per commit in -``setup_cache``; asv pickles its return value and passes it as the first -argument to every benchmark function. Counts and wall times are reported -as ``track_*`` benchmarks (single recorded values) rather than ``time_*`` -ones, which auto-repeat and keep the minimum -- minutes of wasted -subprocess runs for a ~50 s suite. +- ``track_validation_wall_time``: whole-suite wall-clock seconds per backend. + +The expensive upstream generated-facts control is excluded. Counts therefore +start a new series with one fewer test per backend than the original 104-test +collection. Per-test outcomes can be saved with the harness's ``--output`` flag. +Whole-suite time measures validation execution cost, not engine performance: +fixing an early assertion makes the same test perform more work. Use pipeline.py +for fixed-workload performance measurements. """ from __future__ import annotations @@ -42,14 +42,14 @@ def setup_cache() -> Runs: """Run both backends once per commit; cache outcomes and wall time.""" runs = {} for backend in BACKENDS: - outcomes, _, _, wall = run_backend(backend, list(DEFAULT_SUITES), []) + outcomes, _, _, wall = run_backend(backend, list(DEFAULT_SUITES), [], + include_controls=False) runs[backend] = (outcomes, wall) return runs -# Two ~50 s pytest subprocesses per commit; asv kills setup_cache after the -# 60 s default benchmark timeout otherwise. -setup_cache.timeout = 900.0 +# Allow for slow hosts without retaining the old full-control timeout. +setup_cache.timeout = 120.0 def _count_passed(runs: Runs, backend: str, @@ -75,7 +75,7 @@ def track_passed_sympy(runs: Runs, suite_file: str) -> int: return _count_passed(runs, "sympy", suite_file) -def track_suite_wall_time(runs: Runs, backend: str) -> float: +def track_validation_wall_time(runs: Runs, backend: str) -> float: """Wall-clock seconds for one full pytest run of both suites.""" return runs[backend][1] @@ -86,5 +86,10 @@ def track_suite_wall_time(runs: Runs, backend: str) -> float: track_passed_sympy.params = [SUITE_NAMES] track_passed_sympy.unit = "tests" -track_suite_wall_time.params = [list(BACKENDS)] -track_suite_wall_time.unit = "s" +track_validation_wall_time.params = [list(BACKENDS)] +track_validation_wall_time.unit = "s" + +# The control exclusion changes the population, not solver correctness. +track_passed.version = "2-exclude-generated-facts-control" +track_passed_total.version = "2-exclude-generated-facts-control" +track_passed_sympy.version = "2-exclude-generated-facts-control" diff --git a/benchmarks/Dockerfile b/benchmarks/Dockerfile new file mode 100644 index 0000000..aa96b36 --- /dev/null +++ b/benchmarks/Dockerfile @@ -0,0 +1,10 @@ +FROM python:3.14-slim +RUN apt-get update && apt-get install -y --no-install-recommends git g++ \ + && rm -rf /var/lib/apt/lists/* +COPY pyproject.toml /tmp/project/pyproject.toml +# Install dependencies, not a source snapshot: bench-container mounts the +# checkout under test at /work. Preserve SymPy's VCS metadata for the pin check. +RUN python -c 'import tomllib, subprocess; p = tomllib.load(open("/tmp/project/pyproject.toml", "rb")); subprocess.check_call(["python", "-m", "pip", "install", "asv==0.6.6", *p["project"]["optional-dependencies"]["sympy"], *p["project"]["optional-dependencies"]["dev"]])' +RUN python -m pip install "setuptools>=68" +# ASV hardcodes ~/.asv-machine.json; redirect just that file to writable tmpfs. +RUN ln -s /tmp/asv-machine.json /root/.asv-machine.json diff --git a/benchmarks/README.md b/benchmarks/README.md index 253ae45..f713423 100644 --- a/benchmarks/README.md +++ b/benchmarks/README.md @@ -4,3 +4,83 @@ The benchmarks were made by agents that also designed the whole repository, so they cannot be trusted to give a fair comparison. The approach can be more flexible and help with development, though, so it might still be useful. + +## Correctness and speed in parallel + +The upstream validation suites track correctness and supported behavior. ASV's +`asvbench/pipeline.py` separately measures fixed queries, regardless of which +assertion an upstream test currently reaches. No solver changes are required +to use these measurements. + +| ASV benchmark | Measures | +| --- | --- | +| `pipeline.Pipeline.time_satask` | Complete query pipeline, including inconsistent assumptions | +| `pipeline.Phases.time_discovery_encoding` | Fact discovery, fact/assumption encoding, and query encoding on normalized inputs | +| `pipeline.Phases.time_engine_ctor` | Fresh engine construction from a prebuilt database | +| `pipeline.Solve.time_solve` | First query on a fresh engine, including the base consistency solve | +| `pipeline.Outcomes.track_answer` | Actual answer: -1 unknown, 0 false, 1 true, 2 inconsistent | +| `pipeline.Phases.track_clauses`, `track_variables` | Encoding size for each consistent query | +| `pipeline.SumScaling.*` | Query time and encoding size for sums of 10, 20, 40, and 80 terms | + +Inputs combine the existing five handcrafted examples with individual +assertions from pinned SymPy's `test_integer` and `test_zero`. Their provenance +and expected results live in `asvbench/_workloads.py`. These are a small initial +sample, not evidence of universal performance superiority. Add representative +real workloads as performance work exposes gaps. + +Timings check expected answers, including legitimate `None` results and the +specific inconsistency exception. A wrong answer fails the timing benchmark; +it cannot be recorded as a speedup. The separate answer series remains +available when a timing's contract fails. When behavior intentionally improves, +review the expected answer and bump the workload `VERSION` so the changed work +starts a new timing series. Also bump it for changed inputs or cache policy. + +All timings use warm process caches: setup builds inputs and checks the answer +before measurement. Input construction is excluded. Discovery creates a fresh +database on every invocation; construction creates a fresh engine. Solve uses +`number = 1`, no warmup, and a fresh engine in each setup, avoiding accidental +measurement of an already cached base model. Inconsistent inputs are measured +end to end, rather than mixed into construction/solve phase timings. + +## Running ASV + +Install ASV 0.6.6 alongside the project's pinned dependencies. From a checkout: + +```sh +python -m asv check --python=same +python -m asv run --python=same --quick --dry-run --show-stderr --bench 'pipeline\.' +``` + +The quick command is a smoke check, not a usable performance measurement. For +historical runs, `python -m asv run` manages per-commit environments. The config +sets `PYTHONHASHSEED=0` through ASV's `matrix.env_nobuild`. Keep hash seeds and +cache policy comparable; use multiple explicit seeds when checking whether a +finding generalizes. Host load warnings alone do not make measurements reliable. + +On this development host, use `~/bin/bench-container` to lease and pin a CPU. +The Dockerfile installs the pinned SymPy dependency with its VCS metadata, plus +ASV and development tools. Use a standalone clone of the committed revision so +worktree Git pointers and concurrent edits do not affect the run: + +```sh +bench-container build reasoning-bench:local . benchmarks/Dockerfile +git clone --no-hardlinks . /tmp/reasoning-bench-source +BENCH_CPU=10 bench-container run reasoning-bench:local /tmp/reasoning-bench-source -- sh -ec ' + cp -R /work/. /tmp/source + cd /tmp/source + python -m venv --system-site-packages /tmp/venv + /tmp/venv/bin/python -m pip install --no-deps --no-build-isolation -e . + /tmp/venv/bin/python -m asv machine --yes --machine reasoning-cpu10 --num_cpu 1 + /tmp/venv/bin/python -m asv run --python=same --machine reasoning-cpu10 \ + --set-commit-hash HEAD --bench "pipeline\." --show-stderr + cp -a results /results/asv +' +``` + +The writable container copy accommodates ASV caches and the validation harness's +temporary wrappers; the host source remains read-only. The `--set-commit-hash HEAD` option makes ASV save results from the existing +Python environment under the tested commit. For smoke checks add +`--quick --dry-run`. Keep A/B measurements within the same CPU lease or explicitly +set the same `BENCH_CPU`, hold competing load comparable, and alternate baseline +and candidate. Record the source commit and image digest with results. Runner +metadata records the allocated CPU/domain and hash seed defaults to zero. diff --git a/pyproject.toml b/pyproject.toml index 4615015..d61c813 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -23,7 +23,12 @@ reasoning = ["LICENSE.sympy"] include = ["reasoning*"] [tool.pytest.ini_options] -testpaths = ["reasoning/tests", "validation"] +testpaths = ["reasoning/tests", "validation", "tests"] +markers = [ + "slow: slow upstream SymPy test", + "tooslow: very slow upstream SymPy test", + "nocache_fail: upstream test requiring SymPy caching", +] [tool.mypy] python_version = "3.10" diff --git a/tests/test_benchmark_harness.py b/tests/test_benchmark_harness.py new file mode 100644 index 0000000..4c2f558 --- /dev/null +++ b/tests/test_benchmark_harness.py @@ -0,0 +1,107 @@ +"""Protect benchmark selection and correctness guards, without timing assertions.""" +import json +import sys + +import pytest + +from asvbench import pipeline +from asvbench._workloads import NAMES +from validation import compare_backends as harness + + +@pytest.mark.parametrize("backend", harness.BACKENDS) +@pytest.mark.parametrize("include_controls", [False, True]) +def test_named_control_selection(tmp_path, monkeypatch, backend, include_controls): + # An unrelated slow test must still run. The control fails if executed, + # making this check independent of measured duration or the upstream body. + source = '''import pytest +@pytest.mark.slow +def test_known_facts_consistent(): + assert False, "control executed" +@pytest.mark.slow +def test_backend_slow(): + pass +def test_regular(): + pass +''' + suite = tmp_path / "test_query.py" + suite.write_text(source) + + def write_sympy_suite(directory, original): + target = directory / f"{original.stem}_sympy.py" + target.write_text(source) + return target + + monkeypatch.setattr(harness, "write_sympy_suite", write_sympy_suite) + outcomes, _, _, _ = harness.run_backend( + backend, [suite], [], include_controls=include_controls) + expected = {"test_query::test_backend_slow": "PASSED", + "test_query::test_regular": "PASSED"} + if include_controls: + expected["test_query::test_known_facts_consistent"] = "FAILED" + assert outcomes == expected + + +def test_pytest_collection_failure_is_not_progress(tmp_path): + suite = tmp_path / "test_broken.py" + suite.write_text("raise RuntimeError('broken collection')\n") + with pytest.raises(RuntimeError, match="pytest failed with exit code 2"): + harness.run_backend("reasoning", [suite], []) + + +def test_cli_preserves_per_test_outcomes(tmp_path, monkeypatch): + report = tmp_path / "outcomes.json" + monkeypatch.setattr(sys, "argv", ["compare_backends", "--output", str(report), + "--timings", "0"]) + + def run(backend, suites, args, *, include_controls): + assert not include_controls + outcomes = {"test_query::test_a": "PASSED", "test_query::test_b": "FAILED"} + if backend == "sympy": + outcomes = {"test_query::test_a": "FAILED", "test_query::test_b": "PASSED"} + return outcomes, {}, {"test_query::test_b": "failure detail"}, 1.0 + + monkeypatch.setattr(harness, "run_backend", run) + with pytest.raises(SystemExit) as result: + harness.main() + # Both backends have one pass, but the regression must remain visible. + assert result.value.code == 1 + saved = json.loads(report.read_text()) + assert saved["backends"]["reasoning"]["outcomes"]["test_query::test_b"] == "FAILED" + assert saved["backends"]["sympy"]["outcomes"]["test_query::test_b"] == "PASSED" + assert saved["excluded_controls"] == list(harness.CONTROL_TESTS) + + +@pytest.mark.parametrize("name", NAMES) +def test_pipeline_answer_contracts(name): + benchmark = pipeline.Pipeline() + benchmark.setup(name) + benchmark.time_satask(name) + + +def test_lost_answer_fails_timing_but_is_recorded(monkeypatch): + benchmark = pipeline.Pipeline() + benchmark.setup("simple") + monkeypatch.setattr(pipeline, "satask", lambda *args: None) + with pytest.raises(AssertionError, match="answer changed"): + benchmark.time_satask("simple") + with pytest.raises(AssertionError, match="answer changed"): + benchmark.setup("simple") + outcomes = pipeline.Outcomes() + outcomes.setup("simple") + assert outcomes.track_answer("simple") == -1 + + +def test_solve_repeats_start_with_fresh_engine(): + benchmark = pipeline.Solve() + benchmark.setup("upstream_integer") + first = benchmark.engine + assert first._model_values is None + benchmark.time_solve("upstream_integer") + assert first._model_values is not None + benchmark.setup("upstream_integer") + assert benchmark.engine is not first + assert benchmark.engine._model_values is None + benchmark.time_solve("upstream_integer") + assert benchmark.number == 1 + assert benchmark.warmup_time == 0 diff --git a/validation/README.md b/validation/README.md index b68bdca..5872bde 100644 --- a/validation/README.md +++ b/validation/README.md @@ -11,3 +11,29 @@ against a different SymPy install. Install the pinned version with `compare_backends.py` runs the suite against this checkout's `satask` and against SymPy's unmodified `satask`, then compares per-test outcomes. + +Routine comparisons (including ASV) exclude only +`test_query::test_known_facts_consistent`. That test regenerates SymPy's own +known-fact dictionary without exercising either substituted backend. Selection +uses normalized test identities, so it works for the temporary SymPy wrappers +and does not exclude other tests marked `slow`. + +```sh +python validation/compare_backends.py --output validation.json +python validation/compare_backends.py --include-controls +``` + +Plain `python -m pytest validation` also retains the complete upstream suite. +The pin check verifies installation metadata; it does not replace the generated +facts consistency check. Upstream test bodies are unchanged. + +The default collection now has 103 tests instead of 104, and each backend's +passed count drops by one solely because of this exclusion. ASV's pass-count +series have a new version to mark that discontinuity. The JSON report preserves +per-test outcomes and failure details for both backends, so an improvement and +a regression cannot disappear into an unchanged total. CI uploads this report. + +Wall time and the slowest-test table describe **validation execution cost**. +They are diagnostic, not performance scores: a newly passing assertion can let +a test execute additional queries. ASV calls this `track_validation_wall_time`; +use the [fixed-workload benchmarks](../benchmarks/README.md) for engine speed. diff --git a/validation/_selection.py b/validation/_selection.py new file mode 100644 index 0000000..41448a0 --- /dev/null +++ b/validation/_selection.py @@ -0,0 +1,20 @@ +"""Select backend comparisons by normalized test identity, not speed markers. + +Loaded explicitly by compare_backends; plain pytest validation still runs the +complete upstream suites. +""" +import pytest + +from .compare_backends import CONTROL_TESTS, comparison_key + + +def pytest_collection_modifyitems(config: pytest.Config, items: list[pytest.Item]) -> None: + selected, deselected = [], [] + for item in items: + if comparison_key(item.nodeid) in CONTROL_TESTS: + deselected.append(item) + else: + selected.append(item) + items[:] = selected + if deselected: + config.hook.pytest_deselected(items=deselected) diff --git a/validation/compare_backends.py b/validation/compare_backends.py index 314dd89..70743e5 100644 --- a/validation/compare_backends.py +++ b/validation/compare_backends.py @@ -9,7 +9,10 @@ this checkout's ``satask``. The SymPy backend runs temporary re-exports of the same upstream suites with those names rebound to ``sympy.assumptions.satask``. Each backend runs in its own pytest subprocess; -per-test outcomes, timings, and failure texts are compared. An outcome where +per-test outcomes, timings, and failure texts are compared. The expensive +upstream generated-facts control is excluded unless ``--include-controls`` is +specified. Timings describe validation execution cost, not solver performance; +tests execute more assertions as correctness improves. An outcome where reasoning passes and SymPy does not is an improvement, and tests both backends fail with different failure content are expected to diverge as reasoning gets further: both are reported for inspection but do not affect the exit status. @@ -19,6 +22,7 @@ from __future__ import annotations import argparse +import json import re import subprocess import sys @@ -42,6 +46,9 @@ from {SYMPY_PACKAGE}.{{module}} import * # noqa: E402,F401,F403 """ +# Backend-independent, expensive check of upstream generated data. +CONTROL_TESTS = ("test_query::test_known_facts_consistent",) + REASONING_BINDING = "from reasoning.satask import satask" OUTCOME = re.compile(r"^(PASSED|FAILED|ERROR|XFAIL|XPASS|SKIPPED)\s+(\S+)", re.MULTILINE) @@ -86,7 +93,10 @@ def run_pytest(suites: list[Path], report: Path, pytest_args: list[str]) -> tupl ] start = perf_counter() result = subprocess.run(command, cwd=ROOT, capture_output=True, text=True) - return result.stdout + result.stderr, perf_counter() - start + output = result.stdout + result.stderr + if result.returncode not in (0, 1): + raise RuntimeError(f"pytest failed with exit code {result.returncode}:\n{output}") + return output, perf_counter() - start def parse_outcomes(output: str) -> dict[str, str]: @@ -114,13 +124,18 @@ def parse_report(report: Path, tmpdir: Path) -> tuple[dict[str, float], dict[str def run_backend(backend: str, suites: list[Path], - pytest_args: list[str]) -> tuple[dict[str, str], dict[str, float], + pytest_args: list[str], *, include_controls: bool = False, + ) -> tuple[dict[str, str], dict[str, float], dict[str, str], float]: with tempfile.TemporaryDirectory(dir=suites[0].parent) as directory_name: directory = Path(directory_name) targets = suites if backend == "reasoning" else [ write_sympy_suite(directory, suite) for suite in suites] - output, wall = run_pytest(targets, directory / "report.xml", pytest_args) + # Pytest node IDs are relative to its rootdir, and the SymPy backend + # uses temporary filenames. Select by normalized identity at collection. + selection = [] if include_controls else ["-p", "validation._selection"] + output, wall = run_pytest(targets, directory / "report.xml", + [*pytest_args, *selection]) timings, failures = parse_report(directory / "report.xml", directory) outcomes = parse_outcomes(output) if not outcomes: @@ -167,6 +182,10 @@ def main() -> None: help="extra arguments forwarded to pytest") parser.add_argument("--timings", type=int, default=10, help="number of slowest tests to show; 0 disables") + parser.add_argument("--include-controls", action="store_true", + help="include the expensive upstream generated-facts check") + parser.add_argument("--output", type=Path, metavar="JSON", + help="save per-test outcomes, failures, and diagnostic timings") parser.add_argument("--verbose", action="store_true", help="list each backend's failing tests") args = parser.parse_args() @@ -176,12 +195,26 @@ def main() -> None: if REASONING_BINDING not in suite.read_text(): raise SystemExit(f"{suite} does not bind satask from reasoning") - backends = {name: run_backend(name, suites, args.pytest_args) + backends = {name: run_backend(name, suites, args.pytest_args, + include_controls=args.include_controls) for name in BACKENDS} + if not args.include_controls: + print("Excluded upstream control: " + ", ".join(CONTROL_TESTS) + + " (use --include-controls for the full suite)") + if args.output: + args.output.write_text(json.dumps({ + "excluded_controls": [] if args.include_controls else list(CONTROL_TESTS), + "backends": { + name: {"outcomes": outcomes, "test_seconds": timings, + "failures": failures, "validation_wall_seconds": wall} + for name, (outcomes, timings, failures, wall) in backends.items() + }, + }, indent=2, sort_keys=True) + "\n") + for name, (outcomes, timings, _, wall) in backends.items(): print(f"{name}: {len(outcomes)} tests: {summarize(outcomes)} " - f"(wall {wall:.2f}s, tests {sum(timings.values()):.2f}s)") + f"(validation wall {wall:.2f}s, tests {sum(timings.values()):.2f}s)") if args.verbose: for test, outcome in sorted(outcomes.items()): if outcome in ("FAILED", "ERROR"):