ci: add snekmate to external test suites (a16z#315)

saurabhchalke · Jun 25, 2024 · 367b891 · 367b891
1 parent 96aa5ec
commit 367b891
Showing 1 changed file with 34 additions and 9 deletions.
diff --git a/.github/workflows/test-external.yml b/.github/workflows/test-external.yml
@@ -24,22 +24,32 @@ jobs:
             dir: "morpho-data-structures"
             cmd: "halmos --function testProve --loop 4 --symbolic-storage"
             branch: ""
+            profile: ""
           - repo: "a16z/cicada"
             dir: "cicada"
             cmd: "halmos --contract LibUint1024Test --function testProve --loop 256"
             branch: ""
+            profile: ""
           - repo: "a16z/cicada"
             dir: "cicada"
             cmd: "halmos --contract LibPrimeTest --function testProve --loop 256"
             branch: ""
+            profile: ""
           - repo: "farcasterxyz/contracts"
             dir: "farcaster-contracts"
             cmd: "halmos"
             branch: ""
+            profile: ""
           - repo: "zobront/halmos-solady"
             dir: "halmos-solady"
             cmd: "halmos --function testCheck"
             branch: ""
+            profile: ""
+          - repo: "pcaversaccio/snekmate"
+            dir: "snekmate"
+            cmd: "halmos --config test/halmos.toml"
+            branch: ""
+            profile: "halmos"
 
     steps:
       - name: Checkout
@@ -57,17 +67,32 @@ jobs:
           ref: ${{ matrix.project.branch }}
           submodules: recursive
 
-      - name: Login to GitHub Container Registry
-        uses: docker/login-action@v3
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+
+      - name: Set up Python
+        uses: actions/setup-python@v5
         with:
-          registry: ghcr.io
-          username: ${{ github.actor }}
-          password: ${{ secrets.GITHUB_TOKEN }}
+          python-version: "3.12"
+
+      - name: Install dependencies
+        run: python -m pip install --upgrade pip
+
+      - name: Install Halmos
+        run: python -m pip install -e ./halmos
+
+      - name: Install Vyper
+        if: ${{ matrix.project.dir == 'snekmate' }}
+        run: python -m pip install vyper
 
-      - name: Build image
-        run: docker build -t halmos . --file packages/halmos/Dockerfile
-        working-directory: halmos
+      - name: Install Yices 2 SMT solver
+        run: |
+          sudo add-apt-repository ppa:sri-csl/formal-methods
+          sudo apt-get update
+          sudo apt-get install yices2
 
       - name: Test external repo
-        run: docker run -v .:/workspace ${{ matrix.project.cmd }} --statistics --solver-timeout-assertion 0 --solver-threads 4 --solver-command yices-smt2 ${{ matrix.cache-solver }} ${{ inputs.halmos-options }}
+        run: ${{ matrix.project.cmd }} --statistics --solver-timeout-assertion 0 --solver-threads 4 --solver-command yices-smt2 ${{ matrix.cache-solver }} ${{ inputs.halmos-options }}
         working-directory: ${{ matrix.project.dir }}
+        env:
+          FOUNDRY_PROFILE: ${{ matrix.project.profile }}