Skip to content

Conversation

@joehendrix
Copy link
Contributor

@joehendrix joehendrix commented Jan 29, 2026

Description of changes:

This PR is mostly about adding a pySpec generator, but does some other cleanups that will hopefully be uncontroversial.

The "pySpec generator" is a prototype strata subcommand that takes a Python file as an argument, and produces a PySpec DDM Program for the file and its imports. The Python files it processes are intended to capture Python method signatures and their pre and post-conditions as idiomatic Python source code. This should facilitate use of LLMs to generate them.

PySpec files are binary files that have semi-compiled the specifications. This is intended to make them efficient to load PySpec files when trying to validate source code that uses those imports.

The minor changes include:

  1. Migrating some of the source mapping information from the DDM AST package to a Utils package to reduce unnecessary code in the DDM.
  2. Fixing a minor bug in parsing DDM Ident types in Ion files.
  3. Making the FormatState empty def public so it is public inhabited.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

@joehendrix joehendrix changed the title Lean code to run Python strata.gen Add pySpec generator Jan 29, 2026
@joehendrix joehendrix marked this pull request as ready for review January 30, 2026 06:55
@joehendrix joehendrix requested a review from a team as a code owner January 30, 2026 06:55
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant