diff options
| author | Jim Fehrle | 2020-12-23 16:38:31 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2020-12-26 15:47:48 -0800 |
| commit | 6e2b31ab0ec22c04f8987b4eb54d6ba7bbdee4c4 (patch) | |
| tree | 74e47a1864c4eab8d6c3d77e52e12975e32fee56 /dev/ci/docker/README.md | |
| parent | 687fff698db75d54ef0a8b156b85a4dc027edc62 (diff) | |
Set the locale in Docker so Python's default output encoding is utf-8
Diffstat (limited to 'dev/ci/docker/README.md')
| -rw-r--r-- | dev/ci/docker/README.md | 28 |
1 files changed, 13 insertions, 15 deletions
diff --git a/dev/ci/docker/README.md b/dev/ci/docker/README.md index 16c4ac37d9..ed51c8afd3 100644 --- a/dev/ci/docker/README.md +++ b/dev/ci/docker/README.md @@ -4,31 +4,29 @@ This directory provides Docker images to be used by Coq's CI. The images do support Docker autobuild on `hub.docker.com` and Gitlab's private registry. -The Gitlab CI will build a docker image unless the CI environment variable +The Gitlab CI will build a Docker image unless the CI environment variable `SKIP_DOCKER` is set to `true`. This image will be stored in the [Gitlab container registry](https://gitlab.com/coq/coq/container_registry) under the name given by the `CACHEKEY` variable from the [Gitlab CI configuration file](../../../.gitlab-ci.yml). -In Coq's default CI, `SKIP_DOCKER` is set so as to avoid running a lengthy redundant job. +`SKIP_DOCKER` is set to "true" in `https://gitlab.com/coq/coq` to avoid running +a lengthy redundant job. For efficiency, users should enable that setting +in forked repositories after the initial Docker build in the fork succeeds. -It can be used to regenerate a fresh Docker image on Gitlab through the following steps. -- Change the `CACHEKEY` variable to a fresh name in the CI configuration in a new commit. -- Push this commit to a Github PR. This will trigger a Gitlab CI run that will - immediately fail, as the Docker image is missing and the `SKIP_DOCKER` +The steps to generate a new Docker image are: +- Update the `CACHEKEY` variable in .gitlab-ci.yml with the date and md5. +- Submit the change in a PR. This triggers a Gitlab CI run that + immediately fails, as the Docker image is missing and the `SKIP_DOCKER` default value prevents rebuilding the image. -- Run a new pipeline on Gitlab with that PR branch, using the green "Run pipeline" - button on the [web interface](https://gitlab.com/coq/coq/pipelines), - with the `SKIP_DOCKER` environment variable set to `false`. This will run a `docker-boot` process, and - once completed, a new Docker image will be available in the container registry, - with the name set in `CACHEKEY`. +- Run a new pipeline on Gitlab with that PR branch (e.g. "pr-99999"), using the green + "Run pipeline" button on the [web interface](https://gitlab.com/coq/coq/pipelines), + with the `SKIP_DOCKER` environment variable set to `false`. This will run a + `docker-boot` process, and once completed, a new Docker image will be available in + the container registry, with the name set in `CACHEKEY`. - Any pipeline with the same `CACHEKEY` will now automatically reuse that image without rebuilding it from scratch. -For documentation purposes, we also require keeping in sync the `CACHEKEY` comment -from the first line of the [Dockerfile](bionic_coq/Dockerfile) in the same -commit. - In case you do not have the rights to run Gitlab CI pipelines, you should ask the ci-maintainers Github team to do it for you. |
