Allow erasure evaluation to be called through a new ERASEcast construct #420

	name: Test compilation

	on:
	push:
	branches:
	- "**"
	pull_request:
	branches:
	- "**"
	workflow_dispatch:
	inputs: {}

	jobs:
	build-matrix:
	runs-on: ubuntu-latest
	strategy:
	matrix:
	opam_file:
	- 'coq-verified-extraction.opam'
	image:
	- 'mattam82/metacoq:metacoq-1.3.2-coq-8.19'
	fail-fast: false # don't stop jobs if one fails
	steps:
	- uses: actions/checkout@v2
	with:
	submodules: true
	- uses: coq-community/docker-coq-action@v1
	with:
	custom_image: ${{ matrix.image }}
	opam_file: ${{ matrix.opam_file }}
	before_install: \|
	startGroup "fix permission issues"
	sudo chown -R coq:coq .
	endGroup
	# startGroup "opam pin"
	# opam pin -n -y "https://github.com/MetaRocq/metarocq.git#coq-8.19"
	# opam pin -n -y "https://github.com/stedolan/malfunction.git#master"
	# endGroup
	startGroup "install dependencies for benchmarks"
	opam install -y core_bench.v0.16.0
	endGroup
	install: \|
	startGroup "Install dependencies"
	# sudo apt-get update -y -q
	opam pin add -n -y -k path $PACKAGE $WORKDIR
	# opam update -y
	opam install --confirm-level=unsafe-yes -j 2 $PACKAGE --deps-only
	opam install malfunction
	endGroup
	script: \|
	startGroup "fix permission issues"
	sudo chown -R coq:coq .
	endGroup
	startGroup "Build"
	make
	endGroup
	startGroup "Install"
	make install
	endGroup
	after_script: \|
	startGroup "List installed packages"
	opam list
	endGroup
	startGroup "run tests"
	make -C examples
	make -C benchmarks ci
	endGroup

Provide feedback