switch from result_exs to exec_cache #492
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 --solver-command yices-smt2 --solver-threads 3" | |
| branch: "" | |
| profile: "" | |
| - repo: "morpho-org/morpho-blue" | |
| dir: "morpho-blue" | |
| cmd: "--solver-command yices-smt2 --solver-threads 3" | |
| branch: "" | |
| profile: "test" | |
| - repo: "a16z/cicada" | |
| dir: "cicada" | |
| cmd: "--contract LibUint1024Test --function testProve --loop 256 --solver-command yices-smt2 --solver-threads 3" | |
| branch: "" | |
| profile: "" | |
| - repo: "a16z/cicada" | |
| dir: "cicada" | |
| cmd: "--contract LibPrimeTest --function testProve --loop 256 --solver-command yices-smt2 --solver-threads 3" | |
| branch: "" | |
| profile: "" | |
| - repo: "farcasterxyz/contracts" | |
| dir: "farcaster-contracts" | |
| cmd: "--solver-command yices-smt2 --solver-threads 3" | |
| branch: "" | |
| profile: "" | |
| - repo: "zobront/halmos-solady" | |
| dir: "halmos-solady" | |
| cmd: "--function testCheck --solver-command yices-smt2 --solver-threads 3" | |
| branch: "" | |
| profile: "" | |
| - repo: "pcaversaccio/snekmate" | |
| dir: "snekmate" | |
| cmd: "--config test/halmos.toml --contract ERC20TestHalmos --solver-command 'jsi --model --sequence yices,bitwuzla-abstraction' --solver-threads 1" | |
| branch: "" | |
| profile: "halmos" | |
| - repo: "pcaversaccio/snekmate" | |
| dir: "snekmate" | |
| cmd: "--config test/halmos.toml --contract ERC721TestHalmos --solver-command 'jsi --model --sequence yices,bitwuzla-abstraction' --solver-threads 1" | |
| branch: "" | |
| profile: "halmos" | |
| - repo: "pcaversaccio/snekmate" | |
| dir: "snekmate" | |
| cmd: "--config test/halmos.toml --contract ERC1155TestHalmos --solver-command 'jsi --model --sequence yices,bitwuzla-abstraction' --solver-threads 1" | |
| branch: "" | |
| profile: "halmos" | |
| - repo: "pcaversaccio/snekmate" | |
| dir: "snekmate" | |
| cmd: "--config test/halmos.toml --contract MathTestHalmos --solver-command 'jsi --model --sequence yices,bitwuzla-abstraction' --solver-threads 1" | |
| 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 ${{ matrix.cache-solver }} ${{ inputs.halmos-options }} | |
| working-directory: ${{ matrix.project.dir }} | |
| env: | |
| FOUNDRY_PROFILE: ${{ matrix.project.profile }} |