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.
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.
GitHub is deprecating (and eventually removing) its macOS 10.15 runners.
See actions/virtual-environments#5583. Let's upgrade to a newer version in the
CI. This proves relatively straightforward—the only other change required is to
upgrade to a newer version of `what4-solvers`.
This is done purely for the sake of increasing our coverage of Linux when
making releases. See #1140 for the motivation.
We won't run any of the tests et al. for this job.
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>
* Update CHANGES for 2.10
* Remove profiling flags from Cabal file
They result in `cabal check` warnings and probably don’t need to be
hard-coded.
* Remove commented-out Cryptol server references
The code no longer exists, so we’ll never uncomment these.
Equivalent functionality is now provided by `cryptol-remote-api`.
* Update references to version numbers in README. Closes#719.
* 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
Note: the hardcoding in this patch is only for the 2.2 hotfix branch; in
the 2.3 branch we will only have to change the default setting for the
typechecker.