Bake Mathlib build cache into CI image

.github/actions/free-disk-space/action.yml

@@ -1,20 +1,25 @@
 name: 'Free Runner Disk Space'
 description: >-
-  Drop the bind-mounted /opt/hostedtoolcache before heavy lake/mathlib
-  steps. GH-hosted Ubuntu runners preinstall ~14 GB of language
-  toolchains (Python/Node/Ruby/Go/Java/.NET) under that path, which the
-  container sees as /__t. Our jobs never use any of it, but
-  `lake exe cache get` decompresses ~8 k mathlib oleans into the same
-  disk and the combined peak occasionally exceeds the runner disk
+  Drop the preinstalled toolchain bloat before heavy lake/mathlib or
+  docker-build steps. GH-hosted Ubuntu runners preinstall ~14 GB of language
+  toolchains (Python/Node/Ruby/Go/Java/.NET) under /opt/hostedtoolcache,
+  which container jobs see bind-mounted as /__t. Our jobs never use any of
+  it, but `lake exe cache get` decompresses ~8 k mathlib oleans into the
+  same disk and the combined peak occasionally exceeds the runner disk
   limit, manifesting as `No space left on device` mid-decompression.
-  Drop the tool cache proactively to give decompression headroom.
+  Inside a container the action clears /__t; on the host it removes the
+  tool cache plus the Android SDK and .NET trees.
 runs:
   using: 'composite'
   steps:
-    - name: Free /opt/hostedtoolcache
+    - name: Free Preinstalled Toolchains
       shell: bash
       run: |
         set -eu
         df -h /
-        rm -rf /__t/*
+        if [ -d /__t ]; then
+          rm -rf /__t/*
+        else
+          sudo rm -rf /opt/hostedtoolcache /usr/local/lib/android /usr/share/dotnet
+        fi
         df -h /

.github/workflows/build-ci-image.yaml

@@ -7,18 +7,22 @@ on:
         type: boolean
     outputs:
       image_tag:
-        value: ${{ jobs.build.outputs.image_tag }}
+        value: ${{ jobs.check.outputs.image_tag }}
 
 permissions:
   contents: read
   packages: write
 
 jobs:
-  build:
-    name: Build CI Image
+  check:
+    name: Check CI Image
     runs-on: ubuntu-latest
     outputs:
       image_tag: ${{ steps.versions.outputs.image_tag }}
+      exists: ${{ steps.exists.outputs.exists }}
+      rust_stable: ${{ steps.versions.outputs.rust_stable }}
+      lean_toolchain: ${{ steps.versions.outputs.lean_toolchain }}
+      noir_rev: ${{ steps.versions.outputs.noir_rev }}
     steps:
       - name: Checkout
         uses: actions/checkout@v6
@@ -31,15 +35,38 @@ jobs:
           registry: ghcr.io
           username: ${{ github.actor }}
           password: ${{ secrets.GITHUB_TOKEN }}
-      - name: Check CI Image
-        id: check
+      - name: Probe Image Manifest
+        id: probe
         continue-on-error: true
-        run: python3 scripts/ci/verify_ci_image.py ghcr.io/reilabs/lampe-ci:${{ steps.versions.outputs.image_tag }}
+        run: docker manifest inspect ghcr.io/reilabs/lampe-ci:${{ steps.versions.outputs.image_tag }} > /dev/null
+      - name: Record Image Existence
+        id: exists
+        run: |
+          if [ "${{ steps.probe.outcome }}" = "success" ]; then
+            echo "exists=true" >> "$GITHUB_OUTPUT"
+          else
+            echo "exists=false" >> "$GITHUB_OUTPUT"
+          fi
+
+  build:
+    name: Build And Push CI Image
+    needs: check
+    if: needs.check.outputs.exists != 'true' && inputs.allow_push
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v6
+      - name: Free Runner Disk Space
+        uses: ./.github/actions/free-disk-space
+      - name: Log In To GHCR
+        uses: docker/login-action@v3
+        with:
+          registry: ghcr.io
+          username: ${{ github.actor }}
+          password: ${{ secrets.GITHUB_TOKEN }}
       - name: Set Up Docker Buildx
-        if: steps.check.outcome == 'failure' && inputs.allow_push
         uses: docker/setup-buildx-action@v3
       - name: Build And Push Image
-        if: steps.check.outcome == 'failure' && inputs.allow_push
         uses: docker/build-push-action@v6
         with:
           context: .
@@ -49,13 +76,19 @@ jobs:
           tags: |
             ghcr.io/reilabs/lampe-ci:latest
             ghcr.io/reilabs/lampe-ci:sha-${{ github.sha }}
-            ghcr.io/reilabs/lampe-ci:${{ steps.versions.outputs.image_tag }}
+            ghcr.io/reilabs/lampe-ci:${{ needs.check.outputs.image_tag }}
           build-args: |
-            RUST_TOOLCHAIN_STABLE=${{ steps.versions.outputs.rust_stable }}
-            LEAN_TOOLCHAIN=${{ steps.versions.outputs.lean_toolchain }}
-            NOIR_REV=${{ steps.versions.outputs.noir_rev }}
-      - name: Fail If Image Missing
-        if: steps.check.outcome == 'failure' && !inputs.allow_push
+            RUST_TOOLCHAIN_STABLE=${{ needs.check.outputs.rust_stable }}
+            LEAN_TOOLCHAIN=${{ needs.check.outputs.lean_toolchain }}
+            NOIR_REV=${{ needs.check.outputs.noir_rev }}
+
+  guard:
+    name: Fail If Image Missing
+    needs: check
+    if: needs.check.outputs.exists != 'true' && !inputs.allow_push
+    runs-on: ubuntu-latest
+    steps:
+      - name: Report Missing Image
         run: |
-          echo "CI image ghcr.io/reilabs/lampe-ci:${{ steps.versions.outputs.image_tag }} is missing and cannot be built from a fork."
+          echo "CI image ghcr.io/reilabs/lampe-ci:${{ needs.check.outputs.image_tag }} is missing and cannot be built from a fork."
           exit 1

.github/workflows/ci-noir.yaml

@@ -12,7 +12,7 @@ jobs:
   build-ci-image:
     uses: ./.github/workflows/build-ci-image.yaml
     with:
-      allow_push: ${{ github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository }}
+      allow_push: true
 
   run-tests:
     name: Test Noir