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.

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

Solver configuration in CI #699

Closed
robdockins opened this issue Apr 8, 2020 · 3 comments · Fixed by #761
Closed

Solver configuration in CI #699

robdockins opened this issue Apr 8, 2020 · 3 comments · Fixed by #761
Labels
test-framework For issues related to Cryptol's test framework.

Comments

@robdockins
Copy link
Contributor

Right now the cryptol test suite appears only to exercise symbolic solving via Z3. It would be nice to test other solvers in the test suite (e.g., CVC4, yices).

Currently the travis build for cryptol just curls a pretty old copy of Z3 from saw.galois.com, which seems suboptimal. I believe fryingpan builds can install other solvers, but I don't know how to set that up. @kquick, any thoughts on the best way to handle this?

@kquick
Copy link
Member

kquick commented Apr 8, 2020

Summarizing offline conv:

  1. Current need is CVC4, others are future needs.
  2. Not all solvers are valid for all tests. Solver is chosen from the .icry test file.
  3. Both Travis and fryingpan need to have the solvers available (preferred solution, and required for 2).

I added cvc4 package dependency for fryingpan builds; these should be supported now, and adding other solvers is an easy change.

For most solvers, a standard package is available, so the before_install: section in .travis.yml can be updated to add - sudo apt-get -y install cvc4.

@robdockins robdockins added the test-framework For issues related to Cryptol's test framework. label Apr 17, 2020
@brianhuffman
Copy link
Contributor

The (closed) PR #674 might be useful here.

I'm a bit worried about having our CI builds run commands like "install latest z3"; I would much prefer to have control over the precise version number. The version numbers of solvers that we officially support and test should be specified in the Cryptol README (#719), and it would be easiest to keep those in sync if we update the CI scripts and README at the same time.

@atomb
Copy link
Contributor

atomb commented May 6, 2020

It's probably worth mentioning the new GitHub Actions CI setup that @jared-w has been putting together. You can see the latest build output here:

https://github.com/GaloisInc/cryptol/actions/runs/96789882

This will be what we use to create releases from here on out. It specifies precisely what solver versions to install, and uses a single configuration for Linux, macOS, and Windows.

If we want to make super sure that the README is up to date, we could even just say "follow this link to see the versions of the solvers that we're currently testing with", or something like that.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
test-framework For issues related to Cryptol's test framework.
Projects
None yet
Development

Successfully merging a pull request may close this issue.

4 participants