kompilex command for pyk #4342
Merged
kompilex command for pyk #4342
Conversation
This file contains 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
Some attributes in the bootstrapped prelude modules that the java frontend emits are dictionaries, which get loaded in as FrozenDict's by KAtt.from_dict. When attempting to reserialize these an encoder is needed for json.dumps to support them.
|
We should probably make sure this plays nicely with: #4345 |
tothtamas28
reviewed
May 15, 2024
tothtamas28
approved these changes
May 21, 2024
pyk/src/pyk/__main__.py
Outdated
Comment on lines
438
to
439
| _LOGGER.critical(e) | ||
| exit(1) |
There was a problem hiding this comment.
I think you can just let the exception propagate to the output instead.
There was a problem hiding this comment.
Sounds fine for now. There are a variety of user errors here that can cause an exception and I would eventually like to see these exceptions be collected and logged somehow for the user instead of having python die and show them a stack trace.
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.
Implements the command
pyk kompilexwhich uses pyk's outer parser to parse in a K Definition and then hands it off to the java frontend to handle the rest of the compilation.Some bootstrapping is required because the conversions from the outer parsed structures to something compatible with the java frontend aren't fully implemented. For the integration tests, a
prelude-modules.jsonfile is included in the test data folder which has the K prelude already outer parsed.This will only handle modules that are empty or import other modules. The goal is to expand this capability until the full K language is supported, and then the bootstrapping will no longer be necessary.