Adding new proof trace tests from Pi2 #4421
Merged
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
…ore tests and use it
Modifying `_kompiler.py` to add `KOMPILE_SYNTAX_MODULE` as Kompiler arg
Robertorosmaninho
requested review from
Baltoli,
theo25,
dwightguth and
tothtamas28
rv-jenkins
requested review from
ehildenb,
rv-jenkins and
F-WRunTime
as code owners
Robertorosmaninho
force-pushed
the
new-proof-trace-tests
branch
from
2d83c18 to
0df6073
Compare
tothtamas28
reviewed
Jun 5, 2024
… instead of `KOMPILE_SYNTAX_MODULE`
Baltoli
reviewed
Jun 5, 2024
Baltoli
approved these changes
Jun 5, 2024
tothtamas28
approved these changes
Jun 6, 2024
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.
This PR adds a set of new tests that previously lived in the Pi2 repository but no longer need to be there as the company now uses the LLVM Hints Parser instead of its own parser. Therefore, we decided to move the tests from the Pi2 repo to PyK so it can not only increase our test suit but also be as close as possible to the source code.
We decided to keep the whole Hints input instead of using PyK to build it, as we realized that not only were the traces generated using the corresponding PyK function different but also smaller than we expected, modifying the test behavior. One of the differences we spot is that
map_patternadds an unnecessary\left-associn hints production that modifies the final trace.To facilitate the review of this PR, each new test corresponds to a commit!