Skip to content

Commit

Permalink
Merge pull request #61 from coq-community/meta-ci-doc
Browse files Browse the repository at this point in the history
Improving the README.md after merging PR #60
  • Loading branch information
erikmd authored Aug 11, 2021
2 parents 8b96bc0 + 93819a8 commit 43d5dcb
Show file tree
Hide file tree
Showing 3 changed files with 81 additions and 34 deletions.
54 changes: 42 additions & 12 deletions .github/workflows/coq-demo.yml
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,9 @@ jobs:
ocaml_version: ['4.07-flambda']
fail-fast: false # don't stop jobs if one fails
steps:
# BEGIN GHA_TEST_ENV
################################################################
# Begin GHA_TEST_ENV # You should remove this GHA_TEST_ENV block
# # if you copy this demo workflow elsewhere!
- uses: actions/checkout@v2
with:
repository: 'erikmd/docker-coq-github-action-demo'
Expand All @@ -34,7 +36,10 @@ jobs:
with:
path: 'docker-coq-action'
- uses: './docker-coq-action'
# END GHA_TEST_ENV
# End GHA_TEST_ENV
##################
# - uses: actions/checkout@v2
# - uses: coq-community/docker-coq-action@v1
with:
opam_file: 'coq-demo.opam'
coq_version: ${{ matrix.coq_version }}
Expand All @@ -51,7 +56,9 @@ jobs:
# 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
################################################################
# Begin GHA_TEST_ENV # You should remove this GHA_TEST_ENV block
# # if you copy this demo workflow elsewhere!
- uses: actions/checkout@v2
with:
repository: 'erikmd/docker-coq-github-action-demo'
Expand All @@ -60,7 +67,10 @@ jobs:
with:
path: 'docker-coq-action'
- uses: './docker-coq-action'
# END GHA_TEST_ENV
# End GHA_TEST_ENV
##################
# - uses: actions/checkout@v2
# - uses: coq-community/docker-coq-action@v1
with:
opam_file: 'coq-demo.opam'
custom_image: ${{ matrix.image }}
Expand All @@ -78,7 +88,9 @@ jobs:
- 'coqorg/coq:8.13'
fail-fast: false # don't stop jobs if one fails
steps:
# BEGIN GHA_TEST_ENV
################################################################
# Begin GHA_TEST_ENV # You should remove this GHA_TEST_ENV block
# # if you copy this demo workflow elsewhere!
- uses: actions/checkout@v2
with:
repository: 'erikmd/docker-coq-github-action-demo'
Expand All @@ -87,7 +99,10 @@ jobs:
with:
path: 'docker-coq-action'
- uses: './docker-coq-action'
# END GHA_TEST_ENV
# End GHA_TEST_ENV
##################
# - uses: actions/checkout@v2
# - 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.
Expand Down Expand Up @@ -129,7 +144,9 @@ jobs:
- 'coqorg/coq:8.13'
fail-fast: false # don't stop jobs if one fails
steps:
# BEGIN GHA_TEST_ENV
################################################################
# Begin GHA_TEST_ENV # You should remove this GHA_TEST_ENV block
# # if you copy this demo workflow elsewhere!
- uses: actions/checkout@v2
with:
repository: 'erikmd/docker-coq-github-action-demo'
Expand All @@ -138,7 +155,10 @@ jobs:
with:
path: 'docker-coq-action'
- uses: './docker-coq-action'
# END GHA_TEST_ENV
# End GHA_TEST_ENV
##################
# - uses: actions/checkout@v2
# - uses: coq-community/docker-coq-action@v1
with:
custom_image: ${{ matrix.image }}
custom_script: |
Expand Down Expand Up @@ -181,7 +201,9 @@ jobs:
- 'coqorg/coq:8.13'
fail-fast: false # don't stop jobs if one fails
steps:
# BEGIN GHA_TEST_ENV
################################################################
# Begin GHA_TEST_ENV # You should remove this GHA_TEST_ENV block
# # if you copy this demo workflow elsewhere!
- uses: actions/checkout@v2
with:
repository: 'erikmd/docker-coq-github-action-demo'
Expand All @@ -190,7 +212,10 @@ jobs:
with:
path: 'docker-coq-action'
- uses: './docker-coq-action'
# END GHA_TEST_ENV
# End GHA_TEST_ENV
##################
# - uses: actions/checkout@v2
# - uses: coq-community/docker-coq-action@v1
with:
opam_file: 'coq-demo.opam'
custom_image: ${{ matrix.image }}
Expand All @@ -214,7 +239,9 @@ jobs:
- 'coqorg/coq:8.13'
fail-fast: false # don't stop jobs if one fails
steps:
# BEGIN GHA_TEST_ENV
################################################################
# Begin GHA_TEST_ENV # You should remove this GHA_TEST_ENV block
# # if you copy this demo workflow elsewhere!
- uses: actions/checkout@v2
with:
repository: 'erikmd/docker-coq-github-action-demo'
Expand All @@ -223,7 +250,10 @@ jobs:
with:
path: 'docker-coq-action'
- uses: './docker-coq-action'
# END GHA_TEST_ENV
# End GHA_TEST_ENV
##################
# - uses: actions/checkout@v2
# - uses: coq-community/docker-coq-action@v1
with:
opam_file: 'coq-demo.opam'
custom_image: ${{ matrix.image }}
Expand Down
23 changes: 9 additions & 14 deletions .github/workflows/python-demo.yml
Original file line number Diff line number Diff line change
Expand Up @@ -17,31 +17,26 @@ jobs:
# https://github.com/coq-community/docker-coq-action#custom_script
# ######################################################################
python-demo:
name: docker-coq-action / python
name: custom_image / python:3
runs-on: ubuntu-latest
strategy:
matrix:
image:
- 'python:3'
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@v2
# This "with" clause must be removed if the GHA .yml file is committed
# in your own Python project repository:
with:
repository: 'erikmd/poc-github-ci'
ref: 'master'
# This step must be removed if the GHA .yml file is committed
# in your own Python project repository:
- uses: actions/checkout@v2
with:
path: 'docker-coq-action'
# This "uses" clause must be replaced, if the GHA .yml file is committed
# in your own Python project repository, with
# - uses: coq-community/docker-coq-action@v1
- uses: './docker-coq-action'
# End GHA_TEST_ENV
##################
# - uses: actions/checkout@v2
# - uses: coq-community/docker-coq-action@v1
with:
custom_image: ${{ matrix.image }}
custom_image: 'python:3'
custom_script: |
python --version
startGroup "Install dependencies"
Expand Down
38 changes: 30 additions & 8 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# Docker-Coq GitHub action
# Docker-Coq GitHub Action

![reviewdog][reviewdog-badge]
[![coqorg][coqorg-shield]][coqorg-link]
Expand All @@ -24,14 +24,14 @@
[conduct-shield]: https://img.shields.io/badge/%E2%9D%A4-code%20of%20conduct-%23f15a24.svg
[conduct-link]: https://github.com/coq-community/manifesto/blob/master/CODE_OF_CONDUCT.md

This is a GitHub action that uses (by default)
This is a GitHub Action that uses (by default)
[coqorg/coq](https://hub.docker.com/r/coqorg/coq/) Docker images,
which in turn is based on [coqorg/base](https://hub.docker.com/r/coqorg/base/),
a Docker image with a Debian environment.

| | GitHub repo | Type | Docker Hub |
|---|-------------------------------------------------------------------------|---------------|--------------------------------------------------------|
| x | [docker-coq-action](https://github.com/coq-community/docker-coq-action) | GitHub action | N/A |
| | [docker-coq-action](https://github.com/coq-community/docker-coq-action) | GitHub Action | N/A |
|| [docker-coq](https://github.com/coq-community/docker-coq) | Dockerfile | [`coqorg/coq`](https://hub.docker.com/r/coqorg/coq/) |
|| [docker-base](https://github.com/coq-community/docker-base) | Dockerfile | [`coqorg/base`](https://hub.docker.com/r/coqorg/base/) |
|| Debian | Linux distro | [`debian`](https://hub.docker.com/_/debian/) |
Expand All @@ -45,7 +45,7 @@ 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.
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](https://github.com/coq-community/templates#readme).
Expand All @@ -72,7 +72,7 @@ opam list
opam remove coq-proj
```

## Using the Github Action
## Using the GitHub Action

Using a [GitHub Action](https://docs.github.com/en/actions)
in your GitHub repository amounts to committing a file `.github/workflows/your-workflow-name.yml`,
Expand Down Expand Up @@ -101,9 +101,31 @@ for the documentation of those specific to the docker-coq-action,
or the GitHub Actions official documentation for the
[standard fields involved in workflows](https://docs.github.com/en/actions/reference/workflow-syntax-for-github-actions).
See [action.yml](./action.yml).
### References
See also the [example repo](https://github.com/erikmd/docker-coq-github-action-demo).
For details, see also:
* the [action.yml](./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](#inputs));
* the accompanying [`coq-demo` example repo](https://github.com/erikmd/docker-coq-github-action-demo);
* the two workflows [coq-demo.yml](./.github/workflows/coq-demo.yml) and [python-demo.yml](./.github/workflows/python-demo.yml) that both serve as `docker-coq-action`'s CI test-suite and provide some examples of use.

### Versioning

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](https://semver.org/).

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](https://docs.github.com/en/actions/learn-github-actions/finding-and-customizing-actions#using-release-management-for-your-custom-actions).

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*.

### Inputs

Expand Down Expand Up @@ -403,7 +425,7 @@ These bash functions are defined in [timegroup.sh](./timegroup.sh) and have the

If you use the
[`docker-coq`](https://github.com/coq-community/docker-coq) images,
the container user has UID=GID=1000 while the GitHub action workdir
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
Expand Down

0 comments on commit 43d5dcb

Please sign in to comment.