Unbounded noised maximum using the sparse vector technique #450

	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

Provide feedback