From 078744825fab2e21d674d45c732c27a49e497357 Mon Sep 17 00:00:00 2001
From: Gabriele Battimelli <info@gabrielebattimelli.com>
Date: Tue, 18 Aug 2026 17:06:40 -0400
Subject: [PATCH] Accept Lean 4.33's docstring shape, and catch shape changes
 early

The v4.33.0 patch built cleanly and the run then failed two hours later,
partway through the load:

  ValidationError: 4.modifiers.docString
  Input should be a valid tuple [input_value='The speed of light in free space. ']

jixia's model types docString as Lean's older [text, bool] pair, but Lean 4.33
emits a bare string, so every declaration carrying a docstring failed to parse.
Widen the field to accept either shape and read the text through one helper.
Only the text is ever stored, so how Lean represents the flag is not worth
tracking. Verified against both shapes and the null case.

The larger problem is that a compiling jixia proved nothing about whether its
output is usable, and the mismatch only surfaced after a multi-hour load. Add a
smoke test that runs jixia over a single module immediately after building it
and parses the result exactly as the loader does, so this class of breakage
fails in seconds with a clear message instead of hours in.
---
 .github/workflows/weekly-index.yml | 36 ++++++++++++++++++++++++++++++
 database/jixia_db.py               | 20 +++++++++++++++--
 2 files changed, 54 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/weekly-index.yml b/.github/workflows/weekly-index.yml
index 6b4b069..24d0419 100644
--- a/.github/workflows/weekly-index.yml
+++ b/.github/workflows/weekly-index.yml
@@ -190,6 +190,42 @@ jobs:
           exit 1
         timeout-minutes: 30
 
+      # A jixia that compiles can still emit JSON this pipeline cannot parse: the
+      # v4.33.0 patch built fine, then failed two hours into the load because Lean
+      # changed docString from [text, bool] to a bare string. Run jixia over one
+      # small module and parse the result the same way the loader does, so that
+      # class of mismatch surfaces in seconds instead of mid-run.
+      - name: Smoke-test jixia output
+        id: smoke
+        if: steps.build_jixia.outcome == 'success'
+        continue-on-error: true
+        run: |
+          MODULE=$(find physlib/Physlib -name '*.lean' | head -1)
+          echo "Smoke-testing against $MODULE"
+          cd physlib
+          lake env ../jixia/.lake/build/bin/jixia -i \
+            -m /tmp/smoke.mod.json -d /tmp/smoke.decl.json -s /tmp/smoke.sym.json \
+            "../$MODULE" 2>&1 | tail -3
+          cd ..
+          python3 - <<'PY'
+          import sys
+          from jixia.structs import Declaration, Symbol
+          # Import for its compatibility shims before validating anything.
+          import database.jixia_db  # noqa: F401
+          try:
+              decls = Declaration.from_json_file("/tmp/smoke.decl.json")
+              syms = Symbol.from_json_file("/tmp/smoke.sym.json")
+          except Exception as exc:
+              sys.exit(f"::error::jixia output does not match what the loader expects: {exc}")
+          print(f"parsed {len(decls)} declarations, {len(syms)} symbols")
+          PY
+
+      - name: Fail if jixia output is unparseable
+        if: steps.build_jixia.outcome == 'success' && steps.smoke.outcome != 'success'
+        run: |
+          echo "::error title=jixia output incompatible::jixia built, but its output could not be parsed. Lean likely changed a field's shape -- see the smoke-test step. Fix database/jixia_db.py rather than waiting for the multi-hour load to fail."
+          exit 1
+
       # Decide whether indexing can proceed.
       #
       # "PhysLib unchanged" is a real no-op and passes quietly. But if PhysLib has
diff --git a/database/jixia_db.py b/database/jixia_db.py
index c4f11c2..a7f0a4b 100644
--- a/database/jixia_db.py
+++ b/database/jixia_db.py
@@ -4,7 +4,7 @@
 from pathlib import Path
 
 from jixia import LeanProject
-from jixia.structs import LeanName, Symbol, Declaration, is_internal
+from jixia.structs import LeanName, Modifiers, Symbol, Declaration, is_internal
 from psycopg import Connection
 from psycopg.types.json import Jsonb
 from psycopg.types.range import Range
@@ -12,6 +12,22 @@
 logger = logging.getLogger(__name__)
 
 
+# jixia's model types docString as Lean's older [text, bool] pair. Lean 4.33
+# emits a bare string instead, which fails validation for every declaration that
+# has a docstring. Widen the field so either shape parses: only the text is ever
+# stored, so the flag's representation is not something worth tracking.
+Modifiers.model_fields["docstring"].annotation = tuple[str, bool] | str | None
+Modifiers.model_rebuild(force=True)
+
+
+def _docstring_text(modifiers: Modifiers) -> str | None:
+    """The docstring text, however Lean chose to represent it."""
+    docstring = modifiers.docstring
+    if isinstance(docstring, (list, tuple)):
+        return docstring[0] if docstring else None
+    return docstring
+
+
 def _get_signature(declaration: Declaration, module_content):
     if declaration.signature.pp is not None:
         return declaration.signature.pp
@@ -156,7 +172,7 @@ def load_declaration(module_name: LeanName):
                     "index": index,
                     "name": Jsonb(decl.name) if decl.kind != "example" else None,
                     "visible": decl.modifiers.visibility != "private" and decl.kind != "example",
-                    "docstring": decl.modifiers.docstring,
+                    "docstring": _docstring_text(decl.modifiers),
                     "kind": decl.kind,
                     "signature": _get_signature(decl, module_content),
                     "value": _get_value(decl, module_content),