Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Support building with GHC 9.6 #1987

Merged
merged 8 commits into from
Nov 20, 2023
Merged

Support building with GHC 9.6 #1987

merged 8 commits into from
Nov 20, 2023

Commits on Nov 20, 2023

  1. Whitespace only

    @RyanGlScott
    RyanGlScott committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    10abf84 View commit details
    Browse the repository at this point in the history

  2. Support building with sbv-10.* 

    `sbv-10.*` brings in two changes to the SBV internals that affects SAW:

1. `sbv-10.0` removes the `generateSMTBenchmark` function in favor of two
   separate `generateSMTBenchmarkSat` and `generateSMTBenchmarkProof` functions.
   We use the `generateSMTBenchmarkSat` variant in `SAWScript.Prover.Exporter`.
2. `sbv-10.0` changes the `Maybe [String]` argument to `svUninterpreted` (which
   we use in `saw-core-sbv`'s `Verifier.SAW.Simulator.SBV`) to a `UICodeKind`
   argument, where `UINone` is now what used to be denoted with `Nothing`.

We now use the appropriate CPP to make SAW compile before and after these
changes. See also GaloisInc/cryptol#1513, which was in similar territory.
    @RyanGlScott
    RyanGlScott committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    92264c6 View commit details
    Browse the repository at this point in the history

  3. Support building with GHC 9.6 

    Making SAW build with GHC 9.6 is almost entirely a matter of being more precise
with `mtl`-related imports to account for `mtl-2.3.1` not re-exporting as many
identifiers from `Control.Monad`, `Control.Monad.IO.Class`, etc.

I have also bumped the following submodules and `source-repository-package`s to
allow them to build with GHC 9.6:

* `cryptol`: GaloisInc/cryptol#1572
* `hobbits`: eddywestbrook/hobbits#9
    @RyanGlScott
    RyanGlScott committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    0fde5de View commit details
    Browse the repository at this point in the history

  4. heapster-saw: Don't use deprecated TypeInType extension 

    As of GHC 8.6, `TypeInType` is simply an alias for `DataKinds` + `PolyKinds`.
And as of GHC 9.6, `TypeInType` is deprecated. Since we are already using
`DataKinds` + `PolyKinds` in all of the places where we enable `TypeInType` in
`heapster-saw`, let's just remove our use of `TypeInType` to avoid deprecation
warnings.
    @RyanGlScott
    RyanGlScott committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    1ccaf49 View commit details
    Browse the repository at this point in the history

  5. heapster-saw: Avoid -Woverlapping-patterns warning caught by GHC 9.6 

    `parseNamedShapeFromRustDecl` will produce an `-Woverlapping-patterns` warning
with GHC 9.6 (but not in GHCi, see
https://gitlab.haskell.org/ghc/ghc/-/issues/23915), but we can refactor the
code slightly to avoid this issue.
    @RyanGlScott
    RyanGlScott committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    5b43e94 View commit details
    Browse the repository at this point in the history

  6. Use our own language-rust fork in submodule 

    Unfortunately, the upstream `language-rust` repo at
https://github.com/harpocrates/language-rust no longer appears to be actively
maintained, and without a fix for
harpocrates/language-rust#44, it is impossible to
build `language-rust` with GHC 9.6. This patch changes our `language-rust`
submodule to instead use our fork of `language-rust` (at
https://github.com/GaloisInc/language-rust). It is unclear if we will have to
keep doing this in the long term, but this at least unblocks us in the short
term.
    @RyanGlScott
    RyanGlScott committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    15c723a View commit details
    Browse the repository at this point in the history

  7. CI: Test GHC 9.6.3, drop 8.10.7

    @RyanGlScott
    RyanGlScott committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    8e16132 View commit details
    Browse the repository at this point in the history

  8. CI: Use latest GHC 9.2, 9.4 minor releases

    @RyanGlScott
    RyanGlScott committed Nov 20, 2023
    Configuration menu
    Copy the full SHA
    9802ac0 View commit details
    Browse the repository at this point in the history