Improve pySpecs robustness: graceful failures, regex support, and reusable API#512
Open
joehendrix wants to merge 1 commit intomainfrom
Open
Improve pySpecs robustness: graceful failures, regex support, and reusable API#512joehendrix wants to merge 1 commit intomainfrom
joehendrix wants to merge 1 commit intomainfrom
Conversation
cfe01d0 to
af909a0
Compare
Improves the robustness of the pySpecs command so it reports failures gracefully — including regex usage — instead of aborting, and extracts the core logic into a reusable API with CLI flags for skipping definitions, controlling verbosity, and selecting log events. - Graceful failure handling: when a Python import cannot be resolved, the translator now registers the imported names as opaque extern types and continues, rather than aborting. Overload stubs with unexpected bodies produce a warning instead of failing. - Regex support: `from re import compile` is recognized via the built-in prelude, so Python files that use regex no longer trigger unknown-identifier errors. - Reusable API: the translation logic that was inline in the CLI callback is extracted into a self-contained entry point in SimpleAPI, returning structured errors instead of calling exitFailure. - CLI flags: --skip omits named top-level definitions (overloads kept), --quiet suppresses logging and warnings, --log enables event types. - Warning pipeline: warnings are collected during translation and returned as data; a three-level verbosity setting controls reporting. - Composable assertion expressions: the expression tree is refactored from fused nodes into orthogonal building blocks, making serialization a direct structural recursion with no special cases. - Readable DDM output: ensure(pred, msg) format, infix comparisons, indented class member blocks. - Event logging cleanup: global mutable reference replaced by a context- threaded event set.
af909a0 to
bbb3c3b
Compare
shigoel
reviewed
Mar 6, 2026
| -- Parse skip names into PythonIdents | ||
| let some fileStem := pythonFile.fileStem | ||
| | throw s!"No file stem for {pythonFile}" | ||
| let stem := fileStem |
Contributor
There was a problem hiding this comment.
Nit: looks like fileStem can be used everywhere and stem isn't needed
shigoel
reviewed
Mar 6, 2026
| def ppSourceRange (fmm : FileMaps) (path : System.FilePath) (loc : SourceRange) : String := | ||
| match fmm[path]? with | ||
| | none => | ||
| panic! "Invalid path {file}" |
Contributor
There was a problem hiding this comment.
Out of scope for this PR, but noting a panic here that'd be a good candidate to convert to an exception.
shigoel
approved these changes
Mar 6, 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
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.
Summary
Improves the robustness of the
pySpecscommand so it reports failuresgracefully — including regex usage — instead of aborting, and extracts
the core logic into a reusable API with CLI flags for skipping
definitions, controlling verbosity, and selecting log events.
Details
the translator now registers the imported names as opaque extern types
and continues, rather than aborting. This means downstream references
to those names still produce valid (if incomplete) output. Overload
stubs with unexpected bodies produce a warning instead of failing.
from re import compileis recognized via thebuilt-in prelude, so Python files that use regex no longer trigger
unknown-identifier errors. A test confirms this import resolves
without warnings.
callback is extracted into a self-contained entry point in SimpleAPI.
It validates inputs, parses skip-name strings, translates, writes
output, and reports warnings — all returning structured errors instead
of calling
exitFailure. The CLI callback now delegates to this.--skip <name>omits named top-level definitions fromoutput (overloaded variants are always kept).
--quietsuppresseslogging and warnings.
--log <event>enables specific event types.and returned to the caller as data, rather than being printed to
stderr internally. A three-level verbosity setting (none / summary /
detail) controls how they are reported.
preconditions and postconditions is refactored from fused nodes
(e.g., "length >= N" as one node) into orthogonal building blocks
(length, integer literal, greater-or-equal, etc.). This makes
serialization a direct structural recursion with no special cases.
ensure(pred, msg).Comparisons use infix
>=/<=. Class member blocks are indentedon separate lines. These changes make the generated specs easier to
read and diff.
reference; the set of enabled events is threaded through the
translation context. Import messages now report after completion
(past tense) and include warning counts.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.