diff options
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/README.md | 6 | ||||
| -rw-r--r-- | dev/ci/ci-common.sh | 4 | ||||
| -rwxr-xr-x | dev/ci/ci-hott.sh | 2 | ||||
| -rw-r--r-- | dev/ci/user-overlays/07859-printers.sh | 6 |
4 files changed, 8 insertions, 10 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 diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index 6ded97984e..184b90a50b 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -7,4 +7,4 @@ HoTT_CI_DIR="${CI_BUILD_DIR}"/HoTT git_checkout "${HoTT_CI_BRANCH}" "${HoTT_CI_GITURL}" "${HoTT_CI_DIR}" -( cd "${HoTT_CI_DIR}" && ./autogen.sh && ./configure && make ) +( cd "${HoTT_CI_DIR}" && ./autogen.sh && ./configure && make && make validate ) diff --git a/dev/ci/user-overlays/07859-printers.sh b/dev/ci/user-overlays/07859-printers.sh new file mode 100644 index 0000000000..27f588e214 --- /dev/null +++ b/dev/ci/user-overlays/07859-printers.sh @@ -0,0 +1,6 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "7859" ] || [ "$CI_BRANCH" = "rm-univ-broken-printing" ]; then + Equations_CI_BRANCH=fix-printers + Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations +fi |