aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-07-11 17:37:20 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-07-12 15:12:59 +0200
commitc05283cb80f81c521bb3a0d8e742d693b7db1a64 (patch)
treefe263de62bcd6cafb85b9ae0151188d3e16a8e8b
parent31fce698ec8c3186dc6af49961e8572e81cab50b (diff)
[ci] Remove warning jobs in favor of default `-warn-error yes`
As discussed in #6930, we remove the warnings jobs and instead do require the developers to submit a clean build.
-rw-r--r--.gitlab-ci.yml38
-rw-r--r--.travis.yml32
2 files changed, 2 insertions, 68 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 0ad68b508..be19a93a3 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -71,7 +71,7 @@ after_script:
- echo 'end:coq.clean'
- echo 'start:coq.config'
- - ./configure -prefix "$(pwd)/_install_ci" ${COQ_EXTRA_CONF}"$COQ_EXTRA_CONF_QUOTE"
+ - ./configure -warn-error yes -prefix "$(pwd)/_install_ci" ${COQ_EXTRA_CONF}"$COQ_EXTRA_CONF_QUOTE"
- echo 'end:coq.config'
- echo 'start:coq.build'
@@ -88,28 +88,6 @@ after_script:
- set +e
-.warnings-template: &warnings-template
- # keep warnings in test stage so we can test things even when warnings occur
- stage: test
- script:
- - set -e
-
- - echo 'start:coq.clean'
- - make clean # ensure that `make clean` works on a fresh clone
- - echo 'end:coq.clean'
-
- - echo 'start:coq.config'
- - ./configure -local ${COQ_EXTRA_CONF}
- - echo 'end:coq.config'
-
- - echo 'start:coq.build'
- - make -j "$NJOBS" coqocaml
- - echo 'end:coq:build'
-
- - set +e
- variables: &warnings-variables
- COQ_EXTRA_CONF: "-native-compiler yes -coqide byte -byte-only -warn-error yes"
-
# every non build job must set dependencies otherwise all build
# artifacts are used together and we may get some random Coq. To that
# purpose, we add a spurious dependency `not-a-real-job` that must be
@@ -264,20 +242,6 @@ pkg:nix:
paths:
- nix-build-coq.drv-0/*/test-suite/logs
-warnings:base:
- <<: *warnings-template
-
-# warnings:32bit:
-# <<: *warnings-template
-# variables:
-# <<: *warnings-variables
-
-warnings:edge:
- <<: *warnings-template
- variables:
- <<: *warnings-variables
- OPAM_SWITCH: edge
-
documentation:
<<: *doc-template
dependencies:
diff --git a/.travis.yml b/.travis.yml
index 3301d97ce..53fbe5821 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -164,36 +164,6 @@ matrix:
- avsm
packages: *extra-packages
- # Ocaml warnings with two compilers
- - if: NOT (type = pull_request)
- env:
- - MAIN_TARGET="coqocaml"
- - EXTRA_CONF="-byte-only -coqide byte -warn-error yes"
- - EXTRA_OPAM="${LABLGTK}"
- addons:
- apt:
- sources:
- - avsm
- packages: &coqide-packages
- - opam
- - aspcud
- - libgtk2.0-dev
- - libgtksourceview2.0-dev
-
- - if: NOT (type = pull_request)
- env:
- - MAIN_TARGET="coqocaml"
- - COMPILER="${COMPILER_BE}"
- - FINDLIB_VER="${FINDLIB_VER_BE}"
- - CAMLP5_VER="${CAMLP5_VER_BE}"
- - EXTRA_CONF="-byte-only -coqide byte -warn-error yes"
- - EXTRA_OPAM="${LABLGTK_BE}"
- addons:
- apt:
- sources:
- - avsm
- packages: *coqide-packages
-
- os: osx
env:
- TEST_TARGET="test-suite"
@@ -260,7 +230,7 @@ script:
- echo -en 'travis_fold:end:coq.clean\\r'
- echo 'Configuring Coq...' && echo -en 'travis_fold:start:coq.config\\r'
-- ./configure ${COQ_DEST} -native-compiler ${NATIVE_COMP} ${EXTRA_CONF}
+- ./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'