diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-05-17 09:35:06 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-05-17 09:35:06 +0200 |
| commit | 4b53985c2888827fe030294f95b5975d5e34e4c7 (patch) | |
| tree | fc01eb8a20ebe09abe73a2707d53f0393b8f8ceb | |
| parent | 772de8aba675731ed8d476ea0bc628ee21751dc8 (diff) | |
| parent | d8d56dfadc571fdf23ff9f8cb97d4c8cd96691ee (diff) | |
Merge PR#614: Improve Travis
| -rw-r--r-- | .travis.yml | 40 | ||||
| -rw-r--r-- | Makefile.dev | 5 |
2 files changed, 32 insertions, 13 deletions
diff --git a/.travis.yml b/.travis.yml index 560455187..06ce3cae2 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,35 @@ matrix: apt: sources: - avsm - packages: + 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 - - texlive-latex-base - - texlive-latex-recommended - - texlive-latex-extra - - texlive-math-extra - - texlive-fonts-recommended - - texlive-fonts-extra - - latex-xcolor - - ghostscript - - transfig - - imagemagick + - 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 @@ -115,6 +129,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 +141,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: diff --git a/Makefile.dev b/Makefile.dev index 5931e46dd..1803cc8ff 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 |