Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add ecdsa-crucible.saw proof to CI #901

Closed
brianhuffman opened this issue Nov 14, 2020 · 1 comment · Fixed by #932 or #1070
Closed

Add ecdsa-crucible.saw proof to CI #901

brianhuffman opened this issue Nov 14, 2020 · 1 comment · Fixed by #932 or #1070
Labels
subsystem: crucible-jvm Issues related to Java verification with crucible-jvm

Comments

@brianhuffman
Copy link
Contributor

Once the crucible-jvm speed improvements have been merged to master, the time required to check ecdsa-crucible.saw will be reasonable enough to permit us to add it to the regression test suite for CI.
@brianhuffman brianhuffman added the subsystem: crucible-jvm Issues related to Java verification with crucible-jvm label Nov 14, 2020
brianhuffman pushed a commit that referenced this issue Nov 24, 2020
Add ecdsa-crucible.saw to the ecdsa integration test.
69bf933 
Fixes #901.
@brianhuffman brianhuffman mentioned this issue Nov 24, 2020
Merged
brianhuffman pushed a commit that referenced this issue Nov 25, 2020
Add ecdsa-crucible.saw to the ecdsa integration test.
d94084e 
Fixes #901.
@brianhuffman brianhuffman mentioned this issue Feb 10, 2021
Closed
@brianhuffman brianhuffman reopened this Feb 10, 2021
@brianhuffman
Copy link
Contributor Author

In PR #1048 ecdsa-crucible.saw was renamed to ecdsa.saw, but because of the following line in .github/ci.sh, PR #932 did not actually add the proof script to CI: the test was not actually being run in CI either before or after.

saw-script/.github/ci.sh

Line 171 in 9d812c9

for t in test0019_jss_switch_statement test_crucible_jvm test_ecdsa test_issue108 test_tutorial1 test_tutorial2 test_tutorial_w4; do echo $t >> disabled_tests.txt; done

brianhuffman pushed a commit that referenced this issue Feb 10, 2021
Re-enable all disabled integration tests in .github/ci.sh.
59a4b45 
If there is a specific reason for any integration test to be
excluded from CI, the rationale for exclusion should be given
in a comment inside `disabled_tests.txt`.

Fixes #901.
@brianhuffman brianhuffman mentioned this issue Feb 10, 2021
Merged
@mergify mergify bot closed this as completed in #1070 Feb 10, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
subsystem: crucible-jvm Issues related to Java verification with crucible-jvm
Projects
None yet
Milestone
No milestone
1 participant
@brianhuffman