generate error credit from thin air + drop value restriction in wp_up… #618

	name: CI

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

	jobs:
	build:
	runs-on: ubuntu-latest
	strategy:
	matrix:
	image:
	- mathcomp/mathcomp:latest-coq-8.19
	max-parallel: 4
	# don't cancel all in-progress jobs if one matrix job fails:
	fail-fast: false

	steps:
	- uses: actions/checkout@v3
	- uses: coq-community/docker-coq-action@v1
	with:
	opam_file: 'clutch.opam'
	custom_image: ${{ matrix.image }}
	install : \|
	startGroup "Install dependencies"
	sudo apt-get update -y -q
	opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
	opam pin add -n -y -k path $PACKAGE $WORKDIR
	opam update -y
	opam reinstall --forget-pending --yes
	opam install --confirm-level=unsafe-yes -j 2 $PACKAGE --deps-only
	endGroup
	before_script: \|
	sudo chown -R coq:coq . # workaround a permission issue
	script: \|
	startGroup Build
	make -j2
	endGroup
	uninstall: \|
	make clean
	- name: Revert permissions
	# to avoid a warning at cleanup time
	if: ${{ always() }}
	run: sudo chown -R 1001:116 .

Provide feedback