Skip to content

Remove #[infer] attribute #1065

Remove #[infer] attribute

Remove #[infer] attribute #1065

Workflow file for this run

# This is a basic workflow to help you get started with Actions
name: docker CI
# Controls when the action will run. Triggers the workflow on push or pull request
# events but only for the master branch
on:
push:
branches: [ master ]
pull_request:
branches: [ master ]
jobs:
opam:
runs-on: ubuntu-latest
strategy:
fail-fast: false
matrix:
coq_version:
- '8.16'
- '8.17'
steps:
- uses: actions/checkout@v2
- uses: coq-community/docker-coq-action@v1
with:
opam_file: './coq-hierarchy-builder.opam'
coq_version: ${{ matrix.coq_version }}
export: 'OPAMWITHTEST' # space-separated list of variables
env:
OPAMWITHTEST: 'true'
plan-B:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v2
- uses: coq-community/docker-coq-action@v1
with:
opam_file: './coq-hierarchy-builder.opam'
coq_version: '8.16'
ocaml_version: '4.09-flambda'
script: |
mkdir /home/coq/workspace
cp -ra . /home/coq/workspace
cd /home/coq/workspace
opam install ./coq-hierarchy-builder.opam
sed -i.bak -e "s/-Q . HB//" -e "s|tests/factory_sort_tac.v||" _CoqProject.test-suite
# This is what a user does to cut HB loose
export COQ_ELPI_ATTRIBUTES="hb(log(raw))"
make test-suite -j2
wc -l `find . -name \*.v`
coq.hb patch `find . -name \*.v`
wc -l `find . -name \*.v`
if git diff --quiet; then echo "No patch!"; exit 1; fi
make clean
opam remove coq-hierarchy-builder
opam install ./coq-hierarchy-builder-shim.opam
# Does it work?
make test-suite -j2
# We also test the reset facility works (we rebuild hb locally)
make coq.hb
./coq.hb reset `find . -name \*.v`
mv _CoqProject.test-suite.bak _CoqProject.test-suite
git diff --exit-code