From f6b0d8b78ae25c8b1c6b901e57a5f4e38f20cdbd Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 5 May 2017 13:19:21 +0200
Subject: Travis: do not run the tests if building Coq fails

---
 .travis.yml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.travis.yml b/.travis.yml
index 5604551879..8dcc34a8d2 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -115,6 +115,7 @@ install:
 
 script:
 
+- set -e
 - echo 'Configuring Coq...' && echo -en 'travis_fold:start:coq.config\\r'
 - ./configure -local -usecamlp5 -native-compiler yes ${EXTRA_CONF}
 - echo -en 'travis_fold:end:coq.config\\r'
@@ -126,6 +127,7 @@ script:
 - echo 'Running tests...' && echo -en 'travis_fold:start:coq.test\\r'
 - ${TW} make -j ${NJOBS} ${TEST_TARGET}
 - echo -en 'travis_fold:end:coq.test\\r'
+- set +e
 
 # Testing Gitter webhook
 notifications:
-- 
cgit v1.2.3


From 8252ff7ef7159a2493dd5ac76a647a8b96a5a692 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 5 May 2017 14:11:12 +0200
Subject: Travis: deduplicate package list for coqide+documentation targets

---
 .travis.yml | 18 ++----------------
 1 file changed, 2 insertions(+), 16 deletions(-)

diff --git a/.travis.yml b/.travis.yml
index 8dcc34a8d2..158f61cfdb 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -65,7 +65,7 @@ matrix:
         apt:
           sources:
           - avsm
-          packages:
+          packages: &extra-packages
           - opam
           - aspcud
           - libgtk2.0-dev
@@ -90,21 +90,7 @@ matrix:
         apt:
           sources:
           - avsm
-          packages:
-          - opam
-          - aspcud
-          - libgtk2.0-dev
-          - libgtksourceview2.0-dev
-          - texlive-latex-base
-          - texlive-latex-recommended
-          - texlive-latex-extra
-          - texlive-math-extra
-          - texlive-fonts-recommended
-          - texlive-fonts-extra
-          - latex-xcolor
-          - ghostscript
-          - transfig
-          - imagemagick
+          packages: *extra-packages
 
 install:
 - opam init -j ${NJOBS} --compiler=${COMPILER} -n -y
-- 
cgit v1.2.3


From d8d56dfadc571fdf23ff9f8cb97d4c8cd96691ee Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 5 May 2017 14:24:23 +0200
Subject: Travis: add -warn-error targets (standard and 4.04.1 ocaml)

---
 .travis.yml  | 28 ++++++++++++++++++++++++++++
 Makefile.dev |  5 ++++-
 2 files changed, 32 insertions(+), 1 deletion(-)

diff --git a/.travis.yml b/.travis.yml
index 158f61cfdb..06ce3cae26 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -91,6 +91,34 @@ matrix:
           sources:
           - avsm
           packages: *extra-packages
+    - env:
+      - TEST_TARGET="coqocaml"
+      - EXTRA_CONF="-coqide opt -warn-error"
+      - EXTRA_OPAM="lablgtk-extras hevea"
+      # dummy target
+      - BUILD_TARGET="clean"
+      addons:
+        apt:
+          sources:
+          - avsm
+          packages: &coqide-packages
+          - opam
+          - aspcud
+          - libgtk2.0-dev
+          - libgtksourceview2.0-dev
+    - env:
+      - TEST_TARGET="coqocaml"
+      - COMPILER="4.04.1"
+      - CAMLP5_VER="6.17"
+      - EXTRA_CONF="-coqide opt -warn-error"
+      - EXTRA_OPAM="lablgtk-extras hevea"
+      # dummy target
+      - BUILD_TARGET="clean"
+      addons:
+        apt:
+          sources:
+          - avsm
+          packages: *coqide-packages
 
 install:
 - opam init -j ${NJOBS} --compiler=${COMPILER} -n -y
diff --git a/Makefile.dev b/Makefile.dev
index 5931e46dd0..1803cc8ffe 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -97,7 +97,10 @@ minibyte: $(COQTOPBYTE) pluginsbyte
 pluginsopt: $(PLUGINSOPT)
 pluginsbyte: $(PLUGINS)
 
-.PHONY: coqlight states miniopt minibyte pluginsopt pluginsbyte
+# This should build all the ocaml code but not (most of) the .v files
+coqocaml: tools coqbinaries pluginsopt coqide printers
+
+.PHONY: coqlight states miniopt minibyte pluginsopt pluginsbyte coqocaml
 
 ##########################
 ### 2) core ML components
-- 
cgit v1.2.3