Add pySpec generator #355
Merged
Add pySpec generator #355
Conversation
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
joehendrix
force-pushed
the
jhx/python_fixes
branch
2 times, most recently
from
5b4ee2b to
76f48c8
Compare
joehendrix
force-pushed
the
jhx/python_fixes
branch
2 times, most recently
from
c535c4c to
ac8d50d
Compare
joehendrix
force-pushed
the
jhx/python_fixes
branch
4 times, most recently
from
21ff87f to
a0ca0b7
Compare
joehendrix
commented
Feb 3, 2026
andrewmwells-amazon
previously approved these changes
Feb 3, 2026
joehendrix
force-pushed
the
jhx/python_fixes
branch
from
d2b6d5f to
8c63528
Compare
joehendrix
force-pushed
the
jhx/python_fixes
branch
from
b29144b to
8c62624
Compare
andrewmwells-amazon
previously approved these changes
Feb 5, 2026
shigoel
previously approved these changes
Feb 5, 2026
- Fix DDM Format bug where identifiers got unnecessary parentheses by setting atom precedence to maxPrec + 1 - Improve Python specs output with bracket formatting for args and kwonly parameters - Add NoArgs variants for types without arguments (cleaner output) - Change arg names from Str to Ident for proper formatting - Remove debug "Running" output from pythonToStrata - Add guard_msgs test to validate clean output format Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>
…ormatting Python changes: - Modified translateImportFrom to check if module is in preludeSig.rank - Builtin modules (typing, builtins, etc.) no longer generate extern declarations - Hoisted check outside loop for efficiency C_Simp changes: - Updated procedure pretty printer to add spaces around "procedure" keyword - Ensures keywords are properly separated from identifiers in output Test updates: - Updated all C_Simp example tests to match new formatting - Fixed DDMAxiomsExtraction expected output - Updated Python SpecsTest expected output Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>
Wrap long comment lines in FileRange.lean, Python.lean, and Specs.lean to adhere to the project's style guideline of 80 characters per line. Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>
Use suffix pattern for function variants to match Lean conventions (e.g., foldl/foldlM, map/mapM, translateModuleAux). Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>
Add concise comments to 19 functions and datatypes where the purpose is not immediately obvious from the name: - DDM/AST.lean: Document flatten, catbvarLevel, NewBindingM, and foldOverArgBindingSpecs - DDM/Ion.lean: Explain StringOrSexp, StructArgMap, and mapFields - DDM/Util/Fin.lean: Document Fin.Range for iteration - Python/Specs.lean: Add context for Pred, Iterable, ModuleName, TypeTranslator, and resolveModule - Python/Specs/DDM.lean: Document conversion functions - Python/Specs/Decls.lean: Explain PythonIdent, MetadataType, unionAux, and SpecPred All comments are 1-3 sentences and focus on semantic information not obvious from names alone. Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>
Update deprecated String API calls to work with Lean 4.27: - Replace String.trim with String.trimAscii.toString - Update String.revFind to String.revFind? - Fix String.Pos dependent type usage in Python.Specs - Replace String.dropRight with String.dropEnd Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>
joehendrix
dismissed stale reviews from shigoel and andrewmwells-amazon
via
b293dad
joehendrix
force-pushed
the
jhx/python_fixes
branch
from
fafb4a6 to
b293dad
Compare
andrewmwells-amazon
approved these changes
Feb 5, 2026
shigoel
approved these changes
Feb 5, 2026
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 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.
This PR introduces a PySpec generator prototype along with several
supporting improvements and bug fixes.
Main Feature: PySpec Generator
Adds a new strata pySpecs subcommand that translates Python
specification files into binary PySpec files. Python specification
files capture method signatures and their pre/post-conditions as
idiomatic Python source code, facilitating LLM-assisted generation.
The binary PySpec format enables efficient loading when validating
source code that uses these imports.
New files:
translation logic
utilities
Refactoring and Code Organization
Source range improvements:
dedicated modules:
types and formatting
Import organization:
Bug Fixes
files (changed .asString to .asSymbolString in
Strata/DDM/Ion.lean)
(changed maxPrec to maxPrec + 1 in atom definition)
spaces (e.g., (bool)proceduretrivial() → bool procedure trivial())
instantiation
parse failures
Testing
fixes
By submitting this pull request, I confirm that you can use, modify,
copy, and redistribute this contribution, under the terms of your
choice.