update solvers and halmos-builder dockerfiles (#404) #471
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Test external projects | |
| on: | |
| push: | |
| branches: [main, chore-workflows] | |
| workflow_dispatch: | |
| inputs: | |
| halmos-options: | |
| description: "additional halmos options" | |
| required: false | |
| type: string | |
| default: "" | |
| jobs: | |
| test: | |
| runs-on: ubuntu-latest | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| cache-solver: ["", "--cache-solver"] | |
| project: | |
| - repo: "morpho-org/morpho-data-structures" | |
| dir: "morpho-data-structures" | |
| cmd: "--function testProve --loop 4" | |
| branch: "" | |
| profile: "" | |
| - repo: "morpho-org/morpho-blue" | |
| dir: "morpho-blue" | |
| cmd: "" | |
| branch: "" | |
| profile: "test" | |
| - repo: "a16z/cicada" | |
| dir: "cicada" | |
| cmd: "--contract LibUint1024Test --function testProve --loop 256" | |
| branch: "" | |
| profile: "" | |
| - repo: "a16z/cicada" | |
| dir: "cicada" | |
| cmd: "--contract LibPrimeTest --function testProve --loop 256" | |
| branch: "" | |
| profile: "" | |
| - repo: "farcasterxyz/contracts" | |
| dir: "farcaster-contracts" | |
| cmd: "" | |
| branch: "" | |
| profile: "" | |
| - repo: "zobront/halmos-solady" | |
| dir: "halmos-solady" | |
| cmd: "--function testCheck" | |
| branch: "" | |
| profile: "" | |
| - repo: "pcaversaccio/snekmate" | |
| dir: "snekmate" | |
| cmd: "--config test/halmos.toml --contract ERC20TestHalmos" | |
| branch: "" | |
| profile: "halmos" | |
| - repo: "pcaversaccio/snekmate" | |
| dir: "snekmate" | |
| cmd: "--config test/halmos.toml --contract ERC721TestHalmos" | |
| branch: "" | |
| profile: "halmos" | |
| - repo: "pcaversaccio/snekmate" | |
| dir: "snekmate" | |
| cmd: "--config test/halmos.toml --contract ERC1155TestHalmos" | |
| branch: "" | |
| profile: "halmos" | |
| - repo: "pcaversaccio/snekmate" | |
| dir: "snekmate" | |
| cmd: "--config test/halmos.toml --contract MathTestHalmos" | |
| branch: "" | |
| profile: "halmos" | |
| steps: | |
| - name: Checkout halmos | |
| uses: actions/checkout@v4 | |
| with: | |
| # we won't be needing tests/lib for this workflow | |
| submodules: false | |
| - name: Build image | |
| run: docker build -t halmos-image . --file packages/halmos/Dockerfile | |
| - name: Run foundryup | |
| run: | | |
| # run foundryup in halmos-image, save the result as a new image | |
| docker run --name halmos-image-foundryup halmos-image foundryup | |
| # commit the result back to halmos-image | |
| docker commit halmos-image-foundryup halmos-image | |
| - name: Install Vyper | |
| if: ${{ matrix.project.dir == 'snekmate' }} | |
| run: | | |
| docker run --name halmos-image-vyper halmos-image uv pip install git+https://github.com/vyperlang/vyper@master | |
| docker commit halmos-image-vyper halmos-image | |
| - name: Checkout external repo | |
| uses: actions/checkout@v4 | |
| with: | |
| repository: ${{ matrix.project.repo }} | |
| path: ${{ matrix.project.dir }} | |
| ref: ${{ matrix.project.branch }} | |
| submodules: recursive | |
| - name: Print forge version | |
| run: docker run halmos-image forge --version | |
| - name: Print halmos version | |
| run: docker run halmos-image halmos --version | |
| - name: Test external repo | |
| run: docker run -e FOUNDRY_PROFILE -v .:/workspace halmos-image halmos ${{ matrix.project.cmd }} --statistics --solver-timeout-assertion 0 --solver-threads 3 --solver-command yices-smt2 ${{ matrix.cache-solver }} ${{ inputs.halmos-options }} | |
| working-directory: ${{ matrix.project.dir }} | |
| env: | |
| FOUNDRY_PROFILE: ${{ matrix.project.profile }} |