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.

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

feat: use docker image to load solvers and setup the testing environment #295

Merged
merged 10 commits into from
May 23, 2024

Conversation

EmperorOrokuSaki
Copy link
Contributor

This pull request uses the solvers package to load a docker container that has various solvers and dependencies of Halmos setup.

@karmacoma-eth karmacoma-eth self-requested a review May 22, 2024 21:38
@karmacoma-eth
Copy link
Collaborator

thanks @EmperorOrokuSaki, the functionality looks good and I can confirm it works in our CI here:
https://github.com/a16z/halmos/actions/runs/9198938639

since it works, I believe we can merge it as-is but if you're up for it it would be awesome to have a follow-up PR with:

  • if possible, two split images:

    • a solvers image that is just ubuntu + yices, z3, bitwuzla, cvc5, etc. (as many solvers as feasible). No python, foundry or halmos, just the smallest image that contains solvers.
    • a halmos image that uses solvers as a base image and has Python, foundry and the latest halmos
  • the Dockerfiles in-tree. Since we're going to rely on this in CI, we need to be able to easily update the image with updated dependencies

@karmacoma-eth karmacoma-eth enabled auto-merge (squash) May 23, 2024 00:50
@karmacoma-eth karmacoma-eth merged commit b5bef1f into a16z:main May 23, 2024
51 checks passed
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.

2 participants