From 9f4452a6ae4f1e2b5126c64d92c075d1e6a8e185 Mon Sep 17 00:00:00 2001
From: Gabriele Battimelli <info@gabrielebattimelli.com>
Date: Sat, 15 Aug 2026 19:46:54 -0400
Subject: [PATCH] Extend the Lean 4.32 patch to Analyzer/Process.lean

The first version of the patch only covered Analyzer/Process/Declaration.lean.
That file built, but the run then failed on Analyzer/Process.lean, which has
its own v4.32 incompatibility: the nestedAction antiquotation now needs an
explicit :term annotation.

Local testing missed this because the build reused cached .olean artifacts for
that file; CI built clean and hit it immediately. Re-verified with a from-
scratch build (rm -rf .lake/build) against v4.32.0: 40/40 jobs, including
Analyzer.Process.

Key the jixia cache on the patch file as well, so editing the patch can never
reuse a build produced by the previous one.
---
 .github/workflows/weekly-index.yml |  8 +++---
 patches/jixia-lean-4.32.patch      | 42 +++++++++++++++++++++++-------
 2 files changed, 38 insertions(+), 12 deletions(-)

diff --git a/.github/workflows/weekly-index.yml b/.github/workflows/weekly-index.yml
index 9103704..f8184bc 100644
--- a/.github/workflows/weekly-index.yml
+++ b/.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
diff --git a/patches/jixia-lean-4.32.patch b/patches/jixia-lean-4.32.patch
index 74260f3..3938071 100644
--- a/patches/jixia-lean-4.32.patch
+++ b/patches/jixia-lean-4.32.patch
@@ -5,12 +5,16 @@ 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).
@@ -18,9 +22,29 @@ Derived from jarfo/jixia@v4.33.0-rc2, adapted for v4.32.0 (that branch targets
 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!