From 17374520d377740cf8c221824a70d841290413e9 Mon Sep 17 00:00:00 2001 From: Gabriele Battimelli Date: Sat, 15 Aug 2026 19:35:26 -0400 Subject: [PATCH] Unblock indexing on Lean 4.32, fail loudly when it stalls 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. --- .github/workflows/weekly-index.yml | 58 ++++++++++++++++++++++++++---- patches/jixia-lean-4.32.patch | 45 +++++++++++++++++++++++ server.py | 14 +++++++- 3 files changed, 110 insertions(+), 7 deletions(-) create mode 100644 patches/jixia-lean-4.32.patch diff --git a/.github/workflows/weekly-index.yml b/.github/workflows/weekly-index.yml index 4c2a190..9103704 100644 --- a/.github/workflows/weekly-index.yml +++ b/.github/workflows/weekly-index.yml @@ -140,17 +140,35 @@ jobs: # to PhysLib's Lean toolchain. Build jixia with the same toolchain so the # olean headers are compatible (otherwise: "incompatible header"). # - # PhysLib bumps Lean faster than jixia supports it, so this build can - # legitimately fail on a brand-new Lean release. That is an upstream lag, - # not a bug in this repo: don't fail the run over it (see the gate below). + # 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. continue-on-error: true run: | cp physlib/lean-toolchain jixia/lean-toolchain - cd jixia && lake build + cd jixia + if lake build; then + echo "jixia built from upstream unpatched." + exit 0 + fi + PATCH=../patches/jixia-lean-4.32.patch + echo "::warning::Stock jixia build failed; retrying with $PATCH" + if ! git apply "$PATCH"; then + echo "::error::Compatibility patch no longer applies to upstream jixia. It likely needs regenerating for the current jixia/Lean versions." + exit 1 + fi + lake build + echo "jixia built with local compatibility patch." timeout-minutes: 30 - # Decide whether indexing can proceed. Skipping cleanly here keeps the site - # serving the last good index instead of failing the daily run outright. + # Decide whether indexing can proceed. + # + # "PhysLib unchanged" is a real no-op and passes quietly. But if PhysLib has + # new content we cannot index, the run FAILS: a daily green check that + # silently indexes nothing is how this went unnoticed for weeks. The site is + # unaffected either way -- it keeps serving the last good index. - name: Gate on jixia compatibility id: gate if: always() @@ -173,7 +191,10 @@ jobs: echo "**Impact:** the index was not updated. The site is unaffected and still serves the previous index." echo "" echo "**Resolution:** wait for jixia to support this Lean release, or pin PhysLib to a commit on a supported toolchain." + echo "" + echo "This run is FAILED on purpose: PhysLib has new content that is not being indexed." } >> "$GITHUB_STEP_SUMMARY" + exit 1 fi - name: Set JIXIA_PATH and LEAN_SYSROOT @@ -204,6 +225,31 @@ jobs: echo "::error::jixia load failed after 3 attempts" exit 1 + # A jixia build that compiles is not necessarily one that parses correctly, + # which matters most when the compatibility patch above is in use. The load + # is additive (ON CONFLICT DO NOTHING), so a broken analyzer shows up as a + # load that adds nothing rather than as an error. Catch that here. + - name: Sanity-check what the load produced + if: steps.gate.outputs.proceed == 'true' + run: | + python3 - <<'PY' + import os, sys, psycopg + with psycopg.connect(os.environ["CONNECTION_STRING"], autocommit=True) as conn, conn.cursor() as c: + c.execute("SELECT COUNT(*) FROM module") + modules = c.fetchone()[0] + c.execute("SELECT COUNT(*) FROM symbol") + symbols = c.fetchone()[0] + c.execute("SELECT COUNT(*) FROM declaration") + declarations = c.fetchone()[0] + 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; + # normal incremental runs land far above them. + if modules < 100 or symbols < 1000 or declarations < 1000: + sys.exit("::error::Implausibly small index after load — treating as a bad jixia build rather than publishing it.") + PY + - name: Informalize new declarations if: steps.gate.outputs.proceed == 'true' run: | diff --git a/patches/jixia-lean-4.32.patch b/patches/jixia-lean-4.32.patch new file mode 100644 index 0000000..74260f3 --- /dev/null +++ b/patches/jixia-lean-4.32.patch @@ -0,0 +1,45 @@ +Fix jixia to compile against Lean v4.32.0. + +PhysLib tracks Lean releases faster than jixia does. jixia must be built with +PhysLib's exact toolchain to read its .olean files, so when PhysLib moved to +v4.32.0 (2026-07-21) indexing stopped: jixia's Declaration.lean no longer +compiled, and the pipeline skipped every run from 2026-07-29 onward. + +Lean tightened `do`-block elaboration: `let x := \u2190 e` is no longer accepted +where `let x \u2190 e` is meant, `return` inside these branches now infers the +wrong type, and the else-branch needs an explicit `Option Syntax` annotation. +These are syntax/API migrations only \u2014 no behavior change. Verified by +building against v4.32.0 and confirming declaration, symbol, and docstring +extraction match expectations. + +Derived from jarfo/jixia@v4.33.0-rc2, adapted for v4.32.0 (that branch targets +4.33, where `docString?` takes one field instead of two). + +Remove this patch once upstream jixia supports the toolchain PhysLib is on; +the workflow applies it only when the unpatched build fails. + +--- a/Analyzer/Process/Declaration.lean 2026-08-15 19:33:12 ++++ b/Analyzer/Process/Declaration.lean 2026-08-15 19:27:20 +@@ -226,10 +226,10 @@ + Syntax.node2 .none ``Command.optDeclSig decl[2] decl[4] + | _ => unreachable! + +- let (id, binders, type, value) := ← if isDefLike decl then do ++ let (id, binders, type, value) ← if isDefLike decl then do + let defView ← mkDefView modifiers decl +- return (defView.declId, defView.binders, defView.type?, some defView.value) +- else ++ pure (defView.declId, defView.binders, defView.type?, some defView.value) ++ else do + let (binders, type) := match kind with + | ``Command.«axiom» => + expandDeclSig decl[2] |>.map id some +@@ -239,7 +239,7 @@ + | ``Command.«structure» => + (decl[2], decl[4]) + | _ => unreachable! +- return (decl[1], binders, type, none) ++ pure (decl[1], binders, type, (none : Option Syntax)) + + let name := id[0].getId + let name ← getFullname modifiers name diff --git a/server.py b/server.py index ac874ef..77a1f0a 100644 --- a/server.py +++ b/server.py @@ -36,7 +36,19 @@ async def lifespan(app: FastAPI): yield -limiter = Limiter(key_func=get_remote_address, default_limits=["1/second"]) +def client_key(request: Request) -> str: + # Requests reach this app through two proxies (the platform router, then the + # Next.js rewrite), so the socket peer is always 127.0.0.1 -- keying on it + # would put every visitor in one shared bucket and let a handful of users + # rate-limit everyone else. Use the originating client from X-Forwarded-For + # (leftmost entry) and fall back to the peer address only if it's absent. + forwarded = request.headers.get("x-forwarded-for") + if forwarded: + return forwarded.split(",")[0].strip() + return get_remote_address(request) + + +limiter = Limiter(key_func=client_key, default_limits=["1/second"]) app = FastAPI(lifespan=lifespan) app.state.limiter = limiter app.add_exception_handler(RateLimitExceeded, _rate_limit_exceeded_handler)