[ci] Remove CircleCI setup.

GitLab setup is quite stable these days thanks to the work of many
people and `coqbot`. We decided to keep CircleCI support for a while
as a safeguard in case something happened in the migration to GitLab,
but these days we are just wasting resources to them and to us. As I'm
afraid CircleCI won't scale for us, the time to remove it has arrived.

Still, CircleCI had some awesome functionality that GitLab's CI
doesn't offer yet, see the links at:

https://github.com/coq/coq/issues/6919#issuecomment-395885573

- https://gitlab.com/gitlab-org/gitlab-ce/issues/29347
- https://gitlab.com/gitlab-org/gitlab-ce/issues/35222
- https://gitlab.com/gitlab-org/gitlab-ce/issues/41947
- https://gitlab.com/gitlab-org/gitlab-ce/issues/47063

2 files changed, 1 insertions, 9 deletions

diff --git a/dev/ci/README.md b/dev/ci/README.md
index 45176581cd..43d680af61 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -75,9 +75,6 @@ We are currently running tests on the following platforms:
   camlp5, and with warnings as errors; it runs the test-suite and tests the
   compilation of several external developments.
 
-- Circle CI runs tests that are redundant with GitLab CI and may be removed
-  eventually.
-
 - Travis CI is used to test the compilation of Coq and run the test-suite on
   macOS. It also runs a linter that checks whitespace discipline. A
   [pre-commit hook](../tools/pre-commit) is automatically installed by
@@ -165,8 +162,7 @@ automatically built and uploaded to your GitLab registry, and is
 loaded by subsequent jobs.
 
 **IMPORTANT**: When updating Coq's CI docker image, you must modify
-the `CACHEKEY` variable in [`.gitlab-ci.yml`](../../.gitlab-ci.yml),
-[`.circleci/config.yml`](../../.circleci/config.yml),
+the `CACHEKEY` variable in [`.gitlab-ci.yml`](../../.gitlab-ci.yml)
 and [`Dockerfile`](docker/bionic_coq/Dockerfile)
 
 The Docker building job reuses the uploaded image if it is available,
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index a68cd0933e..9259a6e0c8 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -20,10 +20,6 @@ else
     then
         export CI_PULL_REQUEST="$TRAVIS_PULL_REQUEST"
         export CI_BRANCH="$TRAVIS_BRANCH"
-    elif [ -n "${CIRCLECI}" ];
-    then
-        export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER"
-        export CI_BRANCH="$CIRCLE_BRANCH"
     else # assume local
         CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)"
         export CI_BRANCH