feat: support wtns generation #157
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: Docker Image CI | |
| on: | |
| push: | |
| branches: [ "main" ] | |
| pull_request: | |
| branches: [ "main" ] | |
| workflow_dispatch: | |
| jobs: | |
| configuration-test: | |
| strategy: | |
| matrix: | |
| param: | |
| - --solver cvc5 ./benchmarks/circomlib-cff5ab6/[email protected] | |
| - --solver z3 ./benchmarks/circomlib-cff5ab6/[email protected] | |
| - --solver cvc5 --opt-level 0 ./benchmarks/circomlib-cff5ab6/[email protected] | |
| - --solver cvc5 --opt-level 2 --patch-circom ./benchmarks/circomlib-cff5ab6/[email protected] | |
| runs-on: ubuntu-latest | |
| container: | |
| image: veridise/picus:git-latest | |
| env: | |
| PLTADDONDIR: /root/.local/share/racket/ | |
| steps: | |
| - uses: actions/checkout@v1 | |
| - name: linking circom | |
| run: ln -s /root/.cargo/bin/circom /usr/bin/circom | |
| - name: compile circomlib | |
| run: bash ./scripts/prepare-circomlib.sh | |
| - name: run picus with param ${{ matrix.param }} | |
| run: | | |
| set +e | |
| racket ./picus.rkt ${{ matrix.param }} | tee result.out | |
| code=$? | |
| if [ $code -ne 0 ] && [ $code -ne 9 ]; then | |
| exit $code | |
| fi | |
| shell: bash # this ensures that pipefail is set | |
| - name: test expected result | |
| run: | | |
| grep "^The circuit is underconstrained$" ./result.out | |
| wtns-test: | |
| runs-on: ubuntu-latest | |
| container: | |
| image: veridise/picus:git-latest | |
| env: | |
| PLTADDONDIR: /root/.local/share/racket/ | |
| steps: | |
| - uses: actions/checkout@v1 | |
| - name: linking circom | |
| run: ln -s /root/.cargo/bin/circom /usr/bin/circom | |
| - name: run picus | |
| run: | | |
| set +e | |
| racket ./picus.rkt --wtns . ./benchmarks/circomlib-cff5ab6/[email protected] | |
| code=$? | |
| if [ $code -ne 0 ] && [ $code -ne 9 ]; then | |
| exit $code | |
| fi | |
| shell: bash # this ensures that pipefail is set | |
| - name: test expected result | |
| run: | | |
| diff first-witness.wtns tests/data/first-witness.wtns.expect | |
| diff second-witness.wtns tests/data/second-witness.wtns.expect | |
| # run the full test with cvc5 | |
| main-test: | |
| strategy: | |
| matrix: | |
| id: [0, 1, 2, 3] | |
| runs-on: ubuntu-latest | |
| container: | |
| image: veridise/picus:git-latest | |
| env: | |
| PLTADDONDIR: /root/.local/share/racket/ | |
| steps: | |
| - uses: actions/checkout@v1 | |
| - name: linking circom | |
| run: ln -s /root/.cargo/bin/circom /usr/bin/circom | |
| - name: run picus with cvc5, using v3 | |
| run: raco test ++args "--parallel ${{ matrix.id }} 4" ./tests/circomlib-test.rkt | |
| misc-test: | |
| runs-on: ubuntu-latest | |
| container: | |
| image: veridise/picus:git-latest | |
| env: | |
| PLTADDONDIR: /root/.local/share/racket/ | |
| steps: | |
| - uses: actions/checkout@v1 | |
| - name: run tests | |
| run: | | |
| raco test ./tests/performance-test.rkt | |
| raco test ./tests/framework-test.rkt | |
| publish-docker: | |
| needs: [wtns-test, configuration-test, main-test, misc-test] | |
| name: "Publish Docker image to DockerHub" | |
| if: github.event_name == 'push' | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Set up Docker Buildx | |
| uses: docker/setup-buildx-action@v2 | |
| - name: Login to DockerHub | |
| uses: docker/login-action@v2 | |
| with: | |
| username: ${{ secrets.DOCKERHUB_USERNAME }} | |
| password: ${{ secrets.DOCKERHUB_TOKEN }} | |
| - name: Build and push to DockerHub | |
| uses: docker/build-push-action@v3 | |
| with: | |
| push: true | |
| file: Dockerfile | |
| tags: veridise/picus:git-latest, veridise/picus:git-${{ github.sha }} |