This includes the following changes:
* The bindist URLs now include the OS architecture, I have tweaked the parts of
CI that downloads bindists accordingly.
* This snapshot includes `cvc5-1.0.5`, which has fixed a bug that was
responsible for #1548. As such, this fixes#1548.
The previous version (`snapshot-20220812`) was using CVC5 1.0.1, which is too
old to work properly with `what4`. I have bumped the version to
`snapshot-20221212`, which includes CVC5 1.0.2.
This patch:
* Makes the necessary changes on the `cryptol` and `cryptol-remote-api` side
needed add `cvc5`, `w4-cvc5`, and `sbv-cvc5` solvers. This requires SBV 9.1
or later to include the changes from LeventErkok/sbv#630, which re-exports
CVC5-related functionality from all of the places that Cryptol imports from.
* Adds a test case to ensure that basic CVC5 support works.
* Updates the CI and Dockerfile to ensure that CVC5 is included from the
`what4-solvers` bindists.
Fixes#1503.
This is motivated by a couple of reasons:
* GHC 8.8 on Windows suffers from a bug that can cause building certain code
to loop forever or even segfault. As far as I can tell, this bug doesn't
affect GHC 8.10 or later, so dropping 8.8 is a fairly reliable way to avoid
this problem.
* GHC 8.8 is outside of the three most recent stable GHC releases, so it
doesn't make as much sense to keep maintaining support for it.
GitHub Actions has deprecated its Ubuntu 18.04 runners, and they will be
removed by December 1, 2022. Moreover, GitHub Actions now offers Ubuntu 22.04
runners. It seems like a good time to upgrade our CI accordingly.
Somewhat annoyingly, the `haskell` Docker images that we use in our Dockerfiles
use such an old version of Debian that their version of `glibc` is incompatible
with any of the `what4-solvers` built for Ubuntu 20.04 or 22.04. As a result, I
switched them from the `haskell` Docker image to the `ubuntu` one. This
required some minor tweaks to how dependencies are installed, but nothing too
serious.
We will need a better solution to getting CVC4 eventually, but unbreaking the builds, even temporarily, is high priority. And the right solution for CVC4, with the recent transition to CVC5, is somewhat tricky.
Add support for TLS connections in both the rpc server
and client. Allow the client to disable certificate validation
via the `verify` keyword argument, i.e.,
`cryptol.connect(verify=False)`. The docker container
for `cryptol-remote-api` also contains a self-signed
cert for testing purposes.
Co-authored-by: Andrew Kent <andrew@galois.com>
* Use ghc 8.10.3 for cryptol-remote-api to test SGX compatibility
* Fix cvc4
* Fix test suite for cryptol-remote-api
* Default to putting the heap as low in address space as possible
Fixes CVC4 version used in Docker builds and GitHub actions. This is the update that we currently have to do every few weeks to point to a nightly build that still exists.
* Tiny tweaks to release notes
* Update GHC versions
* Update GHC versions for Actions
* Build releases with 8.8.4 (Something strange is going on with 8.10.2 on Windows)
* Fix Dockerfile
* Include version number in CHANGES.md
* Update copyright dates
* Don't include cryptol-specs in release archives
* Remove duplicate copy of Programming Cryptol
* Add additional SMT solvers to Docker image.
This change downloads specific stable release versions of each supported SMT solver to the Dockerfile. In cases where a build was available(yices, cvc4, Mathsat), it is downloaded directly. In other cases, it is build from a specific source snapshot (boolector, abc). These versions could be changes if desired.
This allows easy access to Cryptol and all solvers in a single Docker container, which is useful since some common problems are not amenable to solution with Z3 alone.
As with the original Cryptol Dockerfile, this implementation uses Docker's staged build functionality both to keep the final size as small as possible and to modularize the build. If desired, this segment could be copied verbatim to the SAW Dockerfile to add additional solvers there as well.
Note that this Dockerfile doesn't currently build. However, the new segment has been tested and does work. It may be desirable to update the rest of the Dockerfile before adding this change.
* Builds nightly binary tarballs on Linux, macOS, and Windows
* Runs tests on every PR and merge to master
* Includes GitHub Actions status in README instead of Travis
* Makes the GitRev recompile hack less fragile
* Makes the Makefile Cabal v3 compatible
* Builds the manual as part of the CI process
