Merge initial work from develop

.github/workflows/build-docker-images.yaml

@@ -34,13 +34,17 @@ jobs:
             echo "Could not read apn.__version__" >&2
             exit 1
           fi
-          git_hash="$(git rev-parse HEAD)"
           {
-            echo "BASE_IMAGE_TAG=LeanOpenProblems_base_${image_version}_${git_hash}"
-            echo "AGENT_IMAGE_TAG=LeanOpenProblems_agent_${image_version}_${git_hash}"
-            echo "SCORER_IMAGE_TAG=LeanOpenProblems_scorer_${image_version}_${git_hash}"
+            echo "BASE_IMAGE_TAG=LeanOpenProblems_base_${image_version}"
+            echo "CORPUS_IMAGE_TAG=LeanOpenProblems_corpus_${image_version}"
+            echo "AGENT_IMAGE_TAG=LeanOpenProblems_agent_${image_version}"
+            echo "AGENT_CORPUS_IMAGE_TAG=LeanOpenProblems_agent_corpus_${image_version}"
+            echo "SCORER_IMAGE_TAG=LeanOpenProblems_scorer_${image_version}"
           } >> "$GITHUB_ENV"
 
+      - name: Setup buildx
+        uses: docker/setup-buildx-action@b5ca514318bd6ebac0fb2aedd5d36ec1b5c232a2 # v3.10.0
+
       - name: Login to ECR
         uses: docker/login-action@74a5d142397b4f367a81961eba4e8cd7edddf772 # v3.4.0
         with:
@@ -50,7 +54,7 @@ jobs:
         id: image_tags
         run: |-
           repository="${IMAGE_NAME#*/}"
-          for image in base agent scorer; do
+          for image in base corpus agent agent_corpus scorer; do
             tag_var="${image^^}_IMAGE_TAG"
             tag="${!tag_var}"
             if aws ecr describe-images \
@@ -66,48 +70,90 @@ jobs:
       - name: Set reproducible build timestamp
         run: echo "SOURCE_DATE_EPOCH=$(git log -1 --pretty=%ct)" >> "$GITHUB_ENV"
 
-      - name: Prepare base image
-        if: >-
-          steps.image_tags.outputs.base_exists != 'true' ||
-          steps.image_tags.outputs.agent_exists != 'true' ||
-          steps.image_tags.outputs.scorer_exists != 'true'
+      # The three images are stages of the single apn/lean/Dockerfile (which
+      # docker compose also builds on the fly for local runs). The base stage
+      # is pushed as its own image so that later CI runs can skip the
+      # expensive Lean + Mathlib build: the agent/scorer builds override the
+      # `base` stage with the pushed image via a named build context.
+      #
+      # Layer caches are pushed to ECR_CACHE_REGISTRY (mode=max: all layers,
+      # including intermediate stages), keyed by image tag like PortBench --
+      # ECR tags are immutable, so the cache ref must change with the version.
+      - name: Build and push base image
+        if: steps.image_tags.outputs.base_exists != 'true'
         working-directory: apn/lean
         run: |-
-          if [ "${{ steps.image_tags.outputs.base_exists }}" = "true" ]; then
-            docker pull "${IMAGE_NAME}:${BASE_IMAGE_TAG}"
-            docker tag "${IMAGE_NAME}:${BASE_IMAGE_TAG}" apn-lean-base
-          else
-            docker build \
-              -t apn-lean-base \
-              -t "${IMAGE_NAME}:${BASE_IMAGE_TAG}" \
-              -f Dockerfile.base \
-              .
-            docker push "${IMAGE_NAME}:${BASE_IMAGE_TAG}"
-          fi
+          docker buildx build \
+            --target base \
+            --cache-from "type=registry,ref=${{ vars.ECR_CACHE_REGISTRY }}:${BASE_IMAGE_TAG}" \
+            --cache-to "mode=max,image-manifest=true,oci-mediatypes=true,type=registry,ref=${{ vars.ECR_CACHE_REGISTRY }}:${BASE_IMAGE_TAG}" \
+            --push \
+            -t "${IMAGE_NAME}:${BASE_IMAGE_TAG}" \
+            .
+
+      # The corpus stage is self-contained (FROM debian, downloads pinned public
+      # HF datasets) and frozen at a 2022 snapshot, so it's built once and reused
+      # across versions via the registry cache -- no base build context needed.
+      - name: Build and push corpus image
+        if: steps.image_tags.outputs.corpus_exists != 'true'
+        working-directory: apn/lean
+        run: |-
+          docker buildx build \
+            --target corpus \
+            --cache-from "type=registry,ref=${{ vars.ECR_CACHE_REGISTRY }}:${CORPUS_IMAGE_TAG}" \
+            --cache-to "mode=max,image-manifest=true,oci-mediatypes=true,type=registry,ref=${{ vars.ECR_CACHE_REGISTRY }}:${CORPUS_IMAGE_TAG}" \
+            --push \
+            -t "${IMAGE_NAME}:${CORPUS_IMAGE_TAG}" \
+            .
 
       - name: Build and push agent image
         if: steps.image_tags.outputs.agent_exists != 'true'
         working-directory: apn/lean
         run: |-
-          docker build \
+          docker buildx build \
+            --target agent \
+            --build-context "base=docker-image://${IMAGE_NAME}:${BASE_IMAGE_TAG}" \
+            --cache-from "type=registry,ref=${{ vars.ECR_CACHE_REGISTRY }}:${AGENT_IMAGE_TAG}" \
+            --cache-to "mode=max,image-manifest=true,oci-mediatypes=true,type=registry,ref=${{ vars.ECR_CACHE_REGISTRY }}:${AGENT_IMAGE_TAG}" \
+            --push \
             -t "${IMAGE_NAME}:${AGENT_IMAGE_TAG}" \
-            -f Dockerfile.agent \
             .
-          docker push "${IMAGE_NAME}:${AGENT_IMAGE_TAG}"
+
+      # agent_corpus = agent + the corpus layer; override both upstream stages
+      # with their pushed images so neither is rebuilt here.
+      - name: Build and push agent_corpus image
+        if: steps.image_tags.outputs.agent_corpus_exists != 'true'
+        working-directory: apn/lean
+        run: |-
+          docker buildx build \
+            --target agent_corpus \
+            --build-context "base=docker-image://${IMAGE_NAME}:${BASE_IMAGE_TAG}" \
+            --build-context "agent=docker-image://${IMAGE_NAME}:${AGENT_IMAGE_TAG}" \
+            --build-context "corpus=docker-image://${IMAGE_NAME}:${CORPUS_IMAGE_TAG}" \
+            --cache-from "type=registry,ref=${{ vars.ECR_CACHE_REGISTRY }}:${AGENT_CORPUS_IMAGE_TAG}" \
+            --cache-to "mode=max,image-manifest=true,oci-mediatypes=true,type=registry,ref=${{ vars.ECR_CACHE_REGISTRY }}:${AGENT_CORPUS_IMAGE_TAG}" \
+            --push \
+            -t "${IMAGE_NAME}:${AGENT_CORPUS_IMAGE_TAG}" \
+            .
 
       - name: Build and push scorer image
         if: steps.image_tags.outputs.scorer_exists != 'true'
         working-directory: apn/lean
         run: |-
-          docker build \
+          docker buildx build \
+            --target scorer \
+            --build-context "base=docker-image://${IMAGE_NAME}:${BASE_IMAGE_TAG}" \
+            --cache-from "type=registry,ref=${{ vars.ECR_CACHE_REGISTRY }}:${SCORER_IMAGE_TAG}" \
+            --cache-to "mode=max,image-manifest=true,oci-mediatypes=true,type=registry,ref=${{ vars.ECR_CACHE_REGISTRY }}:${SCORER_IMAGE_TAG}" \
+            --push \
             -t "${IMAGE_NAME}:${SCORER_IMAGE_TAG}" \
-            -f Dockerfile.scorer \
             .
-          docker push "${IMAGE_NAME}:${SCORER_IMAGE_TAG}"
 
       - name: Report image repository
         run: |-
           echo "LEAN_OPEN_PROBLEMS_IMAGE_NAME=${IMAGE_NAME}"
           echo "Base image: ${IMAGE_NAME}:${BASE_IMAGE_TAG}"
+          echo "Corpus image: ${IMAGE_NAME}:${CORPUS_IMAGE_TAG}"
           echo "Agent image: ${IMAGE_NAME}:${AGENT_IMAGE_TAG}"
+          echo "Agent-corpus image: ${IMAGE_NAME}:${AGENT_CORPUS_IMAGE_TAG}"
           echo "Scorer image: ${IMAGE_NAME}:${SCORER_IMAGE_TAG}"

.github/workflows/checks.yml

@@ -0,0 +1,61 @@
+name: Checks
+
+on:
+  pull_request:
+  push:
+    branches:
+      - main
+
+jobs:
+  # The CI image tags (LeanOpenProblems_*_<version>) are keyed on
+  # apn.__version__, while the wheel build uses pyproject.toml's version. The two
+  # must stay in lockstep (scripts/bump_version.py edits both) -- this guards
+  # against a bump that touches only one of them.
+  check-version:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Install uv
+        uses: astral-sh/setup-uv@v5
+        with:
+          enable-cache: true
+          cache-dependency-glob: uv.lock
+
+      - name: Set up Python
+        uses: actions/setup-python@v5
+        with:
+          python-version-file: pyproject.toml
+
+      - name: Check apn.__version__ matches pyproject.toml
+        run: |-
+          version_from_init="$(python -c "import apn; print(apn.__version__)")"
+          echo "Version from apn/__init__.py: $version_from_init"
+          version_from_pyproject="$(uv version --short)"
+          echo "Version from pyproject.toml:  $version_from_pyproject"
+          if [ "$version_from_init" != "$version_from_pyproject" ]; then
+            echo "Version mismatch between apn/__init__.py and pyproject.toml"
+            exit 1
+          fi
+
+  tests:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Install uv
+        uses: astral-sh/setup-uv@v5
+        with:
+          enable-cache: true
+          cache-dependency-glob: uv.lock
+
+      - name: Set up Python
+        uses: actions/setup-python@v5
+        with:
+          python-version-file: pyproject.toml
+
+      - name: Install dependencies
+        run: uv sync
+
+      - name: Run tests
+        run: uv run pytest

.gitignore

@@ -18,6 +18,10 @@ logs/
 .inspect/
 configs/history/
 
+# Lean build artifacts (the lake projects ship source only; Docker builds them).
+.lake/
+apn/lean/extract_ranges/lake-manifest.json
+
 # Cloned upstream sources kept for reference, not part of the repo
 reference_sources/