Build LeanOpenProblems Docker Images and Upload to Amazon ECR #9
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Build LeanOpenProblems Docker Images and Upload to Amazon ECR | |
| on: | |
| workflow_dispatch: | |
| push: | |
| branches: [main] | |
| permissions: | |
| contents: read | |
| id-token: write | |
| env: | |
| IMAGE_NAME: ${{ vars.ECR_REGISTRY }} | |
| jobs: | |
| publish-lean-images: | |
| runs-on: epoch-research-x64-64core-256GB-2040GB | |
| steps: | |
| - name: Derive AWS region from ECR registry | |
| id: ecr | |
| run: echo "region=$(echo '${{ vars.ECR_REGISTRY }}' | cut -d. -f4)" >> "$GITHUB_OUTPUT" | |
| - uses: aws-actions/configure-aws-credentials@b47578312673ae6fa5b5096b330d9fbac3d116df # v4.2.1 | |
| with: | |
| aws-region: ${{ steps.ecr.outputs.region }} | |
| role-to-assume: arn:aws:iam::328726945407:role/production-github-actions-epochai | |
| - uses: actions/checkout@v4 | |
| - name: Set image tags | |
| run: |- | |
| image_version="$(sed -nE 's/^__version__ = "([^"]+)"/\1/p' apn/__init__.py)" | |
| if [ -z "$image_version" ]; then | |
| echo "Could not read apn.__version__" >&2 | |
| exit 1 | |
| fi | |
| { | |
| 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: | |
| registry: ${{ vars.ECR_REGISTRY }} | |
| - name: Check existing image tags | |
| id: image_tags | |
| run: |- | |
| repository="${IMAGE_NAME#*/}" | |
| for image in base corpus agent agent_corpus scorer; do | |
| tag_var="${image^^}_IMAGE_TAG" | |
| tag="${!tag_var}" | |
| if aws ecr describe-images \ | |
| --repository-name "$repository" \ | |
| --image-ids "imageTag=$tag" \ | |
| >/dev/null 2>&1; then | |
| echo "${image}_exists=true" >> "$GITHUB_OUTPUT" | |
| else | |
| echo "${image}_exists=false" >> "$GITHUB_OUTPUT" | |
| fi | |
| done | |
| - name: Set reproducible build timestamp | |
| run: echo "SOURCE_DATE_EPOCH=$(git log -1 --pretty=%ct)" >> "$GITHUB_ENV" | |
| # 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: |- | |
| 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 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}" \ | |
| . | |
| # 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 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}" \ | |
| . | |
| - 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}" |