Remove travis

The azure OSX job replaces the first travis job, and the second always
fails and so is useless.

9 files changed, 9 insertions, 152 deletions

diff --git a/.travis.yml b/.travis.yml
deleted file mode 100644
index 855d36048d..0000000000
--- a/.travis.yml
+++ /dev/null
@@ -1,116 +0,0 @@
-dist: trusty
-
-# Travis builds are slower using sudo: false (the container-based
-# infrastructure) as of March 2017; see
-# https://github.com/coq/coq/pull/467 for some discussion.
-sudo: required
-
-# Until Ocaml becomes a language, we set a known one.
-language: c
-
-cache:
-  directories:
-  - $HOME/.opam
-
-before_cache:
-  - rm -rf ~/.opam/log/
-
-env:
-  global:
-  - NJOBS=2
-  - COMPILER="4.07.0"
-  - DUNE_VER=".1.2.1"
-  - FINDLIB_VER=".1.8.0"
-  - LABLGTK="lablgtk.2.18.6 conf-gtksourceview.2"
-  - NATIVE_COMP="yes"
-  - COQ_DEST="-local"
-  - MAIN_TARGET="world"
-
-matrix:
-  include:
-    - os: osx
-      env:
-      - TEST_TARGET="test-suite"
-      - NATIVE_COMP="no"
-      - COQ_DEST="-local"
-      - EXTRA_OPAM="ounit"
-      before_install:
-      - brew update
-      - brew unlink python
-      - brew install gnu-time
-      # only way to continue using OPAM 1.2
-      - brew install https://raw.githubusercontent.com/Homebrew/homebrew-core/d156edeeed7291f4bc1e08620b331bbd05d52b78/Formula/opam.rb
-      - opam init -j "$NJOBS" --compiler="$COMPILER" -n -y
-      - opam switch "$COMPILER" && opam update
-      - eval $(opam config env)
-      - opam config list
-      - opam install -j "$NJOBS" -y num ocamlfind${FINDLIB_VER} dune${DUNE_VER} ${EXTRA_OPAM}
-      - opam list
-
-    - if: NOT (type = pull_request)
-      os: osx
-      osx_image: xcode7.3
-      env:
-      - TEST_TARGET=""
-      - NATIVE_COMP="no"
-      - COQ_DEST="-prefix $PWD/_install_ci"
-      - EXTRA_CONF="-coqide opt -warn-error yes"
-      - EXTRA_OPAM="$LABLGTK"
-      before_install:
-      - brew update
-      - brew unlink python
-      - brew install gnu-time gtk+ expat gtksourceview gdk-pixbuf
-      # only way to continue using OPAM 1.2
-      - brew install https://raw.githubusercontent.com/Homebrew/homebrew-core/d156edeeed7291f4bc1e08620b331bbd05d52b78/Formula/opam.rb
-      - brew unlink python@2
-      - brew install python3
-      - pip3 install macpack
-      - opam init -j "$NJOBS" --compiler="$COMPILER" -n -y
-      - opam switch "$COMPILER" && opam update
-      - eval $(opam config env)
-      - opam config list
-      - opam install -j "$NJOBS" -y num ocamlfind${FINDLIB_VER} dune${DUNE_VER} ${EXTRA_OPAM}
-      - opam list
-      before_deploy:
-        - dev/build/osx/make-macos-dmg.sh
-      deploy:
-      - provider: bintray
-        user: maximedenes
-        file: .bintray.json
-        key:
-          secure: "gUvXWwWR0gicDqsKOnBfe45taToSFied6gN8tCa5IOtl6E6gFoHoPZ83ZWXQsZP50oMDFS5eji0VQAFGEbOsGrTZaD9Y9Jnu34NND78SWL1tsJ6nHO3aCAoMpB0N3+oRuF6S+9HStU6KXWqgj+GeU4vZ4TOlG01RGctJa6U3vII="
-        skip_cleanup: true
-        on:
-          all_branches: true
-
-before_install:
-- if [ "$TRAVIS_PULL_REQUEST" != "false" ]; then echo "Tested commit (followed by parent commits):"; git log -1; for commit in `git log -1 --format="%P"`; do echo; git log -1 $commit; done; fi
-
-script:
-
-- set -e
-- echo 'Testing make clean...' && echo -en 'travis_fold:start:coq.clean\\r'
-- make clean # ensure that `make clean` works on a fresh clone
-- echo -en 'travis_fold:end:coq.clean\\r'
-
-- echo 'Configuring Coq...' && echo -en 'travis_fold:start:coq.config\\r'
-- ./configure $COQ_DEST -warn-error yes -native-compiler $NATIVE_COMP $EXTRA_CONF
-- echo -en 'travis_fold:end:coq.config\\r'
-
-- echo 'Building Coq...' && echo -en 'travis_fold:start:coq.build\\r'
-- make -j $NJOBS $MAIN_TARGET
-- echo -en 'travis_fold:end:coq.build\\r'
-
-- echo 'Running tests...' && echo -en 'travis_fold:start:coq.test\\r'
-- if [ -n "$TEST_TARGET" ]; then $TW make -j $NJOBS $TEST_TARGET; fi
-- echo -en 'travis_fold:end:coq.test\\r'
-- set +e
-
-# Testing Gitter webhook
-notifications:
-  webhooks:
-    urls:
-      - https://webhooks.gitter.im/e/3cdabdec318214c7cd63
-    on_success: change  # options: [always|never|change] default: always
-    on_failure: always  # options: [always|never|change] default: always
-    on_start: never     # options: [always|never|change] default: always
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index de7fb9183c..bb0e388cdd 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -55,7 +55,7 @@ please add an entry to [`dev/doc/critical-bugs`](/dev/doc/critical-bugs).
 
 Don't be alarmed if the pull request process takes some time. It can take a few days to get feedback, approval on the final changes, and then a merge. Coq doesn't release new versions very frequently so it can take a few months for your change to land in a released version. That said, you can start using the latest Coq `master` branch to take advantage of all the new features, improvements, and fixes.
 
-Whitespace discipline (do not indent using tabs, no trailing spaces, text files end with newlines) is checked by Travis (using `git diff --check`). We ship a [`dev/tools/pre-commit`](/dev/tools/pre-commit) git hook which fixes these errors at commit time. `configure` automatically sets you up to use it, unless you already have a hook at `.git/hooks/pre-commit`.
+Whitespace discipline (do not indent using tabs, no trailing spaces, text files end with newlines) is checked by the `lint` job on GitLab CI (using `git diff --check`). We ship a [`dev/tools/pre-commit`](/dev/tools/pre-commit) git hook which fixes these errors at commit time. `configure` automatically sets you up to use it, unless you already have a hook at `.git/hooks/pre-commit`.
 
 Here are a few tags Coq developers may add to your PR and what they mean. In general feedback and requests for you as the pull request author will be in the comments and tags are only used to organize pull requests.
 
diff --git a/README.md b/README.md
index e8300ca552..65673ab1fe 100644
--- a/README.md
+++ b/README.md
@@ -2,7 +2,6 @@
 
 [![GitLab][gitlab-badge]][gitlab-link]
 [![Azure Pipelines][azure-badge]][azure-link]
-[![Travis][travis-badge]][travis-link]
 [![Appveyor][appveyor-badge]][appveyor-link]
 [![Gitter][gitter-badge]][gitter-link]
 [![DOI][doi-badge]][doi-link]
@@ -13,9 +12,6 @@
 [azure-badge]: https://dev.azure.com/coq/coq/_apis/build/status/coq.coq?branchName=master
 [azure-link]: https://dev.azure.com/coq/coq/_build/latest?definitionId=1?branchName=master
 
-[travis-badge]: https://travis-ci.org/coq/coq.svg?branch=master
-[travis-link]: https://travis-ci.org/coq/coq/builds
-
 [appveyor-badge]: https://ci.appveyor.com/api/projects/status/eln43k05pa2vm908/branch/master?svg=true
 [appveyor-link]: https://ci.appveyor.com/project/coq/coq/branch/master
 
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 07a13b8204..2e934ff0c0 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -444,9 +444,6 @@ function load_overlay_data {
   else
     export CI_BRANCH=""
     export CI_PULL_REQUEST=""
-    # Used when building 8.8.0 with the latest scripts
-    export TRAVIS_BRANCH=""
-    export TRAVIS_PULL_REQUEST=""
   fi
 
   for overlay in /build/user-overlays/*.sh; do
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
index 6663fbecf8..10b4f9b044 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -16,14 +16,12 @@ We are currently running tests on the following platforms:
   `./configure`. It should allow complying with this discipline
   without pain.
 
-- Travis CI is used to test the compilation of Coq and run the test-suite on
-  macOS.
-
 - AppVeyor is used to test the compilation of Coq and run the test-suite on
   Windows.
 
 - Azure Pipelines is used to test the compilation of Coq and run the
-  test-suite on Windows. It is expected to replace appveyor eventually.
+  test-suite on Windows and on macOS. It is expected to replace
+  appveyor eventually.
 
 You can anticipate the results of most of these tests prior to submitting your
 PR by running GitLab CI on your private branches. To do so follow these steps:
diff --git a/dev/ci/ci-wrapper.sh b/dev/ci/ci-wrapper.sh
index 12a70176c2..9ca8f76054 100755
--- a/dev/ci/ci-wrapper.sh
+++ b/dev/ci/ci-wrapper.sh
@@ -6,13 +6,6 @@
 
 set -eo pipefail
 
-function travis_fold {
-    if [ -n "${TRAVIS}" ];
-    then
-	echo "travis_fold:$1:$2"
-    fi
-}
-
 CI_NAME="$1"
 CI_SCRIPT="ci-${CI_NAME}.sh"
 
@@ -22,6 +15,5 @@ cd "${DIR}/../.."
 
 export TIMED=1
 "${DIR}/${CI_SCRIPT}" 2>&1 | tee time-of-build.log
-travis_fold 'start' 'coq.test.timing' && echo 'Aggregating timing log...'
+echo 'Aggregating timing log...'
 python ./tools/make-one-time-file.py time-of-build.log
-travis_fold 'end' 'coq.test.timing'
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
index 56fdab0c26..5705857d76 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -93,7 +93,7 @@ put the approriate label. Otherwise, they are expected to merge the PR using the
 
 When CI has a few failures which look spurious, restarting the corresponding
 jobs is a good way of ensuring this was indeed the case.
-To restart a job on Travis or on AppVeyor, you should connect using your GitHub
+To restart a job on AppVeyor, you should connect using your GitHub
 account; being part of the Coq organization on GitHub should give you the
 permission to do so.
 To restart a job on GitLab CI, you should sign into GitLab (this can be done
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index a27dacc5a7..72e2930386 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -143,7 +143,7 @@ fi
 # Sanity check: PR has an outdated version of CI
 
 BASE_COMMIT=$(echo "$PRDATA" | jq -r '.base.sha')
-CI_FILES=(".travis.yml" ".gitlab-ci.yml" "appveyor.yml")
+CI_FILES=(".gitlab-ci.yml" "appveyor.yml")
 
 if ! git diff --quiet "$BASE_COMMIT" "$LOCAL_BRANCH_COMMIT" -- "${CI_FILES[@]}"
 then
diff --git a/test-suite/report.sh b/test-suite/report.sh
index cef615266b..71aac029ea 100755
--- a/test-suite/report.sh
+++ b/test-suite/report.sh
@@ -24,21 +24,11 @@ cp summary.log "$SAVEDIR"/
 rm "$FAILED"
 
 # print info
-if [ -n "$TRAVIS" ] || [ -n "$APPVEYOR" ] || [ -n "$PRINT_LOGS" ]; then
+if [ -n "$APPVEYOR" ] || [ -n "$PRINT_LOGS" ]; then
     find logs/ -name '*.log' -not -name 'summary.log' -print0 | while IFS= read -r -d '' file; do
-        if [ -n "$TRAVIS" ]; then
-            # ${foo////.} replaces every / by . in $foo
-            printf 'travis_fold:start:coq.logs.%s\n' "${file////.}";
-        else printf '%s\n' "$file"
-        fi
-
+        printf '%s\n' "$file"
         cat "$file"
-
-        if [ -n "$TRAVIS" ]; then
-            # ${foo////.} replaces every / by . in $foo
-            printf 'travis_fold:end:coq.logs.%s\n' "${file////.}";
-        else printf '\n'
-        fi
+        printf '\n'
     done
     printed_logs=1
 fi