From b92a5c1ce5a5336119cc2f0a8ec5d2327c533957 Mon Sep 17 00:00:00 2001
From: Gabriele Battimelli <info@gabrielebattimelli.com>
Date: Sun, 16 Aug 2026 09:17:49 -0400
Subject: [PATCH] Keep the Lean build trees out of the web image

The 2026-08-16 deploy shipped a 21 GB image and the dyno could not boot
inside the platform's startup window, so the site was down until it was
rolled back manually.

The indexing workflow clones physlib/ and jixia/ into the working directory
and builds them with Lake, so COPY . . baked the whole Lean toolchain into
the web image: physlib/ alone was 14 GB, against 148 MB of index that
actually needs to ship. .dockerignore did list .lake/ and *.olean, but those
patterns only match at the root, not the nested paths the workflow creates.

Exclude physlib/ and jixia/ outright, plus nested **/.lake/ and **/*.olean.
Verified by planting 800 MB and 200 MB dummy trees to reproduce the CI
layout: both are excluded from the built image and chroma/ still ships.

Also check the built image size before releasing it, failing with the
largest /app entries listed if it exceeds 6 GB (a healthy image is ~3 GB).
The size limit is the part that generalises: it catches any future leak into
the build context, not just this one. Local builds never had physlib/ in the
first place, which is why this was invisible until it reached production.
---
 .dockerignore                      | 11 +++++++++++
 .github/workflows/weekly-index.yml | 25 +++++++++++++++++++++++--
 2 files changed, 34 insertions(+), 2 deletions(-)

diff --git a/.dockerignore b/.dockerignore
index a77a045..f4eb639 100644
--- a/.dockerignore
+++ b/.dockerignore
@@ -12,6 +12,17 @@ build/
 .idea/
 .vscode/
 .DS_Store
+# Leading-slash-free patterns still only match at the root, so spell out the
+# nested case: the indexing workflow clones and BUILDS these two repos inside
+# the working directory, and `COPY . .` would otherwise bake the whole Lean
+# toolchain into the web image. That is what happened on 2026-08-16 -- physlib/
+# alone was 14 GB, the image reached 21 GB, and the dyno could not start inside
+# the platform's boot window. Neither repo is needed at runtime.
+physlib/
+jixia/
+**/.lake/
+**/*.olean
+**/*.ilean
 .lake/
 *.olean
 *.ilean
diff --git a/.github/workflows/weekly-index.yml b/.github/workflows/weekly-index.yml
index 1629a34..9305a84 100644
--- a/.github/workflows/weekly-index.yml
+++ b/.github/workflows/weekly-index.yml
@@ -27,6 +27,9 @@ jobs:
       # this index competes with the app for the dyno's memory. Warn well before
       # it gets close (Basic/Standard-1X = 512 MB, Standard-2X = 1024 MB).
       CHROMA_MAX_MB: '250'
+      # A healthy image is ~3 GB. On 2026-08-16 a 21 GB image shipped (physlib/
+      # and jixia/ leaked into the build context) and the dyno could not boot.
+      IMAGE_MAX_MB: '6000'
       HEALTHCHECK_URL: https://physlibsearch.net
       CONNECTION_STRING: ${{ secrets.DATABASE_URL }}
       GEMINI_API_KEY: ${{ secrets.GEMINI_API_KEY }}
@@ -310,8 +313,26 @@ jobs:
           echo "prev=$PREV" >> "$GITHUB_OUTPUT"
           echo "Will roll back to v$PREV if the new release is unhealthy."
 
-      # Rebuild the Docker image with the updated chroma/ and deploy
-      - name: Build and release Docker image
+      # The build context contains the cloned+built physlib/ and jixia/ trees.
+      # If .dockerignore ever stops excluding them, the image balloons past what
+      # the platform can boot in its startup window and the site goes down. Check
+      # the built image before releasing it rather than after.
+      - name: Build image and check its size
+        if: steps.gate.outputs.proceed == 'true'
+        env:
+          HEROKU_API_KEY: ${{ secrets.HEROKU_API_KEY }}
+        run: |
+          docker build -t physlibsearch-web .
+          SIZE_MB=$(docker image inspect physlibsearch-web --format '{{.Size}}' | awk '{printf "%d", $1/1048576}')
+          echo "Built image: ${SIZE_MB} MB (limit ${IMAGE_MAX_MB} MB)"
+          echo "Built image: ${SIZE_MB} MB" >> "$GITHUB_STEP_SUMMARY"
+          if [ "$SIZE_MB" -gt "$IMAGE_MAX_MB" ]; then
+            docker run --rm --entrypoint sh physlibsearch-web -c 'du -sh /app/* 2>/dev/null | sort -rh | head -10' || true
+            echo "::error title=Image too large to deploy::Built image is ${SIZE_MB} MB (limit ${IMAGE_MAX_MB} MB). The dyno cannot pull and boot this within the platform's startup window. Largest /app entries are listed above -- most likely .dockerignore stopped excluding physlib/ or jixia/."
+            exit 1
+          fi
+
+      - name: Release Docker image
         if: steps.gate.outputs.proceed == 'true'
         env:
           HEROKU_API_KEY: ${{ secrets.HEROKU_API_KEY }}