Keep the Lean build trees out of the web image - #24
Merged
Conversation
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.
There was a problem hiding this comment.
Pull request overview
Reduces the deployed web image size and prevents future “build context leaks” (e.g., nested Lean build trees) from shipping to Heroku, which previously caused a boot-time outage due to an oversized image.
Changes:
- Expands
.dockerignoreto excludephyslib/,jixia/, and nested Lean build artifacts (**/.lake/,**/*.olean,**/*.ilean). - Adds a GitHub Actions size gate that builds the Docker image and fails the workflow if it exceeds a configured threshold (6 GB), printing the largest
/appentries for diagnosis.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 1 comment.
| File | Description |
|---|---|
| .github/workflows/weekly-index.yml | Adds an image-size guard step before releasing to prevent deploying oversized images. |
| .dockerignore | Ensures nested Lean/Lake build outputs and cloned repos don’t enter the Docker build context. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
Comment on lines
+335
to
338
| - name: Release Docker image | ||
| if: steps.gate.outputs.proceed == 'true' | ||
| env: | ||
| HEROKU_API_KEY: ${{ secrets.HEROKU_API_KEY }} |
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Root cause of the 2026-08-16 outage
The deployed image was 21 GB. A locally-built one is ~2.9 GB.
The indexing workflow clones PhysLib and jixia into the working directory and builds them with Lake.
COPY . .then baked all 14 GB into the web image..dockerignoredid list.lake/and*.olean, but those patterns only match at the repo root — not the nestedphyslib/.lake/...paths the workflow creates.Heroku gives a dyno ~60s to boot. A 21 GB image cannot be pulled and started in that window, so it was killed before it could come up.
Every prior observation fits: same commit (the build context differed), no R14/R15 (never got far enough to allocate), SIGTERM ~1.3s after Ready, and it only ever broke on workflow-built images. Local builds had no
physlib/directory at all — which is why this was not reproducible locally, and why the earlier-H 0.0.0.0fix looked like a complete solution when it was not.What
physlib/,jixia/, and nested**/.lake/,**/*.olean,**/*.ilean./appentries so the cause is immediately visible.The size guard is the part that generalises — it catches any future context leak, not just this one.
Verified
Reproduced the CI layout locally by planting 800 MB
physlib/and 200 MBjixia/trees: