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

Continuous integration tests are all failing #673

Closed
brianhuffman opened this issue Dec 14, 2019 · 2 comments · Fixed by #675
Closed

Continuous integration tests are all failing #673

brianhuffman opened this issue Dec 14, 2019 · 2 comments · Fixed by #675
Labels
test-framework For issues related to Cryptol's test framework.

Comments

@brianhuffman
Copy link
Contributor

The continuous integration tests on my recent pull requests (#672, #671, #669) are all failing because of the same reason: The regression test for issue #444 requires yices to be installed, but it apparently isn't available when running the tests.

> SBV error:
> Unable to locate executable for Yices
> Executable specified: "yices-smt2"

We should make sure that yices is available when running the continuous integration tests.
@brianhuffman brianhuffman added the test-framework For issues related to Cryptol's test framework. label Dec 14, 2019
@brianhuffman
Copy link
Contributor Author

It looks like the tests have been failing ever since 85bff67 when I added the regression test for #444. https://travis-ci.org/GaloisInc/cryptol/jobs/615069659

brianhuffman pushed a commit that referenced this issue Dec 16, 2019
Update CI configuration to download yices-smt2 binary (#673).
452385f
@brianhuffman
Copy link
Contributor Author

Pull request #674 seems to make the yices binary available like I wanted, but now there's another problem: It turns out that the expected error message in issue444.icry.stdout contains the absolute path to the solver binary, which is not the same from one machine to another.

We might still want to merge #674 so that we can have yices available for other regression tests. But because of the system-specific absolute path in the output, I think we'll have to remove the regression test for #444 from the test suite by reverting 85bff67.

brianhuffman pushed a commit that referenced this issue Dec 16, 2019
Revert "Add regression test for #444."
3281e7c 
This reverts commit 85bff67.

The error message in the expected output file `issue444.icry.stdout`
contained a system-specific absolute file path.

Fixes #673.
@brianhuffman brianhuffman mentioned this issue Dec 16, 2019
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
test-framework For issues related to Cryptol's test framework.
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Revert "Add regression test for #444." GaloisInc/cryptol
1 participant
@brianhuffman