Merge PR #13665: Set Python's default output encoding to utf-8

Reviewed-by: Zimmi48
Ack-by: palmskog

5 files changed, 30 insertions, 21 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 749b74d584..bf3ac7a727 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -18,8 +18,9 @@ stages:
 # some default values
 variables:
   # Format: $IMAGE-V$DATE-$hash
-  # The $hash is the first 10 characters of the md5 of the dockerfile
-  CACHEKEY: "bionic_coq-V2020-11-26-50e9456f22"
+  # The $hash is the first 10 characters of the md5 of the Dockerfile. e.g.
+  # echo $(md5sum dev/ci/docker/bionic_coq/Dockerfile | head -c 10)
+  CACHEKEY: "bionic_coq-V2020-12-25-95a34df128"
   IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY"
   # By default, jobs run in the base switch; override to select another switch
   OPAM_SWITCH: "base"
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
diff --git a/doc/README.md b/doc/README.md
index 79d1e1b756..440b104c16 100644
--- a/doc/README.md
+++ b/doc/README.md
@@ -69,6 +69,16 @@ Or if you want to use less disk space:
     apt install texlive-latex-extra texlive-fonts-recommended texlive-xetex \
                 latexmk fonts-freefont-otf
 
+### Setting the locale for Python
+
+Make sure that the locale is configured on your platform so that Python encodes
+printed messages with utf-8 rather than generating runtime exceptions
+for non-ascii characters.  The `.UTF-8` in `export LANG=C.UTF-8` sets UTF-8 encoding.
+The `C` can be replaced with any supported language code.  You can set the default
+for a Docker build with `ENV LANG C.UTF-8`.  (Python may look at other
+environment variables to determine the locale; see the
+[Python documentation](https://docs.python.org/3/library/locale.html#locale.getdefaultlocale)).
+
 Compilation
 -----------
 
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 8f642df8fd..35243b5d7d 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -220,10 +220,7 @@ class CoqObject(ObjectDescription):
             # todo: then maybe the above "if" is not needed
             names_in_subdomain = self.subdomain_data()
             if name in names_in_subdomain:
-                try:
-                    print("Duplicate", self.subdomain, "name: ", name)
-                except UnicodeEncodeError: # in CI
-                    print("*** UnicodeEncodeError")
+                print("Duplicate", self.subdomain, "name: ", name)
             # self._warn_if_duplicate_name(names_in_subdomain, name, signode)
         return targetid