Don’t build upstream’s CI on Salsa

2 files changed, 4 insertions, 236 deletions

diff --git a/.travis.yml b/.travis.yml
deleted file mode 100644
index f20599ed..00000000
--- a/.travis.yml
+++ /dev/null
@@ -1,235 +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:
-  apt: true
-  directories:
-  - $HOME/.opam
-
-before_cache:
-  - rm -rf ~/.opam/log/
-
-addons:
-  apt:
-    sources:
-    - avsm
-## Due to issues like
-## https://github.com/travis-ci/travis-ci/issues/8507 ,
-## https://github.com/travis-ci/travis-ci/issues/9000 ,
-## https://github.com/travis-ci/travis-ci/issues/9081 , and
-## https://github.com/travis-ci/travis-ci/issues/9126 , we get frequent
-## failures with using `packages`.  Therefore, for most targets, we
-## instead invoke `apt-get update` manually with `travis_retry` before
-## invoking `apt-get install`, manually, below in the `install:`
-## target.
-#    packages:
-#    - opam
-#    - aspcud
-#    - gcc-multilib
-
-env:
-  global:
-  - NJOBS=2
-  # system is == 4.02.3
-  - COMPILER="system"
-  - COMPILER_BE="4.07.0"
-  - DUNE_VER=".1.0.0"
-  - CAMLP5_VER=".6.14"
-  - CAMLP5_VER_BE=".7.06"
-  - FINDLIB_VER=".1.4.1"
-  - FINDLIB_VER_BE=".1.8.0"
-  - LABLGTK="lablgtk.2.18.3 conf-gtksourceview.2"
-  - LABLGTK_BE="lablgtk.2.18.6 conf-gtksourceview.2"
-  - NATIVE_COMP="yes"
-  - COQ_DEST="-local"
-  - MAIN_TARGET="world"
-
-matrix:
-
-  include:
-    - if: NOT (type = pull_request)
-      env:
-      - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit"
-    - if: NOT (type = pull_request)
-      env:
-      - TEST_TARGET="validate"                           TW="travis_wait"
-    - if: NOT (type = pull_request)
-      env:
-      - TEST_TARGET="validate"   COMPILER="4.02.3+32bit" TW="travis_wait"
-    - if: NOT (type = pull_request)
-      env:
-      - TEST_TARGET="validate"   COMPILER="${COMPILER_BE}+flambda" CAMLP5_VER="${CAMLP5_VER_BE}" EXTRA_CONF="-flambda-opts -O3" FINDLIB_VER="${FINDLIB_VER_BE}"
-    - if: NOT (type = pull_request)
-      env:
-      - TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph"
-    - if: NOT (type = pull_request)
-      env:
-      - TEST_TARGET="ci-coquelicot"
-    - if: NOT (type = pull_request)
-      env:
-      - TEST_TARGET="ci-equations"
-    - if: NOT (type = pull_request)
-      env:
-      - TEST_TARGET="ci-flocq"
-    - if: NOT (type = pull_request)
-      env:
-      - TEST_TARGET="ci-hott"
-    - if: NOT (type = pull_request)
-      env:
-      - TEST_TARGET="ci-ltac2"
-
-    - env:
-      - TEST_TARGET="lint"
-      install: []
-      before_script: []
-      addons:
-      apt:
-        sources: []
-        packages: []
-      script:
-        - dev/lint-repository.sh
-
-    # Full Coq test-suite with two compilers
-    - if: NOT (type = pull_request)
-      env:
-      - TEST_TARGET="sphinx test-suite"
-      - EXTRA_CONF="-coqide opt"
-      - EXTRA_OPAM="hevea ${LABLGTK}"
-      before_install: &sphinx-install
-      - sudo pip3 install bs4 sphinx sphinx_rtd_theme pexpect antlr4-python3-runtime sphinxcontrib-bibtex
-      addons:
-        apt:
-          sources:
-          - avsm
-          packages: &extra-packages
-          - opam
-          - aspcud
-          - libgtk2.0-dev
-          - libgtksourceview2.0-dev
-          - python3
-          - python3-pip
-          - python3-setuptools
-
-    - if: NOT (type = pull_request)
-      env:
-      - TEST_TARGET="sphinx test-suite"
-      - COMPILER="${COMPILER_BE}"
-      - FINDLIB_VER="${FINDLIB_VER_BE}"
-      - CAMLP5_VER="${CAMLP5_VER_BE}"
-      - EXTRA_CONF="-coqide opt"
-      - EXTRA_OPAM="hevea ${LABLGTK_BE}"
-      before_install: *sphinx-install
-      addons:
-        apt:
-          sources:
-          - avsm
-          packages: *extra-packages
-
-    # Full test-suite with flambda
-    - if: NOT (type = pull_request)
-      env:
-      - TEST_TARGET="sphinx test-suite"
-      - COMPILER="${COMPILER_BE}+flambda"
-      - FINDLIB_VER="${FINDLIB_VER_BE}"
-      - CAMLP5_VER="${CAMLP5_VER_BE}"
-      - EXTRA_CONF="-coqide opt -flambda-opts -O3"
-      - EXTRA_OPAM="hevea ${LABLGTK_BE}"
-      before_install: *sphinx-install
-      addons:
-        apt:
-          sources:
-          - avsm
-          packages: *extra-packages
-
-    - os: osx
-      env:
-      - TEST_TARGET="test-suite"
-      - COMPILER="${COMPILER_BE}"
-      - FINDLIB_VER="${FINDLIB_VER_BE}"
-      - CAMLP5_VER="${CAMLP5_VER_BE}"
-      - NATIVE_COMP="no"
-      - COQ_DEST="-local"
-      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
-
-    - if: NOT (type = pull_request)
-      os: osx
-      osx_image: xcode7.3
-      env:
-      - TEST_TARGET=""
-      - COMPILER="${COMPILER_BE}"
-      - FINDLIB_VER="${FINDLIB_VER_BE}"
-      - CAMLP5_VER="${CAMLP5_VER_BE}"
-      - NATIVE_COMP="no"
-      - COQ_DEST="-prefix ${PWD}/_install"
-      - EXTRA_CONF="-coqide opt -warn-error yes"
-      - EXTRA_OPAM="${LABLGTK_BE}"
-      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
-      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
-
-install:
-- if [ "${TRAVIS_OS_NAME}" == "linux" ]; then travis_retry ./dev/tools/sudo-apt-get-update.sh -q; fi
-- if [ "${TRAVIS_OS_NAME}" == "linux" ]; then sudo apt-get install -y opam aspcud gcc-multilib --allow-unauthenticated; fi
-- 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} camlp5${CAMLP5_VER} ${EXTRA_OPAM}
-- opam list
-
-script:
-
-- set -e
-- 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/debian/gbp.conf b/debian/gbp.conf
index f9ed7826..a4ee2a5f 100644
--- a/debian/gbp.conf
+++ b/debian/gbp.conf
@@ -55,4 +55,7 @@ filter = [
     # These files will be patched in with properly licensed replacements once
     # https://github.com/coq/coq/pull/9282 is merged.
     "plugins/ssrmatching/ssrmatching.mli",
-    "plugins/ssrmatching/ssrmatching.v" ]
+    "plugins/ssrmatching/ssrmatching.v",
+
+    # This tries to build upstream's CI on Salsa, which doesn't work.
+    ".travis.yml" ]