This is a GitHub Action that uses (by default) coqorg/coq Docker images, which in turn is based on coqorg/base, a Docker image with a Debian environment.
| GitHub repo | Type | Docker Hub | |
|---|---|---|---|
| ⊙ | docker-coq-action | GitHub Action | N/A |
| ↳ | docker-coq | Dockerfile | coqorg/coq |
| ↳ | docker-base | Dockerfile | coqorg/base |
| ↳ | Debian | Linux distro | debian |
For more details about these images, see the docker-coq wiki.
The docker-coq-action provides built-in support for opam builds.
coq is built on-top of ocaml and so coq projects use ocaml's
package manager (opam) to build themselves.
This GitHub Action supports opam out of the box.
If your project does not already have a coq-….opam file, you might
generate one such file by using the corresponding template gathered in
coq-community/templates.
This .opam file can then serve as a basis for submitting releases in
coq/opam-coq-archive, and
related guidelines (including the required .opam metadata) are
available in https://coq.inria.fr/opam-packaging.html.
More details can be found in the opam documentation.
Assuming the Git repository contains a folder/coq-proj.opam file,
it will run (by default) the following commands:
opam config list; opam repo list; opam list
sudo apt-get update -y -q
opam pin add -n -y -k path coq-proj folder
opam update -y
opam install --confirm-level=unsafe-yes -j 2 coq-proj --deps-only
opam list
opam install -y -v -j 2 coq-proj
opam list
opam remove -y coq-projThe apt-get command and the --confirm-level=unsafe-yes opam option
are necessary for automatic installation of system packages
that may be required by coq-proj.opam, as described in the
opam 2.1 release notes.
Using a GitHub Action
in your GitHub repository amounts to committing a file .github/workflows/your-workflow-name.yml,
e.g. .github/workflows/build.yml, containing (among others), a snippet such as:
runs-on: ubuntu-latest # container actions require GNU/Linux
strategy:
matrix:
coq_version:
- '8.16'
- dev
ocaml_version: ['default']
fail-fast: false # don't stop jobs if one fails
steps:
- uses: actions/checkout@v3
- uses: coq-community/docker-coq-action@v1
with:
opam_file: 'folder/coq-proj.opam'
coq_version: ${{ matrix.coq_version }}
ocaml_version: ${{ matrix.ocaml_version }}Each field can be customized, see below for the documentation of those specific to the docker-coq-action, or the GitHub Actions official documentation for the standard fields involved in workflows.
For details, see also:
- the action.yml file (containing the metadata processed by the GitHub Actions platform itself, as well as some comments, albeit more terse than the documentation below);
- the accompanying
coq-demoexample repo; - the two workflows coq-demo.yml and python-demo.yml that both serve as
docker-coq-action's CI test-suite and provide some examples of use.
The Git repo of docker-coq-action uses master as developing branch
and v1 as release branch; and the corresponding tags v1.x.y follow
semantic versioning.
We develop docker-coq-action with a special focus on backward
compatibility, so that if your workflow just uses
coq-community/docker-coq-action@v1, you will be able to benefit
from new features, while expecting no breaking change.
However, we recall that the version of any GitHub Action can just as well be referenced by a tag or a commit SHA.
Contrary to some custom practice of GitHub Actions maintainers, we do not change to which commit a tag points once it is published.
As a result, the latest stable version denoted by the short Git reference v1 is implemented as a release branch, not as a tag.
Anyway, if you do not trust the maintainers of a given GitHub Action, it is always safer to reference a commit SHA.
Optional
The path of the .opam file (or a directory), relative to the repo root.
Default: "." (if the argument is omitted or an empty string).
Note-1: relying on the value of this INPUT_OPAM_FILE variable, the
following two variables are exported when running the custom_script:
if [ -z "$INPUT_OPAM_FILE" ] || [ -d "$INPUT_OPAM_FILE" ]; then
WORKDIR=""
PACKAGE=${INPUT_OPAM_FILE:-.}
else
WORKDIR=$(dirname "$INPUT_OPAM_FILE")
PACKAGE=$(basename "$INPUT_OPAM_FILE" .opam)
fiNote-2: if this value is a directory (e.g., .), relying on the
custom_script default value, the action will
install all the *.opam packages stored in this directory.
Optional
The version of Coq. E.g., "8.10".
Default: "latest" (= latest stable version).
Append the -native suffix if the version is >= 8.13 (or dev)
and you are interested in the image that contains the
coq-native package.
E.g., "8.13-native", "latest-native", "dev-native".
If the coq_version value contains the -native suffix,
the ocaml_version value is ignored (as coq-native images only come with a single OCaml version).
Still, a warning is raised if ocaml_version is nonempty and different from "default".
Optional
The version of OCaml.
Default: "default" (= Docker-Coq's default OCaml version for the given Coq version).
Among "default", "4.02", "4.05", "4.07-flambda", "4.08-flambda", "4.09-flambda", "4.10-flambda", "4.11-flambda", "4.12-flambda", "4.13-flambda", "4.14-flambda"…
Warning! not all OCaml versions are available with all Coq versions.
The supported compilers w.r.t. each version of Coq are documented in the
OCaml-versions policy section of the docker-coq wiki.
Optional
The bash snippet to run before install
Default:
startGroup "Print opam config"
opam config list; opam repo list; opam list
endGroupSee custom_script and startGroup/endGroup for more details.
Optional
The bash snippet to install the opam PACKAGE dependencies.
Default:
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
endGroupwhere $PACKAGE and $WORKDIR are set from the opam_file variable.
See custom_script and startGroup/endGroup for more details.
Optional
The bash snippet to run after install (if successful).
Default:
startGroup "List installed packages"
opam list
endGroupSee custom_script and startGroup/endGroup for more details.
Optional
The bash snippet to run before script.
Default: "" (empty string).
See custom_script and startGroup/endGroup for more details.
Optional
The bash snippet to install the opam PACKAGE.
Default:
startGroup "Build"
opam install -y -v -j 2 $PACKAGE
opam list
endGroupwhere $PACKAGE is set from the opam_file variable.
See custom_script and startGroup/endGroup for more details.
Optional
The bash snippet to run after script (if successful).
Default: "" (empty string).
See custom_script and startGroup/endGroup for more details.
Optional
The bash snippet to uninstall the opam PACKAGE.
Default:
startGroup "Uninstallation test"
opam remove -y $PACKAGE
endGroupwhere $PACKAGE is set from the opam_file variable.
See custom_script and startGroup/endGroup for more details.
Optional
The main script run in the container; may be overridden; but overriding more specific parts of the script is preferred.
Default:
{{before_install}}
{{install}}
{{after_install}}
{{before_script}}
{{script}}
{{after_script}}
{{uninstall}}
Note-1: the semantics of this variable is a standard Bash script,
that is evaluated within the workflow container after replacing the
"mustache" placeholders with the value of their variable counterpart.
For example, {{uninstall}} will be replaced with the value of the
uninstall variable (the default value of which being
the string opam remove -y $PACKAGE).
Note-2: this option is named custom_script rather than run or so
to discourage changing its recommended, default value for building
a regular opam project, while keeping the flexibility to be able to
change it.
Note-3: if you decide to override the custom_script value anyway,
you can just as well rely on the "mustache interpolation" of
{{before_install}} … {{uninstall}}, and customize the underlying
values.
Optional
The name of the Docker image to pull.
Default: unset
If this variable is unset, its value is computed from the values of
keywords coq_version and ocaml_version.
If you use the standard
docker-coq images, we
recommend to directly use keywords coq_version and ocaml_version.
If you use another registry such as that of
docker-mathcomp
images, you can benefit from that keyword by writing a configuration
such as:
runs-on: ubuntu-latest
strategy:
matrix:
image:
- mathcomp/mathcomp:1.10.0-coq-8.10
- mathcomp/mathcomp:1.10.0-coq-8.11
- mathcomp/mathcomp:1.11.0-coq-dev
- mathcomp/mathcomp-dev:coq-dev
fail-fast: false # don't stop jobs if one fails
steps:
- uses: actions/checkout@v3
- uses: coq-community/docker-coq-action@v1
with:
opam_file: 'folder/coq-proj.opam'
custom_image: ${{ matrix.image }}If ever you want to retrieve the Docker image name within the CI script, you can
use the export keyword to expose the COQ_IMAGE internal variable.
Optional
A space-separated list of env variables to export to the custom_script.
Default: "", i.e., no additional variable is exported.
Note-1: The values of the variables to export may be defined by using the
env
keyword.
Note-2: Regarding the naming of these variables:
- Only use ASCII letters,
_and digits, i.e., matching the[a-zA-Z_][a-zA-Z0-9_]*regexp. - Avoid reserved identifiers (namely:
HOME,CI, and strings starting withGITHUB_,ACTIONS_,RUNNER_, orINPUT_). - The
docker-coq-actioninternally sets aCOQ_IMAGEenvironment variable that contains the full name of the Docker image used. Useexport: 'COQ_IMAGE'to make this variable available within the script.
Here is a minimal working example of this feature:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v3
- uses: coq-community/docker-coq-action@v1
with:
opam_file: 'folder/coq-proj.opam'
coq_version: 'dev'
ocaml_version: 'default'
export: 'OPAMWITHTEST' # space-separated list of variables
env:
OPAMWITHTEST: 'true'Here, setting the OPAMWITHTEST
environment variable is useful to run the unit tests
(specified using opam's with-test
clause) after the package build.
The default value of fields {{before_install}}, {{install}},
{{after_install}}, {{script}}, and {{uninstall}} involves the bash
functions startGroup (taking 1 argument: startGroup "Group title")
and endGroup.
These bash functions are defined in timegroup.sh and have the following features:
- they create foldable groups in the GitHub Actions logs (see the online doc),
- and they compute the elapsed time for the considered group;
- these groups cannot be nested,
- and if an
endGrouphas been forgotten, it is implicitly and automatically inserted at the nextstartGroup(albeit it is better to make eachendGroupexplicit, for readability).
Here is an example of script along with the output log so obtained:
ex_var="ex_value"
# […]
startGroup "Toy example"
echo "ex_var=$ex_var"
endGroup-
Folded version:
-
Unfolded version:
Beware that the following script is buggy:
script: |
startGroup "Build project"
make -j2 && make test && make install
endGroupBecause if make test fails, it won't make the CI fail.
(Explanation)
This is a typical pitfall that occur in any shell-based CI platform
where the set -e
option is implied: the early-exit associated to this option is
disabled if the failing command is followed by && or ||.
See e.g., the output of the following three commands:
bash -c 'set -e; false && true; echo $?; echo this should not be run'
# → 1
# → this should not be run
bash -c 'set -e; false; true; echo $?; echo this should not be run'
# (no output)
bash -c 'set -e; ( false && true ); echo $?; echo this should not be run'
# (no output)Instead, you should write one of the following variants:
-
using semicolons:
script: | startGroup "Build project" make -j2 ; make test ; make install endGroup
-
using newlines:
script: | startGroup "Build project" make -j2 make test make install endGroup
-
using
&&but within a subshell:script: | startGroup "Build project" ( make -j2 && make test && make install ) endGroup
If you use the
docker-coq images,
the container user has UID=GID=1000 while the GitHub Actions workdir
has (UID=1001, GID=116).
This is not an issue when relying on opam to build the Coq project.
Otherwise, you may want to use sudo in the container to change the
permissions. You may also install additional Debian packages
(see the dedicated section below).
Typically, this would lead to a workflow specification like this:
runs-on: ubuntu-latest
strategy:
matrix:
image:
- 'coqorg/coq:dev'
fail-fast: false # don't stop jobs if one fails
steps:
- uses: actions/checkout@v3
- uses: coq-community/docker-coq-action@v1
with:
opam_file: 'folder/coq-proj.opam'
custom_image: ${{ matrix.image }}
before_script: |
startGroup "Workaround permission issue"
sudo chown -R coq:coq . # <--
endGroup
script: |
startGroup "Build project"
make -j2
endGroup
uninstall: |
startGroup "Clean project"
make clean
endGroup
- name: Revert permissions
# to avoid a warning at cleanup time
if: ${{ always() }}
run: sudo chown -R 1001:116 . # <--For more details, see the
CI setup / Remarks
section in the docker-coq wiki.
The docker-coq-action and its "child" Docker image (specified by the
custom_image field) run inside a container, which
implies the associated filesystem is isolated from the runner.
However, the GitHub workspace directory is made available in the container (using a so-called bind-mount) and set as the current working directory.
As a result:
- all the files installed outside of this GitHub workspace directory
(such as
opampackages installed in/home/coq/.opam) are "lost" whendocker-coq-actionterminates; - all the files put in the GitHub workspace directory (or in a
sub-directory) are kept;
so it is possible to create artifacts, then use an action such asactions/upload-artifact@v2in a subsequent step.
Here is an example job for this use case, which also takes into account the previously-mentioned permissions workaround:
runs-on: ubuntu-latest
strategy:
matrix:
image:
- 'coqorg/coq:dev'
fail-fast: false # don't stop jobs if one fails
steps:
- uses: coq-community/docker-coq-action@v1
with:
opam_file: 'folder/coq-proj.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@v2
with:
name: example-artifact
path: artifacts/
if-no-files-found: error # 'warn' or 'ignore' are also available, defaults to `warn`
retention-days: 8Recall that docker-coq-action runs your CI script in a Docker container,
the filesystem of which being isolated from the GitHub runner.
Still, docker-coq-action bind-mounts some special paths for
GitHub Actions environment files,
so that "$GITHUB_ENV", "$GITHUB_OUTPUT", and "$GITHUB_STEP_SUMMARY" can be used
in (parts of) the custom_script in order to pass environment
variables or step outputs to the following steps, or set a Markdown summary.
Conversely, the export keyword can be used to pass variables
from the previous step to docker-coq-action.
Here is an example of script that uses GITHUB_ENV and GITHUB_OUTPUT:
runs-on: ubuntu-latest
strategy:
matrix:
image:
- 'coqorg/coq:latest'
fail-fast: false # don't stop jobs if one fails
steps:
- uses: actions/checkout@v3
- uses: coq-community/docker-coq-action@v1
id: docker-coq-action # needed to get step outputs
with:
opam_file: 'folder/coq-proj.opam'
custom_image: ${{ matrix.image }}
after_script: |
# Pass values to upcoming steps in two different ways
echo "coq_version_var=$(opam var coq:version)" >> "$GITHUB_ENV"
echo "coq_version_out=$(opam var coq:version)" >> "$GITHUB_OUTPUT"
- name: Next step
env:
coq_version_var2: ${{ steps.docker-coq-action.outputs.coq_version_out }}
run: |
: Summary
echo "Previous step used: coq_version=$coq_version_var"
echo "Previous step used: coq_version=$coq_version_var2 (same)"If you use docker-coq-action with a
Docker-Coq image (the
default when the custom_image field is omitted),
the image is based on Debian stable and the container user
(UID=GID=1000) has sudo rights, so you can rely on apt-get to
install additional Debian packages.
This use case is illustrated by the following job that installs
the emacs and tree packages:
runs-on: ubuntu-latest
strategy:
matrix:
image:
- 'coqorg/coq:dev'
fail-fast: false # don't stop jobs if one fails
steps:
- uses: actions/checkout@v3
- uses: coq-community/docker-coq-action@v1
with:
opam_file: 'folder/coq-proj.opam'
custom_image: ${{ matrix.image }}
before_script: |
startGroup "Install APT dependencies"
cat /etc/os-release # Print the Debian OS version
# 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
endGroupThe code run in the docker-coq-action container relies on the
following invocation to display a customized prompt before each
command:
export PS4='+ \e[33;1m($0 @ line $LINENO) \$\e[0m '; set -exAs a result, due to the set -x option, the value of each variable is
exposed in the log.
For example, the script:
startGroup "Risky example"
TOKEN=$(uuidgen -r)
curl -fsS -X POST -F token="$TOKEN" https://example.com >/dev/null
endGroupwill produce a log such as:
Hence the following two remarks:
-
If need be, it is possible to temporarily disable the trace feature in your script, surrounding the lines at stake by (
set +x,set -x).
Your script would thus look like:set +x #...some code with no trace... set -x
or, to get some even less verbose output:
{ set +x; } 2>/dev/null #...some code with no trace... set -x -
Fortunately, this trace feature cannot make repository secrets
${{ secrets.STH }}leak, as GitHub Actions automatically redact them in the log.
Regarding secrets obtained by other means, e.g. from a command-line program, it is recommended to perform the three actions below in a previousrun:step:-
store the "locally-created secret" in an environment variable:
SOME_TOKEN="..." -
immediately mark the variable as masked:
echo "::add-mask::$SOME_TOKEN"
-
register the variable to make it available for subsequent steps:
printf "%s\n" "SOME_TOKEN=$(printf "%q" "$SOME_TOKEN")" >> $GITHUB_ENV
A comprehensive example of this approach is available in PR erikmd/docker-coq-github-action-demo#12.
For completeness, note that masking inputs involved in
workflow_dispatchmay require somejq-based workaround, as mentioned in issue actions/runner#643. -
React
Typescript
Django
Laravel
Facebook
Microsoft
Google
Alibaba
D3
Tencent