Skip to content

GHC 9.6 v4 try, with CVC5 this time around.#507

Closed
msooseth wants to merge 35 commits intomainfrom
ghc-9.6-v4
Closed

GHC 9.6 v4 try, with CVC5 this time around.#507
msooseth wants to merge 35 commits intomainfrom
ghc-9.6-v4

Conversation

@msooseth
Copy link
Collaborator

Description

Test with CVC5 as default for

Checklist

  • tested locally
  • added automated tests
  • updated the docs
  • updated the changelog

arcz and others added 30 commits April 22, 2024 17:57
On arm Mac, the GHC is trying to locate libc++, but during that it also
searches for c++ (without the lib prefix), which is an alias for a clang
executable. It tries to load an executable as a static library which
results in an error.

I have no idea why these changes work, but they seem to work.
Foundry does not depend on DS tests anymore, they provide their own
cheatcodes directly in their VM now, so that the `lib` directory no
longer exists.
This shell only sets up the test dependencies, but keeps the Haskell
environment setup from the system.
This is a temporary workaround until the nix/ghc issue on MacOS is fixed
upstream.
@gustavo-grieco
Copy link
Collaborator

Is CVC5 support coming? I think I tested some time ago and it was broken 🤔

@msooseth
Copy link
Collaborator Author

msooseth commented Jul 19, 2024

Yeah, unfortunately you are right. We get: Array theory solver does not yet support write-chains connecting two different constant arrays for a single test. I disabled that test for the moment. Just to try.

Test was: keccak concrete and sym injectivity

@d-xo
Copy link
Collaborator

d-xo commented Jul 24, 2024

Awesome to see a green 9.6 finally. I don't love that we have no test coverage for z3 and bitwuzla in ci like this now though.

@d-xo
Copy link
Collaborator

d-xo commented Jul 25, 2024

closing since #499 is merged

@d-xo d-xo closed this Jul 25, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

5 participants