More printing of the halmos version #366
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] | |
| paths: | |
| - .github/workflows/test-external.yml | |
| 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 --symbolic-storage" | |
| branch: "" | |
| profile: "" | |
| - repo: "a16z/cicada" | |
| dir: "cicada" | |
| cmd: "--contract LibUint1024Test --function testProve --loop 256 --solver-command yices-smt2" | |
| branch: "" | |
| profile: "" | |
| - repo: "a16z/cicada" | |
| dir: "cicada" | |
| cmd: "--contract LibPrimeTest --function testProve --loop 256 --solver-command bitwuzla" | |
| branch: "" | |
| profile: "" | |
| - repo: "farcasterxyz/contracts" | |
| dir: "farcaster-contracts" | |
| cmd: "--solver-command yices-smt2" | |
| branch: "" | |
| profile: "" | |
| - repo: "zobront/halmos-solady" | |
| dir: "halmos-solady" | |
| cmd: "--function testCheck --solver-command yices-smt2" | |
| branch: "" | |
| profile: "" | |
| - repo: "pcaversaccio/snekmate" | |
| dir: "snekmate" | |
| cmd: "--config test/halmos.toml --solver-command yices-smt2" | |
| 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 vyper | |
| 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 -v .:/workspace halmos-image ${{ matrix.project.cmd }} --statistics --solver-timeout-assertion 0 --solver-threads 4 ${{ matrix.cache-solver }} ${{ inputs.halmos-options }} | |
| working-directory: ${{ matrix.project.dir }} | |
| env: | |
| FOUNDRY_PROFILE: ${{ matrix.project.profile }} |