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),