VeyMont: codegen #1225
Merged
VeyMont: codegen #1225
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
…aving a name in Namer.scala
…ermission generation less noisy.
- Allow disabling veymont implementation generation. - Split up permission generation into a veymont flag and a non-veymont (pvl) flag. - Add permission generation to implementation generation - Start working on properly generating permissions for the generated channel fields.
…ges. Move the permission generation rewrite in the general rewrite package
…tialization. Refactor GenerateImplemenation to use VeymontContext.
…s not keep endpoint exprs with values
- Add clear success/failure messages to veymont mode logging - Change TTT case study spec to fix myMark error
- Make pvl-to-java compatibility transformation in the veymont pipeline depend on whether pvl or java is being generated - Fix small bug in NewArrayImpl where plain toString was used instead of Doc. This caused an unpretty name to be used, instead of the name indicated by ctx. - Factor out the pvl-generic part of veymont implementation generation and make it available under the --compile flag.
- Begin with working on a patching mechanism so executable and inspectable code can be generated from the generated implementation of VeyMont. - Experiment with compiling and running code at runtime in the veymont test suite. - Refactor the veymont stages system to it is more reusable in the test suite. - Refactor the VeyMont test suite to use custom testing routines.
- Add helpers to hre for working with directories and temp files. - Finish the Patch helpers in hre. The assumption is now that typically patches will be applied only once, and not exhaustively. - Actually run the generated code for the second veymont permissions case study, and compare the actual output with the expected output. - Make VercorsSpec file tracking available for subclasses through imperative helper functions.
- Add flags to focus on choreography verification, code generation, or implementation verification. - Adjust swap test to make sure VeyMont doesn't crash. - Refactor FM2023VeyMontSpec to use new testing harness.
…ement some more flags.
Finish up the VeyMont frontend so it can be properly integrated into the test suite. - Remove the --veymont-generate-permissions flag in favour of the regular --generate-permissions flag - Finish refactoring of VeyMont stages structure, refactoring support for timing messages and VeyMont flags. The VeyMont stages structure now properly reports errors.
…rewriting tests in new format.
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.
Checklist:
PR description
This PR implements code generation support, primarily for verifying the three new TTT case studies.