Separate functional specifications into own CI job #2504
Merged
Conversation
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
ehildenb
force-pushed
the
separate-functional
branch
from
b5957e6 to
f28413f
Compare
ehildenb
force-pushed
the
separate-functional
branch
from
932e867 to
f0a81de
Compare
nwatson22
approved these changes
Jun 28, 2024
rv-jenkins
pushed a commit
to runtimeverification/haskell-backend
that referenced
this pull request
Jul 1, 2024
runtimeverification/evm-semantics#2504 has renamed the `test-prove-pyk` Makefile target to `test-prove-rules`. This PR now runs this target when evaluating KEVM performance.
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.
We see a lot of flakiness on proofs due to resource exhaustion or timeouts and such. In particular, our funcitonal specifications flake frequently, because they have many claims in the same file and it only takes one claim flaking to cause the whole proof-suite to flake. This PR separates them into their own CI job for faster re-running.
test_pyk_proveis renamed to_test_proveand made to be callable in multiple contexts.test_prove_rulesandtest_prove_functionalare added, which segment the test-suite and call each separately.Makefile.ALL_TESTSis resolved.test_prove_dssto use new_test_proveas well.test_prove.pya bit.