From 3b0fc06ccc21f23df111d59cccd1e5ecae4de919 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 27 Nov 2017 14:31:45 +0100
Subject: Travis: do not build stdlib in [warnings] jobs.

---
 .travis.yml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/.travis.yml b/.travis.yml
index 1f6bb11e0e..44c799c714 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -39,6 +39,7 @@ env:
   - LABLGTK_BE="lablgtk.2.18.6 lablgtk-extras.1.6"
   - NATIVE_COMP="yes"
   - COQ_DEST="-local"
+  - MAIN_TARGET="world"
   # Main test suites
   matrix:
   - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit"
@@ -139,7 +140,7 @@ matrix:
 
     # Ocaml warnings with two compilers
     - env:
-      - TEST_TARGET="coqocaml"
+      - MAIN_TARGET="coqocaml"
       - EXTRA_CONF="-coqide opt -warn-error"
       - EXTRA_OPAM="hevea ${LABLGTK}"
       # dummy target
@@ -155,7 +156,7 @@ matrix:
           - libgtksourceview2.0-dev
 
     - env:
-      - TEST_TARGET="coqocaml"
+      - MAIN_TARGET="coqocaml"
       - COMPILER="${COMPILER_BE}"
       - FINDLIB_VER="${FINDLIB_VER_BE}"
       - CAMLP5_VER="${CAMLP5_VER_BE}"
@@ -224,11 +225,11 @@ script:
 - echo -en 'travis_fold:end:coq.config\\r'
 
 - echo 'Building Coq...' && echo -en 'travis_fold:start:coq.build\\r'
-- make -j ${NJOBS}
+- make -j ${NJOBS} ${MAIN_TARGET}
 - echo -en 'travis_fold:end:coq.build\\r'
 
 - echo 'Running tests...' && echo -en 'travis_fold:start:coq.test\\r'
-- ${TW} make -j ${NJOBS} ${TEST_TARGET}
+- if [ -n "${TEST_TARGET}" ]; then ${TW} make -j ${NJOBS} ${TEST_TARGET}; fi
 - echo -en 'travis_fold:end:coq.test\\r'
 - set +e
 
-- 
cgit v1.2.3


From 79810d6665be221bb35e131a453fcd4010580ebb Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 28 Nov 2017 12:55:55 +0100
Subject: Fix native compute for byte compiled Coq.

---
 kernel/nativelib.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index e9c0e171ac..4e7d6b218c 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -87,7 +87,7 @@ let call_compiler ?profile:(profile=false) ml_filename =
       []
   in
   let flambda_args =
-    if Coq_config.caml_version_nums >= [4;3;0] then
+    if Coq_config.caml_version_nums >= [4;3;0] && Dynlink.is_native then
       (* We play safe for now, and use the native compiler
          with -Oclassic, however it is likely that `native_compute`
          users can benefit from tweaking here.
-- 
cgit v1.2.3


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 c0a01f3fda..20dac57a77 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 44c799c714..83a4e7fdda 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 dc4ded3977..d2a1e9235e 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