[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

6 files changed, 1 insertions, 217 deletions

diff --git a/.circleci/config.yml b/.circleci/config.yml
deleted file mode 100644
index adab42c622..0000000000
--- a/.circleci/config.yml
+++ /dev/null
@@ -1,202 +0,0 @@
-# This file used to contain configuration to also build documentation and CoqIDE,
-# run the test-suite and the validate targets,
-# including with 32-bits architecture or bleeding-edge compiler.
-
-defaults:
-  params: &params
-    # Following parameters are used in Coq CircleCI Job (using yaml
-    # reference syntax)
-    working_directory: ~/coq
-    docker:
-      - image: $CI_REGISTRY_IMAGE:$CACHEKEY
-
-  environment: &envvars
-    CACHEKEY: "bionic_coq-V2018-07-11-V2"
-    CI_REGISTRY_IMAGE: registry.gitlab.com/coq/coq
-
-version: 2
-
-before_script: &before_script
-  name: Setup OPAM Switch
-  command: |
-    echo export TERM=xterm >> ~/.profile
-    source ~/.profile
-    echo . ~/.profile >> $BASH_ENV
-    printenv | sort
-    opam switch "$COMPILER"
-    opam config list
-    opam list
-
-.build-template: &build-template
-  <<: *params
-  steps:
-    - checkout
-    - run: *before_script
-    - run: &build-clean
-        name: Clean
-        command: |
-          make clean # ensure that `make clean` works on a fresh clone
-    - run: &build-configure
-        name: Configure
-        command: |
-          ./configure -local -native-compiler ${NATIVE_COMP} -coqide no
-    - run: &build-build
-        name: Build
-        command: |
-          make -j ${NJOBS} byte
-          make -j ${NJOBS}
-          make test-suite/misc/universes/all_stdlib.v
-    - persist_to_workspace:
-        root: &workspace ~/
-        paths:
-          - coq/
-
-  environment:
-    <<: *envvars
-    NATIVE_COMP: "yes"
-
-.ci-template: &ci-template
-  <<: *params
-  steps:
-    - run: *before_script
-    - attach_workspace: &attach_workspace
-        at: *workspace
-
-    - run:
-        name: Test
-        command: |
-          dev/ci/ci-wrapper.sh ${CIRCLE_JOB}
-    - persist_to_workspace:
-        root: *workspace
-        paths:
-          - coq/
-  environment: *envvars
-
-# Defines individual jobs, see the workflows section below for job orchestration
-jobs:
-
-  # Build and prepare test environment
-  build: *build-template
-
-  bignums:
-    <<: *ci-template
-
-  color:
-    <<: *ci-template
-
-  compcert:
-    <<: *ci-template
-
-  coq-dpdgraph:
-    <<: *ci-template
-
-  coquelicot:
-    <<: *ci-template
-
-  cross-crypto:
-    <<: *ci-template
-
-  elpi:
-    <<: *ci-template
-
-  equations:
-    <<: *ci-template
-
-  geocoq:
-    <<: *ci-template
-
-  fcsl-pcm:
-    <<: *ci-template
-
-  fiat-crypto:
-    <<: *ci-template
-
-  fiat-parsers:
-    <<: *ci-template
-
-  flocq:
-    <<: *ci-template
-
-  math-classes:
-    <<: *ci-template
-
-  corn:
-    <<: *ci-template
-
-  formal-topology:
-    <<: *ci-template
-
-  hott:
-    <<: *ci-template
-
-  iris-lambda-rust:
-    <<: *ci-template
-
-  ltac2:
-    <<: *ci-template
-
-  math-comp:
-    <<: *ci-template
-
-  mtac2:
-    <<: *ci-template
-
-  pidetop:
-    <<: *ci-template
-
-  sf:
-    <<: *ci-template
-
-  unimath:
-    <<: *ci-template
-
-  vst:
-    <<: *ci-template
-
-workflows:
-  version: 2
-
-  # Run on each push
-  main:
-    jobs:
-      - build
-
-      - bignums: &req-main
-          requires:
-            - build
-      - color:
-          requires:
-            - build
-            - bignums
-      # - compcert: *req-main
-      # - coq-dpdgraph: *req-main
-      # - coquelicot: *req-main
-      # - cross-crypto: *req-main
-      # - elpi: *req-main
-      # - equations: *req-main
-      # - geocoq: *req-main
-      # - fcsl-pcm: *req-main
-      # - fiat-crypto: *req-main
-      # - fiat-parsers: *req-main
-      # - flocq: *req-main
-      - math-classes:
-          requires:
-            - build
-            - bignums
-      # - mtac2: *req-main
-      - corn:
-          requires:
-            - build
-            - math-classes
-      - formal-topology:
-          requires:
-            - build
-            - corn
-      # - hott: *req-main
-      # - iris-lambda-rust: *req-main
-      # - ltac2: *req-main
-      # - math-comp: *req-main
-      # - pidetop: *req-main
-      # - sf: *req-main
-      # - unimath: *req-main
-      # - vst: *req-main
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index 384e46723a..20d49e675f 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -9,7 +9,6 @@
 ########## CI infrastructure ##########
 
 /dev/ci/          @coq/ci-maintainers
-/.circleci/       @coq/ci-maintainers
 /.travis.yml      @coq/ci-maintainers
 /.gitlab-ci.yml   @coq/ci-maintainers
 
diff --git a/README.md b/README.md
index 67f4f6fea1..fcf20f0097 100644
--- a/README.md
+++ b/README.md
@@ -3,7 +3,6 @@
 [![pipeline status](https://gitlab.com/coq/coq/badges/master/pipeline.svg)](https://gitlab.com/coq/coq/commits/master)
 [![Travis](https://travis-ci.org/coq/coq.svg?branch=master)](https://travis-ci.org/coq/coq/builds)
 [![Appveyor](https://ci.appveyor.com/api/projects/status/eln43k05pa2vm908/branch/master?svg=true)](https://ci.appveyor.com/project/coq/coq/branch/master)
-[![Circle CI](https://circleci.com/gh/coq/coq/tree/master.svg?style=shield)](https://circleci.com/gh/coq/workflows/coq/tree/master)
 [![Gitter](https://badges.gitter.im/coq/coq.svg)](https://gitter.im/coq/coq)
 [![DOI](https://zenodo.org/badge/DOI/10.5281/zenodo.1003420.svg)](https://doi.org/10.5281/zenodo.1003420)
 
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
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 33b4023272..b8aac8b6f8 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -192,10 +192,6 @@ PRINT_LOGS?=
 TRAVIS?= # special because we want to print travis_fold directives
 ifdef APPVEYOR
 PRINT_LOGS:=APPVEYOR
-else
-ifdef CIRCLECI
-PRINT_LOGS:=CIRCLECI
-endif #CIRCLECI
 endif #APPVEYOR
 
 report: summary.log