Skip to content

fix: fallback to mac-compatible shasum command in download_keys.sh #1248

fix: fallback to mac-compatible shasum command in download_keys.sh

fix: fallback to mac-compatible shasum command in download_keys.sh #1248

Workflow file for this run

name: Test gnark prover
on:
push:
branches:
- main
- 'release/**'
paths:
- "light-prover/**"
- ".github/workflows/prover-test.yml"
- ".github/workflows/prover-release.yml"
pull_request:
branches:
- "*"
paths:
- "light-prover/**"
- ".github/workflows/prover-test.yml"
- ".github/workflows/prover-release.yml"
types:
- opened
- synchronize
- reopened
- ready_for_review
jobs:
build-and-test:
if: github.event.pull_request.draft == false
runs-on: buildjet-4vcpu-ubuntu-2204
timeout-minutes: 120
steps:
- name: Checkout sources
uses: actions/checkout@v4
- name: Set up Go
uses: actions/setup-go@v5
with:
go-version-file: "./light-prover/go.mod"
- name: Install Elan
run: |
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y -v --default-toolchain leanprover/lean4:v4.2.0
echo "LAKE_VERSION=$(~/.elan/bin/lake --version)" >> "$GITHUB_ENV"
- name: Cache dependencies
uses: actions/cache@v4
with:
path: light-prover/formal-verification/lake-packages
key: "${{ env.LAKE_VERSION }}"
- name: Download keys for lightweight tests
if: ${{ github.event.pull_request.base.ref == 'main' }}
run: |
cd light-prover
./scripts/download_keys.sh light
- name: Download keys for full tests
if: ${{ github.event.pull_request.base.ref == 'release' }}
run: |
cd light-prover
./scripts/download_keys.sh full
- name: Build
run: |
cd light-prover
go build
- name: Unit tests
run: |
cd light-prover
go test ./prover -timeout 60m
- name: Lightweight integration tests
if: ${{ github.event.pull_request.base.ref == 'main' }}
run: |
cd light-prover
go test -run TestLightweight -timeout 15m
- name: Full integration tests
if: ${{ github.event.pull_request.base.ref == 'release' }}
run: |
cd light-prover
go test -run TestFull -timeout 120m
# - name: Extract circuit to Lean
# run: |
# cd light-prover
# ./light-prover extract-circuit --output formal-verification/FormalVerification/Circuit.lean --tree-height=26 --compressed-accounts=8
# - name: Build lean project
# run: |
# cd light-prover/formal-verification
# ~/.elan/bin/lake exe cache get
# ~/.elan/bin/lake build