aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-12-28 16:47:16 +0000
committerGitHub2020-12-28 16:47:16 +0000
commit942fb01934b02181fd3a88d80fc870f8d4900d2c (patch)
tree249a05c091ff076492e63739bc05038efe244b9a /dev
parentba0a277568182c205ad411986598632bb341f2d9 (diff)
parent6e2b31ab0ec22c04f8987b4eb54d6ba7bbdee4c4 (diff)
Merge PR #13665: Set Python's default output encoding to utf-8
Reviewed-by: Zimmi48 Ack-by: palmskog
Diffstat (limited to 'dev')
-rw-r--r--dev/ci/docker/README.md28
-rw-r--r--dev/ci/docker/bionic_coq/Dockerfile3
2 files changed, 16 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.
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 1aefebb007..b4b6411d28 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -71,3 +71,6 @@ RUN opam switch create "${COMPILER_EDGE}+flambda" && eval $(opam env) && \
opam install $BASE_OPAM $BASE_OPAM_EDGE $COQIDE_OPAM $CI_OPAM
RUN opam clean -a -c
+
+# set the locale for the benefit of Python
+ENV LANG C.UTF-8