test.yml

on:
  push:
    branches:
      - 'main'
  pull_request:

name: Extract, build, run

jobs:
  build:
    name: Build
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4

      - uses: leanprover/lean-action@v1
        with:
          test: false
          use-mathlib-cache: true
          use-github-cache: false
          build-args: "-R -Kwerror"

      - name: install Python dependences
        run: pip install matplotlib numpy scipy

      - name: install Dafny
        run: wget https://github.com/dafny-lang/dafny/releases/download/v4.4.0/dafny-4.4.0-x64-ubuntu-20.04.zip ; unzip dafny-4.4.0-x64-ubuntu-20.04.zip

      - name: build FastExtract
        run: |
          lake build -R -Kwerror FastExtract

      - name: build Python version of SampCert
        run: dafny/dafny build --target:py Tests/SampCert.dfy Tests/Random.py Tests/testing-kolmogorov-discretegaussian.py Tests/testing-kolmogorov-discretelaplace.py -o Tests/SampCert.dfy

      - name: run Discrete Gaussian test
        run: python3 Tests/SampCert-py/testing-kolmogorov-discretegaussian.py

      - name: run Discrete Laplace test
        run: python3 Tests/SampCert-py/testing-kolmogorov-discretelaplace.py