Try every jixia patch instead of hardcoding one Lean release

.github/workflows/weekly-index.yml

@@ -145,27 +145,49 @@ 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 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.
+        # PhysLib bumps Lean faster than jixia supports it (three bumps since July
+        # while jixia sat on v4.29.0), so the stock build usually fails. Fall back
+        # to the compatibility patches in patches/, trying each until one builds.
+        #
+        # Each patch targets a specific Lean release and they are NOT
+        # interchangeable -- e.g. `docString?` takes two fields in v4.32.0 and one
+        # in v4.33.0 -- so adding support for a new Lean release means dropping in
+        # another patch file here, with no change to this workflow.
+        #
+        # Stock is always tried first, so the day upstream catches up we go back to
+        # it automatically and the patches can be deleted. If nothing builds, the
+        # gate below fails the run rather than silently skipping.
         continue-on-error: true
         run: |
           cp physlib/lean-toolchain jixia/lean-toolchain
+          TOOLCHAIN=$(cat physlib/lean-toolchain)
           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."
+
+          echo "::warning::Stock jixia build failed against $TOOLCHAIN; trying compatibility patches."
+          for PATCH in ../patches/jixia-lean-*.patch; do
+            [ -e "$PATCH" ] || continue
+            NAME=$(basename "$PATCH")
+            if ! git apply --check "$PATCH" 2>/dev/null; then
+              echo "  $NAME: does not apply, skipping"
+              continue
+            fi
+            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
+          done
+
+          echo "::error title=No jixia build works::Neither upstream jixia nor any patch in patches/ builds against $TOOLCHAIN. A new patch is needed for this Lean release -- see patches/README.md."
+          exit 1
         timeout-minutes: 30
 
       # Decide whether indexing can proceed.

patches/README.md

@@ -0,0 +1,70 @@
+# jixia compatibility patches
+
+The indexing pipeline runs [jixia](https://github.com/frenzymath/jixia) over
+PhysLib. jixia reads PhysLib's compiled `.olean` files, whose headers are locked
+to an exact Lean version, so **jixia must be built with PhysLib's exact
+toolchain**. Otherwise every module fails with `incompatible header`.
+
+PhysLib tracks Lean releases closely — v4.32.0 in July 2026, v4.33.0 weeks later
+— while upstream jixia has been on v4.29.0 since April 2026. So jixia usually
+does not compile against the toolchain PhysLib is currently on, and the pipeline
+needs a patch to bridge the gap.
+
+## How the workflow uses these
+
+`Build jixia` tries, in order:
+
+1. **Upstream jixia, unpatched.** If this works the patches are unnecessary and
+   should be deleted.
+2. **Each `jixia-lean-*.patch` in turn**, skipping any that no longer apply and
+   reverting any that apply but fail to build.
+
+If nothing builds, the run fails rather than quietly skipping — a green run that
+indexes nothing once went unnoticed for two and a half weeks.
+
+Adding support for a new Lean release means **dropping in another patch file**.
+The workflow needs no change.
+
+## Why there is one patch per Lean version
+
+The patches are not interchangeable. `docString?` takes two constructor fields in
+v4.32.0 and one in v4.33.0, so a single patch cannot satisfy both.
+
+## Writing a new patch
+
+The changes so far have been mechanical migrations, not logic changes:
+
+- `let x := ← e` → `let x ← e` (Lean tightened `do`-block elaboration)
+- `return` → `pure` inside those branches
+- an explicit `(none : Option Syntax)` where the type is no longer inferred
+- an explicit `:term` antiquotation annotation in `nestedAction`
+
+Check [jarfo/jixia](https://github.com/jarfo/jixia) first — that fork has carried
+branches targeting newer Lean releases (`v4.33.0-rc2` was usable verbatim), which
+is where both current patches came from.
+
+To produce one:
+
+```sh
+git clone --depth 1 https://github.com/frenzymath/jixia jixia-upstream
+git clone --depth 1 -b <branch> https://github.com/jarfo/jixia jixia-fixed
+cd jixia-fixed
+echo "leanprover/lean4:vX.Y.Z" > lean-toolchain   # match PhysLib exactly
+rm -rf .lake/build && lake build                  # MUST be a clean build
+```
+
+A clean build is not optional. A cached build once hid a failure in
+`Analyzer/Process.lean` that only surfaced in CI, because the stale `.olean` was
+reused instead of recompiled.
+
+Once it builds, diff the changed files against upstream and save the result as
+`patches/jixia-lean-<version>.patch` with `a/` and `b/` path prefixes so
+`git apply` accepts it. Prose above the first `---` line is ignored by
+`git apply`, so explain the change there.
+
+## Removing them
+
+When upstream jixia supports the toolchain PhysLib is on, step 1 succeeds and the
+patches stop being consulted. Delete them then — they are dead weight, and a
+stale patch that still applies but produces subtly wrong output is worse than no
+patch at all.

patches/jixia-lean-4.33.patch

@@ -0,0 +1,65 @@
+Fix jixia to compile against Lean v4.33.0.
+
+Same situation as the v4.32.0 patch beside this one: PhysLib tracks Lean
+releases (v4.32.0 on 2026-07-21, v4.33.0 shortly after) far faster than
+upstream jixia, which has been on v4.29.0 since April.
+
+Taken verbatim from jarfo/jixia@v4.33.0-rc2, which targets this Lean release
+directly. The only difference from the v4.32.0 patch is `docString?`, which
+takes one field here and two in v4.32.0 -- so the two patches cannot be
+merged into one, and the workflow tries each in turn.
+
+Verified with a clean-tree build against v4.33.0: 40/40 jobs.
+
+Delete this once upstream jixia supports the toolchain PhysLib is on.
+
+--- a/Analyzer/Process/Declaration.lean	2026-08-18 11:14:40
++++ b/Analyzer/Process/Declaration.lean	2026-08-18 11:12:36
+@@ -176,7 +176,7 @@
+   let scopeInfo ← getScopeInfo
+   let mut modifiers ← elabModifiers stx[2]
+   if let some leadingDocComment := stx[0].getOptional? then
+-    modifiers := { modifiers with docString? := some ⟨leadingDocComment, false⟩ }
++    modifiers := { modifiers with docString? := some ⟨leadingDocComment⟩ }
+   let id := stx[3]
+   let name := id.getId
+   let name ← getFullname modifiers <| parentName ++ name
+@@ -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
+--- a/Analyzer/Process.lean	2026-08-18 11:14:40
++++ b/Analyzer/Process.lean	2026-08-18 11:12:36
+@@ -81,9 +81,11 @@
+   let body ← Process.plugins.mapM fun (name, plugin) => do
+     let cond := mkIdent (param ++ name ++ (Name.mkSimple "isPresent"))
+     let action := mkIdent (param ++ name ++ (Name.mkSimple "output"))
+-    let term := mkIdent plugin.getResult
++    let getResult := mkIdent plugin.getResult
++    -- `nestedAction` parses a `doElem` after `←`, so the antiquotation needs an explicit
++    -- `:term` annotation
+     return (← `(doSeqItem| if $cond then
+-      $action:term (← $term)
++      $action:term (← $getResult:term)
+     ))
+   let term ← `(fun $(mkIdent param) => do $body*)
+   let type ← `(Options → CommandElabM Unit)