`sbv-10.0` brings in two changes to the SBV internals that affect Cryptol.
1. `sbv-10.0` removes the `generateSMTBenchmark` function in favor of two
separate `generateSMTBenchmarkSat` and `generateSMTBenchmarkProof` functions.
2. `sbv-10.0` removes the `allSatHasPrefixExistentials` field of `AllSatResult`.
We now use the appropriate CPP to make Cryptol compile before and after these
changes.
Fixes#1513.
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 contains a varity of changes needed to make the libraries in the `cryptol`
repo compile with GHC 9.4:
* GHC 9.4 is pickier about requiring the use of the `FlexibleContexts`
extension, that is now enabled in more places.
* I bumped the upper version bounds of various dependencies to allow them to
build with GHC 9.4.
Fixes#1487.
This patch:
* Adds the appropriate conditional logic to use the `Win32` library to
dynamically load shared libraries on Windows.
* Tweaks some FFI-related test cases to make them work portably on Windows. I
have left comments describing each of the non-obvious tweaks that I had to
make.
* Updates the reference manual accordingly.
Fixes#1394.
GHC 9.2 now includes `-Wincomplete-uni-patterns` as a part of `-Wall`. As a
result, building Cryptol with GHC 9.2 uncovers some previously undetected
warnings.
Some warnings can be fixed by rewriting the code slightly. For example,
changing a use of `Data.List.groupBy` to `Data.List.NonEmpty.groupBy` avoids
the need for an incomplete match on `(_ : _)` on the value that `groupBy`
returns. (Since `Data.List.NonEmpty` was added to `base` in `4.9`, this also
requires bumping the lower version bounds on `base` slightly.)
Other warnings were fixed by explicitly adding fall-through `error` cases.
The resulting code is no less partial than before, but it avoids warnings and
should provide a more specific error in the event that the fall-through cases
are reached.
Yet another class of warnings are those caused by the use of irrefutable
patterns, such as the definition of `ar1 ~[x] = x` in
`Cryptol.TypeCheck.TypePat`. It's rather unfortunate that
`-Wincomplete-uni-patterns` warns about these
(see https://gitlab.haskell.org/ghc/ghc/-/issues/14800), as the only way to
avoid the warning would be to rewrite these functions to use refutable
patterns, thereby changing their strictness properties. I've decided to simply
disable `-Wincomplete-uni-patterns` in each module that uses irrefutable
patterns to avoid this issue. I've written also written a Note explaining the
reasoning and referenced it in the affected modules.
This required a fair amount of fixup to the pretty-printing code,
as some of the primitives have semantics that differ in subtle ways
from the old package. The output now is mostly the same as before,
although some improvements have been made here and there.
The one somewhat negative outcome of this change is that the
"line fill" algorithm in `prettyprinter` works a bit different
and makes choices about where to break lines that are arguably
less desirable than before. When laying out structures nested inside
sequences, it is more likely to break a line inside a substructure,
whereas the old algorithm prefered to break lines between elements
of the outer sequence. There are also appear to be some minor
differences regarding how ribbon width is calculated.
