Apply Bloom's statement-selection verdicts; add the bloom68 config (#35) #43
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 }} | |
| AWS_ECR_PUSH_ROLE: ${{ vars.AWS_ECR_PUSH_ROLE }} | |
| 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: ${{ env.AWS_ECR_PUSH_ROLE }} | |
| - uses: actions/checkout@v4 | |
| - 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 }} | |
| # 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: |- | |
| 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 "version=$image_version" >> "$GITHUB_OUTPUT" | |
| 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 | |
| for target in agent agent_corpus comparator; 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 per | |
| # FC pin. | |
| - name: Build and push images | |
| if: steps.missing.outputs.builds != '' | |
| working-directory: apn/lean | |
| run: |- | |
| 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 }}_fc_${commit:0:12}" \ | |
| . | |
| done <<< "${{ steps.missing.outputs.builds }}" |