Skip to content

Implement and verify the naive translation of lazy/force to thunks (#98) #384

Implement and verify the naive translation of lazy/force to thunks (#98)

Implement and verify the naive translation of lazy/force to thunks (#98) #384

Workflow file for this run

name: Test compilation
on:
push:
branches:
- master
- coq-8.17
pull_request:
branches:
- "**"
workflow_dispatch:
inputs: {}
jobs:
build-matrix:
runs-on: ubuntu-latest
strategy:
matrix:
opam_file:
- 'coq-certicoq.opam'
image:
- 'yforster/coq:8.19.1--clang-11--compcert-3.13.1--extlib-0.12.1--equations-1.3--metacoq-1.3.1'
fail-fast: false # don't stop jobs if one fails
steps:
- uses: actions/checkout@v3
with:
submodules: true
- uses: coq-community/docker-coq-action@v1
with:
custom_image: ${{ matrix.image }}
opam_file: ${{ matrix.opam_file }}
before_install: | # comment back in if MetaCoq commit changes
startGroup "fix permission issues"
sudo chown -R coq:coq .
endGroup
startGroup "opam pin"
opam pin -n -y submodules/metacoq
endGroup
before_script: |
startGroup "fix permission issues"
sudo chown -R coq:coq .
endGroup
startGroup "Copy repo (for later benchmarking)"
cp -r `pwd` ~/repo
endGroup
after_script: |
startGroup "List installed packages"
opam list
endGroup
startGroup "Run benchmarks"
make -C ~/repo/benchmarks all
endGroup
startGroup "Test bootstrapped plugins"
cd ~/repo && ./configure.sh global
make -C ~/repo/bootstrap test
endGroup