Skip to content
Docker-Coq CI

Docker-Coq CI #650

Sign in to view logs

Docker-Coq CI

Docker-Coq CI #650

Workflow file for this run

.github/workflows/coq-demo.yml at ae62702
name: Docker-Coq CI
on:
push:
branches:
- master # forall push/merge in master
- v1 # forall push/merge in v1
pull_request:
branches:
- "**" # forall submitted Pull Requests
schedule:
# test master every day at 16:00 UTC
# cf. https://crontab.guru/
- cron: '0 16 * * *'
jobs:
# The following two jobs are standard/recommended versions, assuming
# your coq project repository contains a committed .opam file.
demo-1:
name: coq_version / docker-coq / opam
runs-on: ubuntu-latest
strategy:
matrix:
# To get the list of supported (coq, ocaml) versions from coqorg/coq,
# see https://github.com/coq-community/docker-coq/wiki#supported-tags
coq_version:
- '8.18'
- 'latest-native'
- 'dev'
ocaml_version: ['default']
fail-fast: false # don't stop jobs if one fails
steps:
################################################################
# Begin GHA_TEST_ENV # You should remove this GHA_TEST_ENV block
# # if you copy this demo workflow elsewhere!
- uses: actions/checkout@v4
with:
repository: 'erikmd/docker-coq-github-action-demo'
ref: 'master'
- uses: actions/checkout@v4
with:
path: 'docker-coq-action'
- uses: './docker-coq-action'
# End GHA_TEST_ENV
##################
# - uses: actions/checkout@v4
# - uses: coq-community/docker-coq-action@v1
with:
opam_file: 'coq-demo.opam'
coq_version: ${{ matrix.coq_version }}
ocaml_version: ${{ matrix.ocaml_version }}
demo-2:
name: custom_image / docker-mathcomp / opam
runs-on: ubuntu-latest
strategy:
matrix:
image:
- 'mathcomp/mathcomp-dev:coq-dev'
- 'mathcomp/mathcomp:latest-coq-8.19'
# - 'mathcomp/mathcomp:latest-coq-dev' # not always available,
# see https://hub.docker.com/r/mathcomp/mathcomp#supported-tags
fail-fast: false # don't stop jobs if one fails
steps:
################################################################
# Begin GHA_TEST_ENV # You should remove this GHA_TEST_ENV block
# # if you copy this demo workflow elsewhere!
- uses: actions/checkout@v4
with:
repository: 'erikmd/docker-coq-github-action-demo'
ref: 'master'
- uses: actions/checkout@v4
with:
path: 'docker-coq-action'
- uses: './docker-coq-action'
# End GHA_TEST_ENV
##################
# - uses: actions/checkout@v4
# - uses: coq-community/docker-coq-action@v1
with:
opam_file: 'coq-demo.opam'
custom_image: ${{ matrix.image }}
# The following job illustrates the use of several customizable fields,
# while keeping the default value of the overall "custom_script" field,
# see https://github.com/coq-community/docker-coq-action#custom_script
demo-3:
name: custom_image / docker-coq / make / script
runs-on: ubuntu-latest
strategy:
matrix:
image:
- 'coqorg/coq:latest'
- 'coqorg/coq:dev'
fail-fast: false # don't stop jobs if one fails
steps:
################################################################
# Begin GHA_TEST_ENV # You should remove this GHA_TEST_ENV block
# # if you copy this demo workflow elsewhere!
- uses: actions/checkout@v4
with:
repository: 'erikmd/docker-coq-github-action-demo'
ref: 'master'
- uses: actions/checkout@v4
with:
path: 'docker-coq-action'
- uses: './docker-coq-action'
# End GHA_TEST_ENV
##################
# - uses: actions/checkout@v4
# - uses: coq-community/docker-coq-action@v1
with:
# As the install/script/uninstall fields are overridden,
# the "opam_file" field is unneeded in this example job.
custom_image: ${{ matrix.image }}
install: |
startGroup "Install dependencies"
opam install -y -j 2 coq-mathcomp-ssreflect
endGroup
before_script: |
startGroup "Workaround permission issue"
sudo chown -R coq:coq .
endGroup
script: |
startGroup "Build project"
coq_makefile -f _CoqProject -o Makefile
make -j2
make test
make install
endGroup
uninstall: |
startGroup "Clean project"
make clean
make uninstall
endGroup
- name: Revert permissions
# to avoid a warning at cleanup time
if: ${{ always() }}
run: sudo chown -R 1001:116 .
# The following job illustrates the redefinition of the
# "custom_script" field.
demo-4:
name: custom_image / docker-coq / make / custom_script
runs-on: ubuntu-latest
strategy:
matrix:
image:
- 'coqorg/coq:latest'
- 'coqorg/coq:dev'
fail-fast: false # don't stop jobs if one fails
steps:
################################################################
# Begin GHA_TEST_ENV # You should remove this GHA_TEST_ENV block
# # if you copy this demo workflow elsewhere!
- uses: actions/checkout@v4
with:
repository: 'erikmd/docker-coq-github-action-demo'
ref: 'master'
- uses: actions/checkout@v4
with:
path: 'docker-coq-action'
- uses: './docker-coq-action'
# End GHA_TEST_ENV
##################
# - uses: actions/checkout@v4
# - uses: coq-community/docker-coq-action@v1
with:
custom_image: ${{ matrix.image }}
custom_script: |
startGroup "Print opam config"
opam config list; opam repo list; opam list
endGroup
startGroup "Install dependencies"
opam update -y
opam install -y -j 2 coq-mathcomp-ssreflect
endGroup
startGroup "List installed packages"
opam list
endGroup
startGroup "Workaround permission issue"
sudo chown -R coq:coq .
endGroup
startGroup "Build project"
coq_makefile -f _CoqProject -o Makefile
make -j2
make test
make install
endGroup
startGroup "Clean project"
make clean
make uninstall
endGroup
- name: Revert permissions
# to avoid a warning at cleanup time
if: ${{ always() }}
run: sudo chown -R 1001:116 .
# The following job illustrates how to pass environment variables.
demo-5:
name: custom_image / docker-coq / opam / env
runs-on: ubuntu-latest
strategy:
matrix:
image:
- 'coqorg/coq:latest'
fail-fast: false # don't stop jobs if one fails
steps:
################################################################
# Begin GHA_TEST_ENV # You should remove this GHA_TEST_ENV block
# # if you copy this demo workflow elsewhere!
- uses: actions/checkout@v4
with:
repository: 'erikmd/docker-coq-github-action-demo'
ref: 'master'
- uses: actions/checkout@v4
with:
path: 'docker-coq-action'
- uses: './docker-coq-action'
# End GHA_TEST_ENV
##################
# - uses: actions/checkout@v4
# - uses: coq-community/docker-coq-action@v1
with:
opam_file: 'coq-demo.opam'
custom_image: ${{ matrix.image }}
before_script: |
startGroup "Toy example"
echo "COQ_IMAGE=$COQ_IMAGE"
[ -n "$COQ_IMAGE" ]
echo "ex_var=$ex_var"
[ "$ex_var" = "ex_value" ]
endGroup
export: 'COQ_IMAGE ex_var OPAMWITHTEST' # space-sep. list of vars
env:
OPAMWITHTEST: 'true'
ex_var: 'ex_value'
# The following two jobs illustrate the installation of system packages.
demo-6:
name: custom_image / docker-coq / opam / auto install depexts
runs-on: ubuntu-latest
strategy:
matrix:
image:
- 'coqorg/coq:dev'
fail-fast: false # don't stop jobs if one fails
steps:
################################################################
# Begin GHA_TEST_ENV # You should remove this GHA_TEST_ENV block
# # if you copy this demo workflow elsewhere!
- uses: actions/checkout@v4
with:
repository: 'erikmd/docker-coq-github-action-demo'
ref: 'master'
- uses: actions/checkout@v4
with:
path: 'docker-coq-action'
- uses: './docker-coq-action'
# End GHA_TEST_ENV
##################
# - uses: actions/checkout@v4
# - uses: coq-community/docker-coq-action@v1
with:
opam_file: 'coq-depexts-test.opam'
custom_image: ${{ matrix.image }}
after_script: |
startGroup "Post-test"
gappa --version
endGroup
demo-7:
name: custom_image / docker-coq / opam / apt-get install more
runs-on: ubuntu-latest
strategy:
matrix:
image:
- 'coqorg/coq:latest'
- 'coqorg/coq:dev'
fail-fast: false # don't stop jobs if one fails
steps:
################################################################
# Begin GHA_TEST_ENV # You should remove this GHA_TEST_ENV block
# # if you copy this demo workflow elsewhere!
- uses: actions/checkout@v4
with:
repository: 'erikmd/docker-coq-github-action-demo'
ref: 'master'
- uses: actions/checkout@v4
with:
path: 'docker-coq-action'
- uses: './docker-coq-action'
# End GHA_TEST_ENV
##################
# - uses: actions/checkout@v4
# - uses: coq-community/docker-coq-action@v1
with:
opam_file: 'coq-demo.opam'
custom_image: ${{ matrix.image }}
before_script: |
startGroup "Install APT dependencies"
cat /etc/os-release
# sudo apt-get update -y -q # this mandatory command is already run in install step by default
sudo DEBIAN_FRONTEND=noninteractive apt-get install -y -q --no-install-recommends \
emacs \
tree # for instance
# Alphabetical order is recommended for long package lists to ease review and update
endGroup
after_script: |
startGroup "Post-test"
emacs --version
tree
endGroup
# The following job illustrates the upload of generated artifacts.
demo-8:
name: custom_image / docker-coq / opam+make / upload-artifacts
runs-on: ubuntu-latest
strategy:
matrix:
image:
- 'coqorg/coq:latest'
fail-fast: false # don't stop jobs if one fails
steps:
################################################################
# Begin GHA_TEST_ENV # You should remove this GHA_TEST_ENV block
# # if you copy this demo workflow elsewhere!
- uses: actions/checkout@v4
with:
repository: 'erikmd/docker-coq-github-action-demo'
ref: 'master'
- uses: actions/checkout@v4
with:
path: 'docker-coq-action'
- uses: './docker-coq-action'
# End GHA_TEST_ENV
##################
# - uses: actions/checkout@v4
# - uses: coq-community/docker-coq-action@v1
with:
opam_file: 'coq-demo.opam'
custom_image: ${{ matrix.image }}
before_script: |
startGroup "Workaround permission issue"
sudo chown -R coq:coq .
endGroup
script: |
startGroup "Build project"
coq_makefile -f _CoqProject -o Makefile
make -j2
endGroup
after_script: |
set -o pipefail # recommended if the script uses pipes
startGroup "Build artifacts"
mkdir -v -p artifacts
opam list > artifacts/opam_list.txt
make test 2>&1 | tee artifacts/make_test.txt
endGroup
uninstall: ''
- name: Revert permissions
# to avoid a warning at cleanup time
if: ${{ always() }}
run: sudo chown -R 1001:116 .
- uses: actions/upload-artifact@v4
with:
name: example-artifact
path: artifacts/
if-no-files-found: error # 'warn' or 'ignore' are also available, defaults to `warn`
retention-days: 8
# The following job illustrates the upload of github environment files.
demo-9:
name: custom_image / docker-mathcomp / opam / env+GITHUB_ENV
runs-on: ubuntu-latest
strategy:
matrix:
image:
- 'mathcomp/mathcomp:latest-coq-8.19'
fail-fast: false # don't stop jobs if one fails
steps:
################################################################
# Begin GHA_TEST_ENV # You should remove this GHA_TEST_ENV block
# # if you copy this demo workflow elsewhere!
- uses: actions/checkout@v4
with:
repository: 'erikmd/docker-coq-github-action-demo'
ref: 'master'
- uses: actions/checkout@v4
with:
path: 'docker-coq-action'
- uses: './docker-coq-action'
# End GHA_TEST_ENV
##################
# - uses: actions/checkout@v4
# - uses: coq-community/docker-coq-action@v1
id: docker-coq-action
env:
# Pass string data to docker-coq-action
after_ok: 'Test successful!'
with:
export: 'COQ_IMAGE after_ok'
custom_image: ${{ matrix.image }}
opam_file: 'coq-demo.opam'
before_script: |
# Pass step outputs (Docker image name) to next step
echo "docker_image=$COQ_IMAGE" >> "$GITHUB_OUTPUT"
after_script: |
# Pass env vars (Coq version string...) to next step
echo "coq_version=$(opam var coq:version)" >> "$GITHUB_ENV"
echo "some_variable=expected_value" >> "$GITHUB_ENV"
# Display Markdown summary
[ -n "$after_ok" ]
echo "### $after_ok :rocket:" >> "$GITHUB_STEP_SUMMARY"
- name: Next step
env:
docker_image: ${{ steps.docker-coq-action.outputs.docker_image }}
run: |
: Summary
echo "Previous step pulled Docker image: $docker_image"
[ -n "$docker_image" ]
echo "Previous step used: coq_version=$coq_version"
[ -n "$coq_version" ]
echo "some_variable=$some_variable"
[ "$some_variable" = "expected_value" ]