aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/README.md
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-07-27 14:33:09 +0200
committerEmilio Jesus Gallego Arias2018-07-27 14:33:09 +0200
commitdfafe315dc2ced29e4522b5f56dfe0f9594645e6 (patch)
tree59a4c1604988a5e724c52932c11bed4cc3c1f879 /dev/ci/README.md
parent05ef2d2234578294cd0be6aace2b4ed4c9815d37 (diff)
[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
Diffstat (limited to 'dev/ci/README.md')
-rw-r--r--dev/ci/README.md6
1 files changed, 1 insertions, 5 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,