From 041d0bac93e5940f1155a475cbebe716609b3be2 Mon Sep 17 00:00:00 2001 From: tadamcz Date: Tue, 11 Aug 2026 20:16:20 +0100 Subject: [PATCH 1/2] Per-dataset FC pins for the sandbox images Each dataset now pins its own formal-conjectures commit in apn/data//fc_commit (all initially the same constant). The pin flows into the compose files as the FC_COMMIT build arg -- the Dockerfile's only ARG without a default -- and into the image tags (LeanOpenProblems___fc_), so datasets sharing a pin share images and a pin change alone triggers a fresh CI build. The FC branch is no longer recorded anywhere: a plain clone fetches all branch refs, so checkout by commit suffices. --- .github/workflows/build-docker-images.yaml | 48 ++++++++++++++-------- apn/data/README.md | 1 + apn/data/erdos/NOTICE.md | 2 +- apn/data/erdos/fc_commit | 1 + apn/data/fc100open/NOTICE.md | 2 +- apn/data/fc100open/fc_commit | 1 + apn/data/oeis/NOTICE.md | 7 ++-- apn/data/oeis/fc_commit | 1 + apn/dataset.py | 15 +++++++ apn/lean/Dockerfile | 16 ++++++-- apn/task.py | 46 +++++++++++++-------- scripts/bump_version.py | 8 ++-- scripts/generate_erdos_isolated.py | 3 +- scripts/generate_fc100_isolated.py | 6 ++- tests/lean_sandbox.py | 26 +++++++----- tests/test_erdos_isolation.py | 4 +- tests/test_fc100_isolation.py | 4 +- tests/test_fc_pins.py | 26 ++++++++++++ tests/test_gold_proofs.py | 4 +- tests/test_lean_vuln_e2e.py | 4 +- tests/test_oeis_isolation.py | 4 +- tests/test_singlefile_proof.py | 4 +- 22 files changed, 165 insertions(+), 68 deletions(-) create mode 100644 apn/data/erdos/fc_commit create mode 100644 apn/data/fc100open/fc_commit create mode 100644 apn/data/oeis/fc_commit create mode 100644 tests/test_fc_pins.py diff --git a/.github/workflows/build-docker-images.yaml b/.github/workflows/build-docker-images.yaml index 52a02721..4a3e5ba8 100644 --- a/.github/workflows/build-docker-images.yaml +++ b/.github/workflows/build-docker-images.yaml @@ -36,8 +36,10 @@ jobs: with: registry: ${{ vars.ECR_REGISTRY }} - # ECR tags are immutable and keyed by apn.__version__, so a target is - # built only if its tag is missing (i.e. after a version bump). + # ECR tags are immutable and keyed by apn.__version__ plus the dataset's + # FC pin (apn/data//fc_commit), so a (target, pin) image is + # built only if its tag is missing -- i.e. after a version bump or a pin + # change. Datasets sharing a pin share tags, so nothing is built twice. - name: Find images missing from ECR id: missing run: |- @@ -47,30 +49,44 @@ jobs: exit 1 fi echo "version=$image_version" >> "$GITHUB_OUTPUT" - targets="" - for target in agent agent_corpus scorer; do - if ! aws ecr describe-images \ - --repository-name "${IMAGE_NAME#*/}" \ - --image-ids "imageTag=LeanOpenProblems_${target}_${image_version}" \ - >/dev/null 2>&1; then - targets="$targets $target" + commits="$(sort -u apn/data/*/fc_commit)" + builds="" + while read -r commit; do + if ! echo "$commit" | grep -qE '^[0-9a-f]{40}$'; then + echo "Invalid fc_commit entry: '$commit'" >&2 + exit 1 fi - done - echo "targets=${targets# }" >> "$GITHUB_OUTPUT" + for target in agent agent_corpus scorer; do + if ! aws ecr describe-images \ + --repository-name "${IMAGE_NAME#*/}" \ + --image-ids "imageTag=LeanOpenProblems_${target}_${image_version}_fc_${commit:0:12}" \ + >/dev/null 2>&1; then + builds="${builds}${target} ${commit}"$'\n' + fi + done + done <<< "$commits" + { + echo "builds<> "$GITHUB_OUTPUT" - name: Set reproducible build timestamp run: echo "SOURCE_DATE_EPOCH=$(git log -1 --pretty=%ct)" >> "$GITHUB_ENV" # The targets are stages of one Dockerfile built on one builder, so - # shared stages (the expensive Lean + Mathlib base) are built once. + # shared stages (the expensive Lean + Mathlib base) are built once per + # FC pin. - name: Build and push images - if: steps.missing.outputs.targets != '' + if: steps.missing.outputs.builds != '' working-directory: apn/lean run: |- - for target in ${{ steps.missing.outputs.targets }}; do + while read -r target commit; do + [ -z "$target" ] && continue docker buildx build \ --target "$target" \ + --build-arg "FC_COMMIT=${commit}" \ --push \ - -t "${IMAGE_NAME}:LeanOpenProblems_${target}_${{ steps.missing.outputs.version }}" \ + -t "${IMAGE_NAME}:LeanOpenProblems_${target}_${{ steps.missing.outputs.version }}_fc_${commit:0:12}" \ . - done + done <<< "${{ steps.missing.outputs.builds }}" diff --git a/apn/data/README.md b/apn/data/README.md index 7bf4bd85..033209de 100644 --- a/apn/data/README.md +++ b/apn/data/README.md @@ -5,6 +5,7 @@ Every dataset directory here has the same shape: | Path | Used at runtime | Contents | | --- | --- |---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------| | `samples.jsonl` | Yes | One row per item; keys below. | +| `fc_commit` | Yes | The dataset's pinned formal-conjectures commit (40-hex). Baked into the dataset's sandbox images (compose build arg; keys the image tag) and the pin its `Sources/` were vendored at. Datasets sharing a pin share images. | | `Isolated/.lean` | Yes | The source file's definitions plus the single target theorem; sibling theorems, test lemmas and anonymous `example`s cut; `answer(...) ↔` forms rewritten to plain `P` (recorded verdicts un-filled) and `@[category ...]` lists dropped. Generated by `scripts/generate_*_isolated.py`, tested by `tests/test_*_isolation.py`. | | `subsets/.json` | Yes | `{description, ids}`; every id must exist in the manifest. | | `Sources/` | No | Verbatim vendored Lean from upstream; each tree's README records the exact upstream pin. | diff --git a/apn/data/erdos/NOTICE.md b/apn/data/erdos/NOTICE.md index 6c397b3c..9ab8ef08 100644 --- a/apn/data/erdos/NOTICE.md +++ b/apn/data/erdos/NOTICE.md @@ -3,7 +3,7 @@ Upstream source: the Tsoukalas paper's attempted list (arXiv 2605.22763; upstream commit and file hash in `subsets/tsoukalas_attempted.json`'s `description`). 350 of the paper's 353 statements resolve at the pinned FC -commit and are in `samples.jsonl`; the subset names the same 350 ids, and +commit (`fc_commit`) and are in `samples.jsonl`; the subset names the same 350 ids, and bare `apn_erdos` runs them all. `scripts/generate_erdos_isolated.py` censuses every research-category statement in `Sources/`, so the committed manifest is curated down to the attempted set. diff --git a/apn/data/erdos/fc_commit b/apn/data/erdos/fc_commit new file mode 100644 index 00000000..13515f9c --- /dev/null +++ b/apn/data/erdos/fc_commit @@ -0,0 +1 @@ +67338a157bbb8d87e9a349d662f82a868bda6327 diff --git a/apn/data/fc100open/NOTICE.md b/apn/data/fc100open/NOTICE.md index 46e53e1d..64bc9576 100644 --- a/apn/data/fc100open/NOTICE.md +++ b/apn/data/fc100open/NOTICE.md @@ -1,3 +1,3 @@ # The FC100OpenSet1 dataset -Upstream source: `FormalConjectures/Subsets/FC100OpenSet1.lean` at `82f6f8958c152dfdd2555cedcee83887b94b7f5520c8cb171a7dd522ea3795c1` of FormalConjectures. The same 100 items are in `samples.jsonl`. The 14 value-typed `answer(sorry)` members are `excluded` rows, leaving 86 runnable entries. \ No newline at end of file +Upstream source: `FormalConjectures/Subsets/FC100OpenSet1.lean` at the FC commit pinned in `fc_commit`. The same 100 items are in `samples.jsonl`. The 14 value-typed `answer(sorry)` members are `excluded` rows, leaving 86 runnable entries. \ No newline at end of file diff --git a/apn/data/fc100open/fc_commit b/apn/data/fc100open/fc_commit new file mode 100644 index 00000000..13515f9c --- /dev/null +++ b/apn/data/fc100open/fc_commit @@ -0,0 +1 @@ +67338a157bbb8d87e9a349d662f82a868bda6327 diff --git a/apn/data/oeis/NOTICE.md b/apn/data/oeis/NOTICE.md index f722431f..37c43ec9 100644 --- a/apn/data/oeis/NOTICE.md +++ b/apn/data/oeis/NOTICE.md @@ -1,7 +1,6 @@ # The OEIS dataset -Upstream source: `FormalConjectures/OEIS/Auto/THEOREM_MAPPING.txt` at sha256 -`386c0c6e7abf782077b0eee5bf59ddb0caf67acf11db96502b8b2e11bd64c2fe` of -FormalConjectures. The same 492 conjectures are in `samples.jsonl`, one row -per conjecture with its OEIS A-number. 3 conjectures map to more than one +Upstream source: `FormalConjectures/OEIS/Auto/THEOREM_MAPPING.txt` at the FC +commit pinned in `fc_commit`. The same 492 conjectures are in +`samples.jsonl`, one row per conjecture with its OEIS A-number. 3 conjectures map to more than one upstream file: `source` is the first, the rest are `other_sources`. \ No newline at end of file diff --git a/apn/data/oeis/fc_commit b/apn/data/oeis/fc_commit new file mode 100644 index 00000000..13515f9c --- /dev/null +++ b/apn/data/oeis/fc_commit @@ -0,0 +1 @@ +67338a157bbb8d87e9a349d662f82a868bda6327 diff --git a/apn/dataset.py b/apn/dataset.py index eb940be1..c806b05a 100644 --- a/apn/dataset.py +++ b/apn/dataset.py @@ -1,6 +1,7 @@ from __future__ import annotations import json +import re from dataclasses import dataclass, field from pathlib import Path from typing import Any, Iterable @@ -12,6 +13,20 @@ ERDOS_DIR = Path(__file__).parent / "data" / "erdos" +def fc_commit(dataset_dir: str | Path) -> str: + """The dataset's pinned formal-conjectures commit (``fc_commit``). + + The pin is what the dataset's sandbox images bake (compose build arg, + image tag component) and what its vendored ``Sources/`` were extracted at. + """ + commit = (Path(dataset_dir) / "fc_commit").read_text().strip() + if not re.fullmatch(r"[0-9a-f]{40}", commit): + raise ValueError( + f"{Path(dataset_dir).name}: fc_commit must hold a 40-hex commit, got {commit!r}" + ) + return commit + + @dataclass(frozen=True) class SampleRow: """One universe member of a dataset's ``samples.jsonl`` manifest. diff --git a/apn/lean/Dockerfile b/apn/lean/Dockerfile index a6f05791..d31a7643 100644 --- a/apn/lean/Dockerfile +++ b/apn/lean/Dockerfile @@ -13,6 +13,12 @@ # # Lean v4.27.0 matches the Formal Conjectures Erdős/OEIS datasets (oleans are # version-specific, so the repl and SafeVerify are all built at this version). +# Every dataset's FC pin must have lean-toolchain = v4.27.0: the FC checkout's +# own lean-toolchain drives the library build, but PyPantograph's repl (the +# pinned commit below targets v4.27.0) and the vendored safeverify/ and +# extract_ranges/ lean-toolchain files must match the oleans they load/replay. +# Moving past an FC toolchain bump is therefore a coordinated change to all of +# those pins together. # # The builder stage clones the whole formal-conjectures repo and builds the # library; base copies in ONLY the toolchain, the lake build artifacts @@ -41,9 +47,10 @@ RUN curl -sSfL "https://github.com/leanprover/elan/releases/download/${ELAN_VERS && /tmp/elan-init -y --default-toolchain "leanprover/lean4:${LEAN_VERSION}" \ && rm /tmp/elan-init -ARG FC_BRANCH=auto_oeis -ARG FC_COMMIT=67338a157bbb8d87e9a349d662f82a868bda6327 -RUN git clone --filter=blob:none --branch "${FC_BRANCH}" \ +# The dataset's FC pin (apn/data//fc_commit). Required: there is +# deliberately no default a stale build could silently fall back to +ARG FC_COMMIT +RUN git clone --filter=blob:none \ https://github.com/google-deepmind/formal-conjectures /workspace/leanproject \ && git -C /workspace/leanproject checkout "${FC_COMMIT}" @@ -255,7 +262,8 @@ CMD ["sleep", "infinity"] # a runtime service and kept separate from `scorer` so the scored image stays # # minimal. Source-only COPY (no host .lake); imports only Lean core, so it # # builds offline with no `lake update`. Run via: # -# docker build --target generate -t apn-generate apn/lean # +# docker build --target generate -t apn-generate \ # +# --build-arg FC_COMMIT="$(cat apn/data//fc_commit)" apn/lean # # docker run --rm -v "$PWD":/repo apn-generate \ # # python3 /repo/scripts/generate_oeis_isolated.py --container '' ... # # (in practice: build the extractor into a container with the repo mounted). # diff --git a/apn/task.py b/apn/task.py index 7d1b9439..a74af18c 100644 --- a/apn/task.py +++ b/apn/task.py @@ -15,6 +15,7 @@ OEIS_DIR, erdos_dataset, fc100open_dataset, + fc_commit, load_subset, oeis_dataset, ) @@ -28,58 +29,66 @@ def _docker_tag_component(value: str) -> str: return re.sub(r"[^A-Za-z0-9_.-]", "_", value) -def get_identifier_for_image(image_kind: str) -> str: +def get_identifier_for_image(image_kind: str, fc_commit: str) -> str: + """Image tag: keyed on apn.__version__ AND the FC pin, so datasets sharing + a pin share images and a pin change alone yields fresh tags.""" image_version = _docker_tag_component(__version__) - return f"LeanOpenProblems_{image_kind}_{image_version}" + return f"LeanOpenProblems_{image_kind}_{image_version}_fc_{fc_commit[:12]}" -def _build_section(target: str) -> str: +def _build_section(target: str, fc_commit: str) -> str: return f"""\ build: context: {Path(__file__).parent / "lean"} target: {target} + args: + FC_COMMIT: {fc_commit} """ -def get_compose_file_content(literature: bool = False) -> str: +def get_compose_file_content(fc_commit: str, literature: bool = False) -> str: agent_kind = "agent_corpus" if literature else "agent" - agent_tag = get_identifier_for_image(agent_kind) - scorer_tag = get_identifier_for_image("scorer") + agent_tag = get_identifier_for_image(agent_kind, fc_commit) + scorer_tag = get_identifier_for_image("scorer", fc_commit) return f""" services: default: image: {IMAGE_REPOSITORY}:{agent_tag} -{_build_section(agent_kind)} init: true +{_build_section(agent_kind, fc_commit)} init: true entrypoint: tail -f /dev/null mem_limit: 10g network_mode: none compile: image: {IMAGE_REPOSITORY}:{scorer_tag} -{_build_section("scorer")} init: true +{_build_section("scorer", fc_commit)} init: true entrypoint: tail -f /dev/null mem_limit: 10g network_mode: none scorer: image: {IMAGE_REPOSITORY}:{scorer_tag} -{_build_section("scorer")} init: true +{_build_section("scorer", fc_commit)} init: true entrypoint: tail -f /dev/null mem_limit: 50g network_mode: none """ -def get_compose_file(literature: bool = False) -> Path: - # Both variants are named compose.yaml, isolated in per-variant subdirs so they - # don't clobber each other. +def get_compose_file(fc_commit: str, literature: bool = False) -> Path: + # Both variants are named compose.yaml, isolated in per-(FC pin, variant) + # subdirs so they don't clobber each other. # k8s_sandbox only treats a sandbox config as a compose file when its name *ends* in # "compose.yaml"/"compose.yml" (is_docker_compose_file); anything else # would be fed to the agent-env Helm chart verbatim. variant = "corpus" if literature else "closed-book" compose_path = ( - COMPOSE_FILES_DIR / _docker_tag_component(__version__) / variant / "compose.yaml" + COMPOSE_FILES_DIR + / _docker_tag_component(__version__) + / f"fc_{fc_commit[:12]}" + / variant + / "compose.yaml" ) compose_path.parent.mkdir(parents=True, exist_ok=True) - content = get_compose_file_content(literature) + content = get_compose_file_content(fc_commit, literature) if not compose_path.exists() or compose_path.read_text() != content: compose_path.write_text(content) return compose_path @@ -108,7 +117,7 @@ def apn_oeis( agent_type=agent_type, ), scorer=proof_scorer(SandboxSafeVerify(sandbox_name="scorer")), - sandbox=("docker", str(get_compose_file(literature))), + sandbox=("docker", str(get_compose_file(fc_commit(OEIS_DIR), literature))), ) @@ -128,7 +137,7 @@ def apn_fc100open( agent_type=agent_type, ), scorer=proof_scorer(SandboxSafeVerify(sandbox_name="scorer")), - sandbox=("docker", str(get_compose_file(literature))), + sandbox=("docker", str(get_compose_file(fc_commit(FC100_DIR), literature))), ) @@ -144,7 +153,8 @@ def apn_erdos( All 353 FC ErdosProblems statements the paper's agent attempted, of which 350 ship as samples (3 are unresolvable at the vendored FC commit; see ``subsets/tsoukalas_attempted.json``'s description). Statement text is FC - at 67338a1 -- the exact commit the sandbox images bake -- and every + at the dataset's pin (``apn/data/erdos/fc_commit``) -- the exact + commit the sandbox images bake -- and every ``answer(...) ↔`` form is certified-rewritten to the attempt-time binary task, plain ``P`` (recorded ``True``/``False`` verdicts un-filled, and FC's recorded-verdict annotations stripped, so the answer key cannot @@ -160,5 +170,5 @@ def apn_erdos( agent_type=agent_type, ), scorer=proof_scorer(SandboxSafeVerify(sandbox_name="scorer")), - sandbox=("docker", str(get_compose_file(literature))), + sandbox=("docker", str(get_compose_file(fc_commit(ERDOS_DIR), literature))), ) diff --git a/scripts/bump_version.py b/scripts/bump_version.py index 4ab28797..22779870 100644 --- a/scripts/bump_version.py +++ b/scripts/bump_version.py @@ -3,9 +3,11 @@ Bump version in pyproject.toml, apn/__init__.py, and uv.lock. Usage: python scripts/bump_version.py [rc|release|major|minor|patch] -The CI image tags (LeanOpenProblems_*_) are keyed on apn.__version__, -so bumping the version is how you trigger a fresh ECR build of the sandbox -images. Keep the two version sources in lockstep -- this script edits both. +The CI image tags (LeanOpenProblems_*__fc_) are keyed on +apn.__version__ and the per-dataset FC pins (apn/data//fc_commit), +so bumping the version -- or changing a pin -- triggers a fresh ECR build of +the sandbox images. Keep the two version sources in lockstep -- this script +edits both. Default is 'rc', which produces release candidate versions: 0.1.3 -> 0.1.4rc1 diff --git a/scripts/generate_erdos_isolated.py b/scripts/generate_erdos_isolated.py index 0f7b2c9c..9eed4e88 100644 --- a/scripts/generate_erdos_isolated.py +++ b/scripts/generate_erdos_isolated.py @@ -30,7 +30,8 @@ container with the repo mounted; the baked extractor of the Dockerfile's ``generate`` stage is the default ``--exe``: - docker build --target generate -t apn-generate apn/lean + docker build --target generate -t apn-generate \\ + --build-arg FC_COMMIT="$(cat apn/data/erdos/fc_commit)" apn/lean docker run -d --name apn-isolate-dev -v "$PWD":/repo -w /repo \\ apn-generate sleep infinity diff --git a/scripts/generate_fc100_isolated.py b/scripts/generate_fc100_isolated.py index 73100dbd..ae70158a 100644 --- a/scripts/generate_fc100_isolated.py +++ b/scripts/generate_fc100_isolated.py @@ -25,7 +25,11 @@ ``generate`` stage is the default ``--exe``: docker run -d --name apn-isolate-dev -v "$PWD":/repo -w /repo \\ - "$IMAGE_REPOSITORY:LeanOpenProblems_generate_" sleep infinity + "$IMAGE_REPOSITORY:LeanOpenProblems_generate__fc_" sleep infinity + +(```` is the first 12 chars of ``apn/data/fc100open/fc_commit``, +the dataset's FC pin; or build locally with ``docker build --target generate +--build-arg FC_COMMIT="$(cat apn/data/fc100open/fc_commit)" apn/lean``.) Then generate: diff --git a/tests/lean_sandbox.py b/tests/lean_sandbox.py index 7d111db8..22b9909a 100644 --- a/tests/lean_sandbox.py +++ b/tests/lean_sandbox.py @@ -45,23 +45,28 @@ from scripts.isolation import BAKED_EXE, CONTAINER_PROJECT, COMPILE_SCRIPT, parse_extractor_output -def generate_compose_file() -> str: +def generate_compose_file(fc_commit: str) -> str: """Path to a one-service compose that builds the Dockerfile's ``generate`` - stage. Reuses ``apn.task``'s build-section + version-tag helpers, so the - image is current by construction (``build:`` rebuilds from the Dockerfile) - and never pinned to a stale fixed tag.""" - tag = get_identifier_for_image("generate") + stage at the given FC pin. Reuses ``apn.task``'s build-section + + version-tag helpers, so the image is current by construction (``build:`` + rebuilds from the Dockerfile) and never pinned to a stale fixed tag.""" + tag = get_identifier_for_image("generate", fc_commit) content = f"""# Generated by tests/lean_sandbox.py -- the Dockerfile `generate` stage # (base Lean/Mathlib/FormalConjectures + the baked extract_ranges binary). services: default: image: {IMAGE_REPOSITORY}:{tag} -{_build_section("generate")} init: true +{_build_section("generate", fc_commit)} init: true entrypoint: tail -f /dev/null mem_limit: 32g network_mode: none """ - d = Path(tempfile.gettempdir()) / "apn_generate_compose" / _docker_tag_component(__version__) + d = ( + Path(tempfile.gettempdir()) + / "apn_generate_compose" + / _docker_tag_component(__version__) + / f"fc_{fc_commit[:12]}" + ) d.mkdir(parents=True, exist_ok=True) path = d / "compose.yaml" if not path.exists() or path.read_text() != content: @@ -70,14 +75,15 @@ def generate_compose_file() -> str: @asynccontextmanager -async def generate_env(task_name: str) -> AsyncIterator[DockerSandboxEnvironment]: - """Bring up the ``generate`` compose and yield the live sandbox env. +async def generate_env(task_name: str, fc_commit: str) -> AsyncIterator[DockerSandboxEnvironment]: + """Bring up the ``generate`` compose at the dataset's FC pin and yield the + live sandbox env. Per-session bring-up/tear-down through Inspect's sandbox lifecycle (the same path a real eval uses); the docker cache keeps repeat runs cheap. Mirrors ``tests/test_singlefile_proof.py::_sandbox_envs``. """ - compose = generate_compose_file() + compose = generate_compose_file(fc_commit) await DockerSandboxEnvironment.task_init(task_name, compose) try: envs = await init_sandbox_environments_sample( diff --git a/tests/test_erdos_isolation.py b/tests/test_erdos_isolation.py index 5d10bcba..3cd51953 100644 --- a/tests/test_erdos_isolation.py +++ b/tests/test_erdos_isolation.py @@ -40,7 +40,7 @@ import pytest import pytest_asyncio -from apn.dataset import ERDOS_DIR, SampleRow, load_manifest +from apn.dataset import ERDOS_DIR, SampleRow, fc_commit, load_manifest from scripts.erdos_isolation import ( ISOLATED_DIR, SOURCES_DIR, @@ -89,7 +89,7 @@ async def iso_data(kept_rows: list[SampleRow]) -> IsoData: arrangement as ``tests/test_fc100_isolation.py::iso_data``, for the same reasons. """ - async with generate_env("pytest_erdos_isolation") as env: + async with generate_env("pytest_erdos_isolation", fc_commit(ERDOS_DIR)) as env: rels = sorted({r.source.removeprefix("Sources/") for r in kept_rows}) src = await extract(env, [SOURCES_DIR / rel for rel in rels], arcnames=rels) iso_files = sorted(ISOLATED_DIR.glob("*.lean")) diff --git a/tests/test_fc100_isolation.py b/tests/test_fc100_isolation.py index 33722ef4..aff82681 100644 --- a/tests/test_fc100_isolation.py +++ b/tests/test_fc100_isolation.py @@ -37,7 +37,7 @@ import pytest import pytest_asyncio -from apn.dataset import FC100_DIR, load_manifest +from apn.dataset import FC100_DIR, fc_commit, load_manifest from scripts.fc100_isolation import ( ISOLATED_DIR, SOURCES_DIR, @@ -82,7 +82,7 @@ async def iso_data(mapping: list[tuple[str, str]]) -> IsoData: (fully qualified decl names) are unique. Same async/loop-scope arrangement as ``tests/test_oeis_isolation.py::iso_data``, for the same reasons. """ - async with generate_env("pytest_fc100_isolation") as env: + async with generate_env("pytest_fc100_isolation", fc_commit(FC100_DIR)) as env: rels = sorted({rel for _, rel in mapping}) src = await extract(env, [SOURCES_DIR / rel for rel in rels], arcnames=rels) iso_files = sorted(ISOLATED_DIR.glob("*.lean")) diff --git a/tests/test_fc_pins.py b/tests/test_fc_pins.py new file mode 100644 index 00000000..30a47e1f --- /dev/null +++ b/tests/test_fc_pins.py @@ -0,0 +1,26 @@ +"""The per-dataset FC pins (``apn/data//fc_commit``) are loadable +and produce valid docker image tags. Fast, no docker.""" + +import re +from pathlib import Path + +import pytest + +from apn.dataset import ERDOS_DIR, FC100_DIR, OEIS_DIR, fc_commit +from apn.task import get_identifier_for_image + +DATASET_DIRS = {"erdos": ERDOS_DIR, "fc100open": FC100_DIR, "oeis": OEIS_DIR} + + +@pytest.mark.parametrize("dataset_dir", DATASET_DIRS.values(), ids=DATASET_DIRS.keys()) +def test_pin_loads(dataset_dir: Path) -> None: + commit = fc_commit(dataset_dir) + assert re.fullmatch(r"[0-9a-f]{40}", commit) + + +@pytest.mark.parametrize("dataset_dir", DATASET_DIRS.values(), ids=DATASET_DIRS.keys()) +def test_pin_makes_valid_image_tag(dataset_dir: Path) -> None: + # agent_corpus is the longest image kind. + tag = get_identifier_for_image("agent_corpus", fc_commit(dataset_dir)) + assert re.fullmatch(r"[A-Za-z0-9_.-]+", tag) + assert len(tag) <= 128 diff --git a/tests/test_gold_proofs.py b/tests/test_gold_proofs.py index 5f8888cc..e9625113 100644 --- a/tests/test_gold_proofs.py +++ b/tests/test_gold_proofs.py @@ -70,6 +70,7 @@ import apn.checker as checker_mod from apn.checker import SandboxSafeVerify +from apn.dataset import OEIS_DIR, fc_commit from apn.task import get_compose_file REPO = Path(__file__).resolve().parent.parent @@ -114,7 +115,8 @@ async def _sandbox_envs() -> AsyncIterator[dict[str, SandboxEnvironment]]: spans the untrusted ``compile`` and trusted ``scorer`` sandboxes, so we expose the whole dict. """ - compose = str(get_compose_file(literature=False)) + # The gold proofs are OEIS conjectures, so score against the oeis pin's image. + compose = str(get_compose_file(fc_commit(OEIS_DIR), literature=False)) task_name = "pytest_gold_proofs_scorer" await DockerSandboxEnvironment.task_init(task_name, compose) try: diff --git a/tests/test_lean_vuln_e2e.py b/tests/test_lean_vuln_e2e.py index 5d1e9dad..5984c65f 100644 --- a/tests/test_lean_vuln_e2e.py +++ b/tests/test_lean_vuln_e2e.py @@ -65,6 +65,7 @@ import apn.checker as checker_mod import apn.scorer as scorer_mod from apn.checker import SAFE_VERIFY_BIN, SandboxSafeVerify +from apn.dataset import OEIS_DIR, fc_commit from apn.layout import SUBMISSION_DIR from apn.scorer import proof_scorer from apn.task import get_compose_file @@ -260,7 +261,8 @@ async def _sandboxes() -> AsyncIterator[dict[str, SandboxEnvironment]]: Per-test bring-up isolates an OOM/crash (and any compile-time tamper) to a single case. """ - compose = str(get_compose_file(literature=False)) + # Dataset-agnostic suite: any dataset's image works, so use the oeis pin. + compose = str(get_compose_file(fc_commit(OEIS_DIR), literature=False)) task_name = "pytest_lean_vuln_e2e" await DockerSandboxEnvironment.task_init(task_name, compose) try: diff --git a/tests/test_oeis_isolation.py b/tests/test_oeis_isolation.py index 4b7921fc..dc06bbc8 100644 --- a/tests/test_oeis_isolation.py +++ b/tests/test_oeis_isolation.py @@ -36,7 +36,7 @@ import pytest import pytest_asyncio -from apn.dataset import OEIS_DIR, SampleRow, load_manifest +from apn.dataset import OEIS_DIR, SampleRow, fc_commit, load_manifest from scripts.isolation import ( matches_name, planned_survivors, @@ -85,7 +85,7 @@ async def iso_data(manifest: list[SampleRow]) -> IsoData: second event loop that Inspect's loop-bound globals deadlock against; sharing pytest-asyncio's own loop avoids that. The gates below just assert against the returned data, so they need no further sandbox access.""" - async with generate_env("pytest_oeis_isolation") as env: + async with generate_env("pytest_oeis_isolation", fc_commit(OEIS_DIR)) as env: source_files = sorted({r.source.rsplit("/", 1)[-1] for r in manifest}) src = await extract(env, [SOURCES_DIR / f for f in source_files]) iso_files = sorted(ISOLATED_DIR.glob("*.lean")) diff --git a/tests/test_singlefile_proof.py b/tests/test_singlefile_proof.py index 3b97ac7c..329810c4 100644 --- a/tests/test_singlefile_proof.py +++ b/tests/test_singlefile_proof.py @@ -54,6 +54,7 @@ import apn.checker as checker_mod from apn.checker import CheckOutcome, SandboxSafeVerify +from apn.dataset import OEIS_DIR, fc_commit from apn.task import get_compose_file @@ -85,7 +86,8 @@ async def _sandbox_envs() -> AsyncIterator[dict[str, SandboxEnvironment]]: bring-up/tear-down -- simple and correct; the docker cache keeps repeat runs cheap (the same trade-off PortBench's test harness makes). """ - compose = str(get_compose_file(literature=False)) + # Dataset-agnostic suite: any dataset's image works, so use the oeis pin. + compose = str(get_compose_file(fc_commit(OEIS_DIR), literature=False)) task_name = "pytest_singlefile_scorer" await DockerSandboxEnvironment.task_init(task_name, compose) try: From 0f07bb1503821643b8c5c80bd2a51fb1e5f6891e Mon Sep 17 00:00:00 2001 From: tadamcz Date: Tue, 11 Aug 2026 20:17:30 +0100 Subject: [PATCH 2/2] Bump version to 0.1.6 Not strictly required (the new _fc_ tag component already changes every tag), but makes the pin-keyed image generation obvious. --- apn/__init__.py | 2 +- pyproject.toml | 2 +- uv.lock | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/apn/__init__.py b/apn/__init__.py index 7e4d2cda..296a7779 100644 --- a/apn/__init__.py +++ b/apn/__init__.py @@ -1,4 +1,4 @@ __all__ = ["__version__"] -__version__ = "0.1.5" +__version__ = "0.1.6" diff --git a/pyproject.toml b/pyproject.toml index ec8295e9..d03bcaf4 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -1,6 +1,6 @@ [project] name = "apn" -version = "0.1.5" +version = "0.1.6" description = "An Inspect implementation of the AlphaProof Nexus formal proof-search framework" requires-python = ">=3.13,<3.14" dependencies = [] diff --git a/uv.lock b/uv.lock index 2ef7db33..5d5f77bd 100644 --- a/uv.lock +++ b/uv.lock @@ -182,7 +182,7 @@ wheels = [ [[package]] name = "apn" -version = "0.1.5" +version = "0.1.6" source = { editable = "." } [package.dev-dependencies]