From b16f9e8a17d2223e6045e57a11bef2aa44ffb6ff Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 27 Nov 2017 14:44:15 +0100 Subject: CI: use -byte-only in [warnings] jobs. This avoids mixing native and byte compilation as the debug printers are always byte compiled and the tools have no .byte rule, only the OCAMLBEST rule. --- .gitlab-ci.yml | 2 +- .travis.yml | 4 ++-- Makefile.dev | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index c0a01f3fd..20dac57a7 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -105,7 +105,7 @@ before_script: - set +e variables: &warnings-variables - EXTRA_CONF: "-native-compiler yes -coqide opt" + EXTRA_CONF: "-native-compiler yes -coqide byte -byte-only" EXTRA_PACKAGES: "$COQIDE_PACKAGES" EXTRA_OPAM: "$COQIDE_OPAM" diff --git a/.travis.yml b/.travis.yml index 44c799c71..83a4e7fdd 100644 --- a/.travis.yml +++ b/.travis.yml @@ -141,7 +141,7 @@ matrix: # Ocaml warnings with two compilers - env: - MAIN_TARGET="coqocaml" - - EXTRA_CONF="-coqide opt -warn-error" + - EXTRA_CONF="-byte-only -coqide byte -warn-error" - EXTRA_OPAM="hevea ${LABLGTK}" # dummy target - BUILD_TARGET="clean" @@ -160,7 +160,7 @@ matrix: - COMPILER="${COMPILER_BE}" - FINDLIB_VER="${FINDLIB_VER_BE}" - CAMLP5_VER="${CAMLP5_VER_BE}" - - EXTRA_CONF="-coqide opt -warn-error" + - EXTRA_CONF="-byte-only -coqide byte -warn-error" - EXTRA_OPAM="num hevea ${LABLGTK_BE}" # dummy target - BUILD_TARGET="clean" diff --git a/Makefile.dev b/Makefile.dev index dc4ded397..d2a1e9235 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -98,7 +98,7 @@ pluginsopt: $(PLUGINSOPT) pluginsbyte: $(PLUGINS) # This should build all the ocaml code but not (most of) the .v files -coqocaml: tools coqbinaries pluginsopt coqide printers bin/votour +coqocaml: tools coqbinaries $(PLUGINSCMO:.cmo=$(DYNOBJ)) coqide printers bin/votour .PHONY: coqlight states miniopt minibyte pluginsopt pluginsbyte coqocaml -- cgit v1.2.3