Accept Lean 4.33's docstring shape, and catch shape changes early

.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

database/jixia_db.py

@@ -4,14 +4,30 @@
 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
 
 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),