Try every jixia patch instead of hardcoding one Lean release - #25
Merged
Conversation
PhysLib moved to Lean v4.33.0, so the v4.32.0 patch no longer produced a compiling jixia and indexing stopped again. That is the third Lean bump since July while upstream jixia has sat on v4.29.0 since April, so pinning the workflow to a single patch guarantees this recurs. Add patches/jixia-lean-4.33.patch, taken verbatim from jarfo/jixia@v4.33.0-rc2, which targets this release directly. Verified with a clean-tree build: 40/40. Make the build step try upstream first, then every patches/jixia-lean-*.patch in turn, reverting any that applies but fails to build. Both patches apply cleanly to the same regions -- they differ only in whether docString? takes one field or two -- so applying successfully proves nothing and only a build does. Verified by applying the v4.32.0 patch under v4.33.0, watching it fail, and confirming the loop reverts and recovers with the v4.33.0 patch. Supporting a new Lean release is now a matter of dropping in another patch file, with no workflow change. patches/README.md documents how to produce one, including the clean-build requirement -- a cached build previously hid a failure in Analyzer/Process.lean that only surfaced in CI.
There was a problem hiding this comment.
Pull request overview
Updates the weekly indexing workflow so jixia is rebuilt against PhysLib’s current Lean toolchain by attempting upstream first and then iterating through versioned compatibility patches, reducing breakage on frequent Lean bumps.
Changes:
- Add a new jixia compatibility patch for Lean v4.33.0.
- Update the
Build jixiaworkflow step to try upstream unpatched, then try eachpatches/jixia-lean-*.patchuntil one successfully builds (reverting failed patches). - Add
patches/README.mddocumenting how the patch mechanism works and how to produce new patches.
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 2 comments.
| File | Description |
|---|---|
.github/workflows/weekly-index.yml |
Build jixia now loops through all compatibility patches after upstream build fails. |
patches/jixia-lean-4.33.patch |
Introduces a patch to make jixia compile against Lean v4.33.0. |
patches/README.md |
Documents the rationale and workflow behavior for jixia compatibility patches. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
Comment on lines
+179
to
+186
| git apply "$PATCH" | ||
| if lake build; then | ||
| echo "jixia built with $NAME." | ||
| exit 0 | ||
| fi | ||
| echo " $NAME: applied but did not build, reverting" | ||
| git apply -R "$PATCH" | ||
| lake clean || true |
Comment on lines
+175
to
+178
| if ! git apply --check "$PATCH" 2>/dev/null; then | ||
| echo " $NAME: does not apply, skipping" | ||
| continue | ||
| fi |
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
PhysLib moved to Lean v4.33.0, so the v4.32.0 patch stopped producing a compiling jixia and indexing halted again:
That is the third Lean bump since July, while upstream jixia has been on v4.29.0 since April. Pinning the workflow to one patch guarantees this recurs every time.
(The gate correctly failed the run rather than reporting green over a no-op — the fail-loudly behaviour working as intended. The site was never affected.)
What
patches/jixia-lean-4.33.patch— taken verbatim fromjarfo/jixia@v4.33.0-rc2, which targets this release directly. Verified with a clean-tree build against v4.33.0: 40/40 jobs.Build jixianow tries upstream unpatched first, then everypatches/jixia-lean-*.patchin turn, reverting any that applies but fails to build.patches/README.mddocumenting how to produce the next one.Why a loop rather than picking by version
Both patches apply cleanly to the same code regions — they differ only in whether
docString?takes one constructor field (4.33) or two (4.32). Sogit applysucceeding proves nothing; only a successful build does.Verified by simulating exactly what CI will do:
Effect
Supporting a new Lean release is now one new patch file, no workflow change. Upstream is still tried first, so the day jixia catches up we return to stock automatically and the whole
patches/directory can be deleted.