Commit da351fb8 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Merge branch 'bugfix/v1.1'

parents 2b77287d 638ee537
......@@ -9,11 +9,16 @@ stages:
script:
- misc/ci-docker.sh misc/ci-local.sh
build:
build-system:
variables:
COMPILER: system
<<: *build_definition
build-4.02.3:
variables:
COMPILER: 4.02.3
<<: *build_definition
build-4.03.0:
variables:
COMPILER: 4.03.0
......@@ -39,22 +44,25 @@ build-4.07.0:
COMPILER: 4.07.0
<<: *build_definition
bench:
.bench_template1: &bench_definition_always
stage: test
variables:
COMPILER: 4.04.0
OPAM_PACKAGES: alt-ergo.2.0.0
script:
- misc/ci-docker.sh misc/ci-local.sh bench ide
.bench_template: &bench_definition
stage: test
script:
- misc/ci-docker.sh misc/ci-local.sh bench ide
.bench_template2: &bench_definition
<<: *bench_definition_always
only:
- tags
- schedules
bench-system:
<<: *bench_definition_always
bench-4.02.3:
variables:
COMPILER: 4.02.3
<<: *bench_definition
bench-4.03.0:
variables:
COMPILER: 4.03.0
......@@ -78,12 +86,12 @@ bench-4.06.1:
bench-4.07.0:
variables:
COMPILER: 4.07.0
<<: *bench_definition
<<: *bench_definition_always
full:
full-4.07.0:
stage: test
variables:
COMPILER: 4.04.0
COMPILER: 4.07.0
DEBIAN_PACKAGES: hevea rubber texlive-latex-extra lmodern texlive-fonts-recommended
OPAM_PACKAGES: coq-flocq.2.6.1 js_of_ocaml-ppx alt-ergo.2.0.0
script:
......@@ -92,7 +100,7 @@ full:
nightly-bench:
stage: nightly
variables:
COMPILER: 4.04.0
COMPILER: 4.05.0
DEBIAN_PACKAGES: cvc3 spass
OPAM_PACKAGES: alt-ergo.2.0.0 zenon.0.8.0 coq.8.7.1 coq-flocq.2.6.1
script:
......@@ -101,7 +109,7 @@ nightly-bench:
ce-bench:
stage: nightly
variables:
COMPILER: 4.04.0
COMPILER: 4.05.0
DEBIAN_PACKAGES: cvc3 spass
OPAM_PACKAGES: alt-ergo.2.0.0 zenon.0.8.0 coq.8.7.1 coq-flocq.2.6.1
script:
......
......@@ -98,6 +98,7 @@ drivers () {
}
valid_goals () {
bin/why3$suffix --list-provers | grep -q Alt-Ergo || return 0
pgm="bin/why3prove$suffix"
test -d $1 || exit 1
for f in $1/*.mlw; do
......@@ -113,6 +114,7 @@ valid_goals () {
}
invalid_goals () {
bin/why3$suffix --list-provers | grep -q Alt-Ergo || return 0
pgm="bin/why3prove$suffix"
test -d $1 || exit 1
for f in $1/*.mlw; do
......
......@@ -3,7 +3,7 @@
set -e
autoconf && (automake --add-missing 2> /dev/null || true)
docker build -t bench-image-system -f misc/Dockerfile.init .
docker build -t bench-image-system-stable -f misc/Dockerfile.init .
IMAGE=$CI_REGISTRY_IMAGE:$(echo $CI_COMMIT_REF_NAME | tr -cs "[:alnum:].\n" "-")
docker build -t $IMAGE -f misc/Dockerfile.deploy .
docker login -u $CI_REGISTRY_USER -p $CI_REGISTRY_PASSWORD $CI_REGISTRY
......
......@@ -6,6 +6,10 @@ if test -z "$DEBIAN_VERSION"; then
DEBIAN_VERSION="stable"
fi
if test -z "$COMPILER"; then
COMPILER="system"
fi
autoconf && (automake --add-missing 2> /dev/null || true)
IMAGE=bench-image-$COMPILER-$DEBIAN_VERSION
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment