aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-11-27 14:44:15 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-11-28 12:57:28 +0100
commitb16f9e8a17d2223e6045e57a11bef2aa44ffb6ff (patch)
treec5b87ec42015910929d4f86e0f1ef3d6eca83f25
parent79810d6665be221bb35e131a453fcd4010580ebb (diff)
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.
-rw-r--r--.gitlab-ci.yml2
-rw-r--r--.travis.yml4
-rw-r--r--Makefile.dev2
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