Test external projects #453
Workflow file for this run
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: | |
| # TODO: remove this step once halmos-builder package is public | |
| - name: Login to GitHub Container Registry | |
| uses: docker/login-action@v3 | |
| with: | |
| registry: ghcr.io | |
| username: ${{ github.actor }} | |
| password: ${{ secrets.GITHUB_TOKEN }} | |
| - 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: Install Vyper | |
| if: ${{ matrix.project.dir == 'snekmate' }} | |
| run: | | |
| docker run --name halmos-vyper --entrypoint uv halmos-image pip install git+https://github.com/vyperlang/vyper@master | |
| docker commit --change 'ENTRYPOINT ["halmos"]' halmos-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 halmos version | |
| run: docker run halmos-image --version | |
| - name: Test external repo | |
| run: docker run -e FOUNDRY_PROFILE -v .:/workspace halmos-image ${{ 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 }} |