Per-dataset FC pins for the sandbox images

.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/<dataset>/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<<APN_EOF"
+            printf '%s' "$builds"
+            echo "APN_EOF"
+          } >> "$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 }}"

apn/__init__.py

@@ -1,4 +1,4 @@
 
 __all__ = ["__version__"]
 
-__version__ = "0.1.5"
+__version__ = "0.1.6"

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/<id>.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/<name>.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.                                                                                                                                                                                                                                                    |

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.

apn/data/erdos/fc_commit

@@ -0,0 +1 @@
+67338a157bbb8d87e9a349d662f82a868bda6327

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.
+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.

apn/data/fc100open/fc_commit

@@ -0,0 +1 @@
+67338a157bbb8d87e9a349d662f82a868bda6327

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`.

apn/data/oeis/fc_commit

@@ -0,0 +1 @@
+67338a157bbb8d87e9a349d662f82a868bda6327

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.

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/<dataset>/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/<dataset>/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).     #

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))),
     )

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"
 license = "MIT"
 license-files = ["LICENSE"]

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_*_<version>) 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_*_<version>_fc_<commit12>) are keyed on
+apn.__version__ and the per-dataset FC pins (apn/data/<dataset>/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

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
 

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_<version>" sleep infinity
+        "$IMAGE_REPOSITORY:LeanOpenProblems_generate_<version>_fc_<commit12>" sleep infinity
+
+(``<commit12>`` 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: