Extend the Lean 4.32 patch to Analyzer/Process.lean - #22
Merged
Conversation
The first version of the patch only covered Analyzer/Process/Declaration.lean. That file built, but the run then failed on Analyzer/Process.lean, which has its own v4.32 incompatibility: the nestedAction antiquotation now needs an explicit :term annotation. Local testing missed this because the build reused cached .olean artifacts for that file; CI built clean and hit it immediately. Re-verified with a from- scratch build (rm -rf .lake/build) against v4.32.0: 40/40 jobs, including Analyzer.Process. Key the jixia cache on the patch file as well, so editing the patch can never reuse a build produced by the previous one.
There was a problem hiding this comment.
Pull request overview
Extends the existing Lean v4.32.0 compatibility patch for the upstream jixia analyzer to cover an additional compile failure in Analyzer/Process.lean, and updates CI caching to avoid reusing stale build artifacts when the patch changes.
Changes:
- Update
patches/jixia-lean-4.32.patchto include theAnalyzer/Process.leanantiquotation fix (explicit:term). - Improve the weekly indexing workflow’s jixia cache key by including the patch file hash (so patch edits force a fresh cache key).
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 1 comment.
| File | Description |
|---|---|
| patches/jixia-lean-4.32.patch | Adds the missing Analyzer/Process.lean fix and updates patch documentation to reflect both required adjustments. |
| .github/workflows/weekly-index.yml | Updates the jixia cache key to include the patch hash to avoid stale cached .olean reuse across patch edits. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
| # a build made from the previous one. A stale cached .olean is exactly | ||
| # what hid the Analyzer/Process.lean failure during local testing. | ||
| key: jixia-v3-${{ hashFiles('physlib/lean-toolchain') }}-${{ hashFiles('jixia/lakefile.lean', 'jixia/lakefile.toml') }}-${{ hashFiles('patches/jixia-lean-4.32.patch') }} | ||
| restore-keys: jixia-v3-${{ hashFiles('physlib/lean-toolchain') }}- |
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.
Why
Run 31915300012 confirmed the patch works —
Analyzer.Process.Declarationbuilt successfully, clearing the original blocker — but the build then failed on a second file:My local verification missed this because the build reused cached
.oleanartifacts for that file. CI built clean and hit it immediately.What
Analyzer/Process.lean: thenestedActionantiquotation now needs an explicit:termannotation (same fix asjarfo/jixia@v4.33.0-rc2).rm -rf .lake/build) against v4.32.0:Build completed successfully (40 jobs), includingAnalyzer.Process.jixia-v3-…) so editing the patch can never reuse a build made from the previous version — the precise trap that hid this failure.Note
The gate correctly failed the run rather than reporting green over a no-op, which is the fail-loudly behavior added in #21 working as intended. Nothing was deployed; the site was unaffected throughout.