From c05283cb80f81c521bb3a0d8e742d693b7db1a64 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 11 Jul 2018 17:37:20 +0200 Subject: [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. --- .gitlab-ci.yml | 38 +------------------------------------- .travis.yml | 32 +------------------------------- 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' -- cgit v1.2.3 From 77e3b3c43aebe9ad18ac99b34cf6dfac1ecc93fd Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 11 Jul 2018 18:32:37 +0200 Subject: [warnings] Disable warning 59 [assignment to a non-mutable value] to make flambda happy. See issue #8043. Using `[@@@ocaml.warning "-59"]` to disable this fails, it seems like an OCaml bug. --- configure.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/configure.ml b/configure.ml index 194f47c49..0b6b47e9a 100644 --- a/configure.ml +++ b/configure.ml @@ -647,8 +647,9 @@ let camltag = match caml_version_list with 48: implicit elimination of optional arguments: too common 50: unexpected documentation comment: too common and annoying to avoid 56: unreachable match case: the [_ -> .] syntax doesn't exist in 4.02.3 + 59: "potential assignment to a non-mutable value": See Coq's issue #8043 *) -let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-50" +let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-50-59" let coq_warn_error = if !prefs.warn_error then "-warn-error +a" -- cgit v1.2.3 From a069562bc0d4e82f6b1587864a8297b21a3250cc Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 11 Jul 2018 20:14:45 +0200 Subject: [warnings] Disable warning 58 "no cmx file was found in path" See https://github.com/ocaml/num/issues/9 --- configure.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/configure.ml b/configure.ml index 0b6b47e9a..3a98e8892 100644 --- a/configure.ml +++ b/configure.ml @@ -647,9 +647,10 @@ let camltag = match caml_version_list with 48: implicit elimination of optional arguments: too common 50: unexpected documentation comment: too common and annoying to avoid 56: unreachable match case: the [_ -> .] syntax doesn't exist in 4.02.3 + 58: "no cmx file was found in path": See https://github.com/ocaml/num/issues/9 59: "potential assignment to a non-mutable value": See Coq's issue #8043 *) -let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-50-59" +let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-50-58-59" let coq_warn_error = if !prefs.warn_error then "-warn-error +a" -- cgit v1.2.3