Extend the Lean 4.32 patch to Analyzer/Process.lean

.github/workflows/weekly-index.yml

@@ -129,9 +129,11 @@ jobs:
         uses: actions/cache@v4
         with:
           path: jixia/.lake/build
-          # v2: rebuilt against PhysLib's toolchain (see Build jixia below)
-          key: jixia-v2-${{ hashFiles('physlib/lean-toolchain') }}-${{ hashFiles('jixia/lakefile.lean', 'jixia/lakefile.toml') }}
-          restore-keys: jixia-v2-${{ hashFiles('physlib/lean-toolchain') }}-
+          # Keyed on the compatibility patch too: editing the patch must not reuse
+          # 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') }}-
 
       - name: Build jixia
         id: build_jixia

patches/jixia-lean-4.32.patch

@@ -5,22 +5,46 @@ 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
+Two files need adjusting. In Analyzer/Process/Declaration.lean, Lean tightened
+`do`-block elaboration: `let x := <- e` is no longer accepted
+where `let x <- 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.
+In Analyzer/Process.lean, the `nestedAction` antiquotation now needs an explicit
+`:term` annotation.
+
+These are syntax/API migrations only -- no behavior change. Verified with a
+clean-tree build against v4.32.0 (a cached build hides the Process.lean failure)
+and by confirming declaration, symbol, and docstring extraction are correct.
 
 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 @@
+diff --git a/Analyzer/Process.lean b/Analyzer/Process.lean
+index 36e83d9..db7cf10 100644
+--- a/Analyzer/Process.lean
++++ b/Analyzer/Process.lean
+@@ -81,9 +81,11 @@ elab "impl_process" : term => do
+   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)
+diff --git a/Analyzer/Process/Declaration.lean b/Analyzer/Process/Declaration.lean
+index e770be6..ebddf51 100644
+--- a/Analyzer/Process/Declaration.lean
++++ b/Analyzer/Process/Declaration.lean
+@@ -226,10 +226,10 @@ def getDeclarationInfo (stx : Syntax) : CommandElabM DeclarationInfo := do
        Syntax.node2 .none ``Command.optDeclSig decl[2] decl[4]
      | _ => unreachable!
 
@@ -34,7 +58,7 @@ the workflow applies it only when the unpatched build fails.
      let (binders, type) := match kind with
      | ``Command.«axiom» =>
        expandDeclSig decl[2] |>.map id some
-@@ -239,7 +239,7 @@
+@@ -239,7 +239,7 @@ def getDeclarationInfo (stx : Syntax) : CommandElabM DeclarationInfo := do
      | ``Command.«structure» =>
        (decl[2], decl[4])
      | _ => unreachable!