prover-test.yml

name: Test gnark prover
on:
  push:
    branches:
      - main
      - "release/**"
    paths:
      - "prover/server/**"
      - ".github/workflows/prover-test.yml"
      - ".github/workflows/prover-release.yml"
  pull_request:
    branches:
      - "*"
    paths:
      - "prover/server/**"
      - ".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: "./prover/server/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: prover/server/formal-verification/lake-packages
          key: "${{ env.LAKE_VERSION }}"

      - name: Download keys for lightweight tests
        if: ${{ github.event.pull_request.base.ref == 'main' }}
        run: |
          cd prover/server
          ./scripts/download_keys.sh light

      - name: Download keys for full tests
        if: ${{ github.event.pull_request.base.ref == 'release' }}
        run: |
          cd prover/server
          ./scripts/download_keys.sh full

      - name: Build
        run: |
          cd prover/server
          go build

      - name: Unit tests
        run: |
          cd prover/server
          go test ./prover -timeout 60m

      - name: Lightweight integration tests
        if: ${{ github.event.pull_request.base.ref == 'main' }}
        run: |
          cd prover/server
          go test -run TestLightweight -timeout 15m

      - name: Full integration tests
        if: ${{ github.event.pull_request.base.ref == 'release' }}
        run: |
          cd prover/server
          go test -run TestFull -timeout 120m

      # - name: Extract circuit to Lean
      #   run: |
      #     cd prover/server
      #     ./light-prover extract-circuit --output formal-verification/FormalVerification/Circuit.lean --tree-height=26 --compressed-accounts=8

      # - name: Build lean project
      #   run: |
      #     cd prover/server/formal-verification
      #     ~/.elan/bin/lake exe cache get
      #     ~/.elan/bin/lake build