renderOneLine should render to one line
Previously the implementation was using layoutCompat with the hope that this operation rendered to a single line. It doesn't. This function is only used in the obscure :dumptests command where rendering to a single line is important for the file format.
Previously, `splitV` would assume that if you were splitting a value `val` into
something of type `[inf][each]`, then `val` must be a stream of type of `[inf *
each]` (i.e., of type `[inf]`). This is not true in the corner case where
`each` equals `0`, however. In that case, `val` is of type `[0]`, which is a
word, not a stream. As such, we need to ensure that we do not call `fromSeq` on
`val`, which crashes if `val` is not a stream or sequence.
Fixes#1749.
* Update all commands to track their results
* Implement REPL :check-docstrings command
This command checks that all of the unlabeled and "repl" labeled
codeblocks in docstrings can successfully evaluate as REPL commands.
Cryptol will now indicate exit failure if any of REPL commands fail,
making it possible to use in automated testing.
:check-docstrings internal implementation is set up to track results
of subcommands in support for integration into a remote server API
endpoint.
* Implement :focus
* Add some :check-docstring test cases
* Update changelog
* Update CrashCourse.tex now that more commands are checked
* Require repl and convert \r\n to \n in lexer
Checking ill-typed constraint guards for exhaustivity can cause Cryptol to
panic. If we detect any type errors after type-checking the guards, we now
abort early and report any recorded errors instead of proceeding to check
exhaustivity.
Fixes#1593. Fixes#1693.
Numeric constraint guards have very particular syntactic requirements:
* They must always be used in top-level definitions.
* Their definitions must always be accompanied by a top-level type signature.
Previously, we checked these requirements in a combination of places in the
parser and the typechecker. The checks in the typechecker weren't very
thorough, however, and they failed to catch local definitions without type
signatures that use constraint guards, as seen in #1685.
This patch moves all of these syntactic checks to the parser (in
`Cryptol.Parser.ExpandPropGuards`). We now recurse into expressions to check
for local definition that use constraint guards and error if we encounter one.
This ensures that by the time we reach the typechecker, all constraint guard
expressions are at least syntactically valid.
Fixes#1685.
Previously, `parmap` could incorrectly return a `VWord` when the element type
was not `Bit`, and it could also return a `VSeq` when the element type was
`Bit`. This changes the implementation of `parmap` to use the `mkSeq` smart
constructor, which properly chooses what sort of `GenValue` to return depending
on the element type.
Fixes#1578.
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.
Previous, `fromTo` and related functions would always return a `VSeq`. If the
type happened to be a `Bit`, this would violate the internal invariant that
sequences of `Bit`s are always represented with `VWord`s, leading to the panics
observed in #1435. This patch fixes the issue by using the `mkSeq` smart
constructor, which chooses between `VWord` and `VSeq` depending on the sequence
type.
Fixes#1435.
In the case where the index is a symbolic `Integer` and the sequence is of
length `n`, the What4 backend mistakenly chose `n` to be the largest possible
index. This corrects it to instead be `n - 1`.
Fixes#1359.
