Skip to content

Per-dataset FC pins for the sandbox images - #21

Merged
tadamcz merged 3 commits into
mainfrom
per-dataset-fc-pins
Aug 11, 2026
Merged

Per-dataset FC pins for the sandbox images#21
tadamcz merged 3 commits into
mainfrom
per-dataset-fc-pins

Conversation

@tadamcz

@tadamcz tadamcz commented Aug 11, 2026

Copy link
Copy Markdown
Collaborator

Each dataset (erdos, fc100open, oeis) now pins its own formal-conjectures commit in apn/data/<dataset>/fc_commit, instead of one hash baked into every image via a Dockerfile ARG default. All three pins are initially the same constant (67338a15, the previous value), so image content is unchanged.

  • The pin flows into the generated compose files as the FC_COMMIT build arg — the Dockerfile's only ARG without a default (docker has no native required-arg mechanism; a build missing it fails at the checkout).
  • Image tags become LeanOpenProblems_<kind>_<version>_fc_<commit12>, so datasets sharing a pin share images by construction, and changing a pin alone triggers a fresh CI build of the missing tags.
  • The FC branch is no longer recorded anywhere: a plain git clone fetches all branch refs, so checkout by commit reaches commits on any branch (--single-branch is only implied by --depth, which we don't use).
  • CI builds the distinct-pins × targets matrix, reading pins with sort -u apn/data/*/fc_commit.
  • The per-dataset isolation test suites and test_gold_proofs build their sandbox at their dataset's pin; the dataset-agnostic suites use the oeis pin.
  • Version bumped to 0.1.6 for clarity (not strictly required — the new tag component already changes every tag).

Rollout note: on merge, CI sees three missing tags and builds+pushes once; a hawk run launched before that push would reference a not-yet-pushed tag (same window as after any version bump).

Validated locally: full docker compose build of agent+scorer from the generated compose (public base images, FC_COMMIT passed through), plus test_single_file_proof_is_accepted end-to-end against the freshly built images through Inspect's real sandbox lifecycle; fast suites (test_fc_pins, test_registry) and mypy clean.

Each dataset now pins its own formal-conjectures commit in
apn/data/<dataset>/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_<kind>_<version>_fc_<commit12>), 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.
Not strictly required (the new _fc_<commit12> tag component already
changes every tag), but makes the pin-keyed image generation obvious.
@tadamcz
tadamcz merged commit a08ae16 into main Aug 11, 2026
5 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant