Normalize Lean 4.33 docstrings before pydantic validates them - #27
Merged
Conversation
The previous fix widened Modifiers' docstring annotation and rebuilt the
model, but indexing still failed on every declaration carrying a docstring:
0.modifiers.docString
Input should be a valid tuple [input_value='The charge density. ']
Declaration and Symbol compile their own nested copy of Modifiers' schema when
their classes are created, so rebuilding Modifiers afterwards leaves those
copies validating against the original tuple-only type. The shim worked when
validating Modifiers directly, which is why it looked correct.
Normalize the raw JSON to the [text, bool] pair before pydantic sees it
instead. Every read goes through RootModel.from_obj, so this covers
Declaration, Symbol, and anything else jixia loads, and it does not depend on
pydantic's schema-rebuild internals. Verified against all three shapes: a 4.33
bare string, a 4.32 pair, and no docstring.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Why
Indexing is still blocked. jixia now builds fine against Lean 4.33 (the patch loop works), but the smoke test rejects its output — every declaration with a docstring fails:
Lean 4.32 emitted
docStringas a[text, bool]pair; 4.33 emits a bare string.Why the previous fix didn't work
#26 widened
Modifiers' annotation and calledmodel_rebuild(force=True). That fixesModifiers.model_validate(...)in isolation — which is presumably how it was checked — but not the real path.DeclarationandSymbolcompile their own nested copy ofModifiers' schema when their classes are created. RebuildingModifiersafterwards leaves those copies validating against the original tuple-only type. Confirmed directly:I also tried clearing
__pydantic_core_schema__/__pydantic_validator__on the dependents and rebuilding — the error persisted (pydantic 2.13.4).What
Normalize the raw JSON to the pair form before pydantic sees it. Every read goes through
RootModel.from_obj, so this coversDeclaration,Symbol, and anything else jixia loads, without depending on pydantic schema internals.Verified
Using the shim exactly as written in the file:
Both Lean versions parse, so this doesn't break if a patch selects a 4.32-shaped build.