Unblock indexing on Lean 4.32, fail loudly when it stalls - #21
Merged
Conversation
Indexing has been stalled since 2026-07-29. PhysLib moved to Lean v4.32.0 and jixia (still on v4.29.0) stopped compiling, so every daily run skipped the whole pipeline -- while reporting success. Three fixes: Add patches/jixia-lean-4.32.patch, which makes jixia build against v4.32.0. Lean tightened do-block elaboration; the patch is a syntax migration only (let x := <- e -> let x <- e, return -> pure, an explicit Option Syntax). Verified by building against v4.32.0 and checking that declaration, symbol, and docstring extraction are correct. The workflow applies it only if the stock build fails, so we return to upstream automatically once jixia catches up and the patch can then be deleted. Fail the run when PhysLib has new content we cannot index. Previously this skipped quietly, which is why nobody noticed for two and a half weeks. An unchanged PhysLib is still a legitimate no-op and stays green. Either way the site is unaffected and keeps serving the last good index. Add a post-load sanity check on row counts. The load is additive, so a jixia that compiles but parses incorrectly would show up as a load that adds nothing rather than as a failure -- worth catching before we publish an index built with a patched analyzer. Also key rate limiting on the forwarded client IP. Requests arrive through the platform router and the Next.js rewrite, so the socket peer is always 127.0.0.1: every visitor shared one bucket, and the new per-endpoint limits would have throttled all users collectively rather than individual abusers.
There was a problem hiding this comment.
Pull request overview
This PR restores automated PhysLib indexing after the Lean 4.32 upgrade by adding a fallback compatibility patch for jixia, making stalled indexing fail loudly when PhysLib has new commits, adding a post-load row-count sanity check, and fixing rate-limiting so it’s keyed per real client IP (via forwarded headers) instead of 127.0.0.1.
Changes:
- Add
patches/jixia-lean-4.32.patchand update the workflow to retry building jixia with it when the upstream build fails. - Change the indexing gate to fail the run when PhysLib has new content that cannot be indexed, and add a DB row-count sanity check after loading.
- Update SlowAPI’s rate-limit key function to use the leftmost
X-Forwarded-Forentry.
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 3 comments.
| File | Description |
|---|---|
server.py |
Uses a forwarded-client IP-based key for rate limiting to avoid sitewide shared buckets. |
patches/jixia-lean-4.32.patch |
Adds a fallback patch to keep jixia compiling against Lean v4.32.0. |
.github/workflows/weekly-index.yml |
Adds fallback patch application, fails loudly when indexing stalls on new PhysLib content, and adds a post-load sanity check. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
Comment on lines
+45
to
+48
| forwarded = request.headers.get("x-forwarded-for") | ||
| if forwarded: | ||
| return forwarded.split(",")[0].strip() | ||
| return get_remote_address(request) |
Comment on lines
+143
to
+147
| # PhysLib bumps Lean faster than jixia supports it, so the stock build can | ||
| # fail on a new Lean release. When that happens, retry with our local | ||
| # compatibility patch. The patch is applied ONLY as a fallback, so the day | ||
| # upstream catches up we silently go back to stock and the patch can be | ||
| # deleted. If neither builds, the gate below skips indexing. |
| print(f"modules={modules} symbols={symbols} declarations={declarations}") | ||
| with open(os.environ["GITHUB_STEP_SUMMARY"], "a") as fh: | ||
| fh.write(f"\nIndex after load: {modules} modules, {symbols} symbols, {declarations} declarations\n") | ||
| # These floors would only be crossed by a analyzer producing garbage; |
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
Indexing has been stalled since 2026-07-29 — ~2.5 weeks of PhysLib commits are missing from the site.
PhysLib moved to Lean v4.32.0 on Jul 21. jixia (still on v4.29.0) stopped compiling, so every daily run since Aug 4 hit the gate and skipped the entire pipeline — while reporting success. The green checkmarks are why it went unnoticed.
What
1.
patches/jixia-lean-4.32.patch— makes jixia build against v4.32.0.Lean tightened
do-block elaboration. The patch is a syntax migration only, no behavior change:let x := ← e→let x ← ereturn→pureinside those branches(none : Option Syntax)in the else-branchDerived from
jarfo/jixia@v4.33.0-rc2, adapted for 4.32 (that branch targets 4.33, wheredocString?takes one field instead of two).Verified:
Build completed successfully (40 jobs)against v4.32.0, and the binary extracts declarations, symbols (19 incl. full structure expansion), and docstrings correctly in a real Lake project.The workflow applies it only if the stock build fails, so we return to upstream automatically once jixia catches up — and the patch can then be deleted.
2. Fail the run when PhysLib has new content we cannot index. Previously it skipped quietly. An unchanged PhysLib is still a legitimate no-op and stays green. The site is unaffected either way — it keeps serving the last good index.
3. Post-load sanity check. The load is additive (
ON CONFLICT DO NOTHING), so a jixia that compiles but parses wrong would look like a load that adds nothing rather than an error. Row-count floors catch that before we publish an index built with a patched analyzer.4. Rate limiting keyed on forwarded client IP. Requests arrive via the platform router → Next.js rewrite, so the socket peer is always
127.0.0.1. Every visitor shared one bucket:@limiter.limit("15/minute")on/expandwas 15/minute sitewide, and the global1/seconddefault was one request per second for the entire site. Now keyed on the leftmostX-Forwarded-Forentry.Risk
The patch touches a third-party analyzer that parses the library. Mitigated by the sanity check (3), and by the patch being fallback-only. First run after merge is worth watching.