Merged
Conversation
Document the strata.base Python API in DDMDoc.lean (Dialect, Program, Init, declarations, AST node types, metadata) and create PythonDialect.md for the auto-generated Python dialect, CLI commands, and Parser API. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Verso's InlineLean elaboration interprets language-annotated code blocks as Lean constants, causing "Unknown constant `python`" build errors. Use bare code fences to match the rest of DDMDoc. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
joehendrix
force-pushed
the
jhx/python-doc
branch
from
41c9b23 to
65d2fad
Compare
tautschnig
previously approved these changes
Apr 3, 2026
- Add missing `Init` import in "Adding Operators" code block - Define `val` variable in OpDecl usage example (was `some_expr`) - Add `decl_list` syncat and use defined variables in metadata example - Add cross-reference to Building Programs section for context Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Pass tuples instead of lists to add_syncat in Init setup to match the type signature `tuple[str, ...] | None`. Make the DDM Manual reference in PythonDialect.md a relative link for GitHub navigation. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
tautschnig
previously approved these changes
Apr 3, 2026
MikaelMayer
reviewed
Apr 3, 2026
atomb
previously approved these changes
Apr 3, 2026
Contributor
|
I like having this included in the DDM manual, and perhaps the Java API documentation (#694) should move there, too (though I'm inclined to merge that PR as-is and then possibly migrate it). |
- Trim README CLI sections to a Quick Start with pointer to PythonDialect.md, avoiding duplicate maintenance (MikaelMayer) - Link PythonDialect.md to deployed DDM Manual at strata-org.github.io instead of Lean source file (MikaelMayer) - Link DDMDoc.lean PythonDialect.md reference to GitHub blob URL so it works in rendered HTML (MikaelMayer) Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
tautschnig
approved these changes
Apr 3, 2026
atomb
approved these changes
Apr 3, 2026
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
4 participants
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.
Add documentation for the strata Python package so that developers can work with DDM concepts without reading Lean source code.
Changes
1. Python section in DDMDoc.lean
The DDM manual had no coverage of the Python API — developers had to read
base.pysource to understand how to create dialects, build programs, or serialize to Ion. The new section documents thestrata.basemodule:Dialect,Program,Init, declarations (SynCatDecl,OpDecl,ArgDecl), AST node types, collections, source locations, and metadata. It maps Python types to their Lean generic AST counterparts (Operation↔OperationF, etc.) and notes gaps like the missingSpaceSepBy/SpacePrefixSepBycategories. Placed before the existing "Command Line Use" stub so it flows naturally after Lean integration.2. Tools/Python/PythonDialect.md
The existing README covers CLI invocations but not how the Python dialect is structured or how to use the parser programmatically. The new Markdown file explains the dialect generation process (reflecting over CPython's
astmodule), the type mapping from Python AST to DDM categories, theParserclass andgen_dialect()API, and version compatibility across Python 3.11–3.14. Kept as Markdown rather than Verso since this is engineer-facing tooling documentation, not a formal manual.3. Tools/Python/README.md pointer updates
Added cross-references to the DDM manual and PythonDialect.md so engineers landing in
Tools/Pythoncan find the right documentation quickly.By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.