Doing so is completely unnecessary, as we never actually need to build any
Haskell code in these jobs (rather, we invoke pre-built executables instead).
Fixes#1668.
These functions now trigger `-Wx-partial` warnings with GHC 9.8 or later. Where
convenient, I rewrote some code to use `NonEmpty` lists, but for more involved
pieces of code, I simply made it clearer which parts rely on invariants about
lists being non-empty by marking the (hopefully) inaccessible cases with
`panic`s.
This patch:
* Tightens up imports in `Cryptol.Eval.FFI.GenHeader` to avoid importing two
different versions of `unzip` (note that GHC 9.8 defines `unzip` in
`Data.Functor`, which is different from the version defined in `Data.List`).
* Bumps the upper version bounds on various dependencies (`base`, `sbv`, etc.)
to support versions that are compatible with GHC 9.8.
Fixes#1624.
This ensures that the constraints and right-hand side expressions in each guard
are well formed. This check suffices to catch the bug in
https://github.com/GaloisInc/saw-script/issues/2043, which was fixed separately
in a previous commit.
I have also updated the `tests/constraint-guards/type-sig-constraint.icry` test
to use `coreLint=on` rather than checking `debug` output, as the former is more
resilient to internal changes in Cryptol's pretty-printer.
Fixes#1647.
Previously, `checkPropGuardCase` would not consider type signature constraints
when determining how many proof applications to generate, which ultimately led
to the issues observed in https://github.com/GaloisInc/saw-script/issues/2043.
This is relatively easy to fix by ensuring that we pass these constraints as an
additional argument to `checkPropGuardCase`.
It is difficult to fully validate that this fix works without SAW, but I have
checked in a smoke test that checks if the guards in a numeric constraint guard
definition have the expected number of proof applications.
- p-1 bits in an IEEE float refers to the significand, not the
mantissa, at least according to the latest preferred terminology,
which aims to keep the word "mantissa" for the full mantissa
including the units bit;
- reciprocal rather than reciprocol;
- the example in 1.23 had the wrong module declarations; also insert a
separator word between the verbatim blocks so they can be told
apart.
Haskell Language Server still struggles a bit with opening projects that
are subprojects of larger projects (in the git submodule sense).
When opening such projects from within their parent project, the overall
project path remains the outermost one, which breaks relative paths of
subprojects.
The file-embed has a utility to help with such path adjustments.
Theoretically, HLS will eventually support "multi-home units", where
different files will be compiled under different home folders if they
belong to subprojects, but in the meantime, this un-breaks HLS for users
that open Cryptol as a subproject of, say, SAW.