Commit 85faa980 authored by Quentin Garchery's avatar Quentin Garchery

Merge branch 'master' into certif

parents 188b964d 7127f577

Too many changes to show.

To preserve performance only 1000 of 1000+ files are displayed.

......@@ -21,6 +21,7 @@ why3.conf
.*.aux
*.elc
*.summary
.merlin
\#*\#
# /
......@@ -29,7 +30,6 @@ why3.conf
/autom4te.cache
/Makefile
/configure
/install-sh
/semantic.cache
/TAGS
/output_why3
......@@ -38,8 +38,8 @@ why3.conf
/distrib
/why3regtests.err
/why3regtests.out
/.merlin
/src/jessie/.merlin
/_build
# /bench/
/bench/programs/good/booleans/
......@@ -83,6 +83,9 @@ why3.conf
/bin/why3replay.byte
/bin/why3replay.opt
/bin/why3replay
/bin/why3pp.opt
/bin/why3pp.byte
/bin/why3pp
/bin/why3session.opt
/bin/why3session.byte
/bin/why3session
......@@ -95,6 +98,9 @@ why3.conf
/bin/why3webserver.opt
/bin/why3webserver.byte
/bin/why3webserver
/bin/why3pp.opt
/bin/why3pp.byte
/bin/why3pp
/bin/isabelle_client.opt
/bin/isabelle_client.byte
/bin/isabelle_client
......@@ -211,6 +217,8 @@ pvsbin/
/src/util/json_parser.mli
/src/util/json_parser.ml
/src/util/json_parser.conflicts
/src/util/mlmpfr_wrapper.ml
/src/util/ppx_debug_optim
# /src/session
/src/session/xml.ml
......
stages:
- docker
- build
- test
- nightly
- deploy
variables:
BUILD_IMAGE: "$CI_REGISTRY_IMAGE:ci-master-2019-11-14"
GIT_CLEAN_FLAGS: "-ffdxq"
build-image:
stage: docker
script:
- docker login -u "$CI_REGISTRY_USER" -p "$CI_JOB_TOKEN" "$CI_REGISTRY"
- if docker pull "$BUILD_IMAGE"; then echo "Image already exists!"; exit 1; fi
- docker build --force-rm -t "$BUILD_IMAGE" - < misc/Dockerfile.build
- docker push "$BUILD_IMAGE"
- docker rmi "$BUILD_IMAGE"
only:
variables:
- $NEW_BUILD_IMAGE
tags:
- shell
.docker_template: &docker_definition
image: "$BUILD_IMAGE"
tags:
- docker
.build_template: &build_definition
stage: build
script:
- misc/ci-docker.sh misc/ci-local.sh
- misc/ci-local.sh
<<: *docker_definition
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
<<: *build_definition
build-4.04.2:
variables:
COMPILER: 4.04.2
COMPILER: ocaml-system
<<: *build_definition
build-4.05.0:
......@@ -44,10 +54,21 @@ build-4.07.1:
COMPILER: 4.07.1
<<: *build_definition
build-4.08.1:
variables:
COMPILER: 4.08.1
<<: *build_definition
build-4.09.0:
variables:
COMPILER: 4.09.0
<<: *build_definition
.bench_template1: &bench_definition_always
stage: test
script:
- misc/ci-docker.sh misc/ci-local.sh bench ide
- misc/ci-local.sh bench ide
<<: *docker_definition
.bench_template2: &bench_definition
<<: *bench_definition_always
......@@ -58,21 +79,6 @@ build-4.07.1:
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
<<: *bench_definition
bench-4.04.2:
variables:
COMPILER: 4.04.2
<<: *bench_definition
bench-4.05.0:
variables:
COMPILER: 4.05.0
......@@ -88,45 +94,59 @@ bench-4.07.1:
COMPILER: 4.07.1
<<: *bench_definition_always
full-4.07.1:
bench-4.08.1:
variables:
COMPILER: 4.08.1
<<: *bench_definition
bench-4.09.0:
variables:
COMPILER: 4.09.0
<<: *bench_definition
full:
stage: test
variables:
COMPILER: 4.07.1
DEBIAN_PACKAGES: hevea rubber texlive-latex-extra lmodern texlive-fonts-recommended
OPAM_PACKAGES: coq-flocq.3.1.0 js_of_ocaml-ppx alt-ergo.2.0.0
COMPILER: full
script:
- misc/ci-docker.sh misc/ci-local.sh bench ide doc web_ide
- misc/ci-local.sh ide doc web_ide bench
<<: *docker_definition
nightly-bench:
stage: nightly
variables:
COMPILER: 4.05.0
DEBIAN_PACKAGES: cvc3 spass
OPAM_PACKAGES: alt-ergo.2.0.0 zenon.0.8.0 coq.8.7.2 coq-flocq.3.1.0
COMPILER: bench
script:
- misc/ci-docker.sh misc/ci-local.sh nightly-bench-reduced
- misc/ci-local.sh nightly-bench-reduced
<<: *docker_definition
ce-bench:
stage: nightly
variables:
COMPILER: 4.05.0
DEBIAN_PACKAGES: cvc3 spass
OPAM_PACKAGES: alt-ergo.2.0.0 zenon.0.8.0 coq.8.7.2 coq-flocq.3.1.0
COMPILER: bench
script:
- misc/ci-docker.sh misc/ci-local.sh ce-bench
- misc/ci-local.sh ce-bench
<<: *docker_definition
opam:
stage: build
variables:
COMPILER: system
script:
- misc/ci-docker.sh misc/ci-opam.sh
- opam pin -v -y add why3 .
- opam pin -v -y add why3-ide .
<<: *docker_definition
deploy:
stage: deploy
script:
- misc/ci-deploy.sh
- IMAGE=$CI_REGISTRY_IMAGE:$(echo $CI_COMMIT_REF_NAME | tr -cs "[:alnum:].\n" "-")
- docker login -u "$CI_REGISTRY_USER" -p "$CI_JOB_TOKEN" "$CI_REGISTRY"
- docker pull "$IMAGE" || true
- docker build --force-rm --cache-from "$IMAGE" -t "$IMAGE" -f misc/Dockerfile.deploy .
- docker push "$IMAGE"
- docker rmi "$IMAGE"
only:
- master
- /^bugfix[/]v[0-9.]*$/
- tags
tags:
- shell
Léo Andrès <leo@ndrs.fr>
Benedikt Becker <benedikt.becker@inria.fr>
Cláudio Belo Lourenço <belolourenco@gmail.com> <claudio-filipe.belo-da-silva-lourenco@inria.fr>
François Bobot <francois@bobot.eu> <bobot@lri.fr>
François Bobot <francois@bobot.eu> <francois.bobot@cea.fr>
Martin Clochard <martin.clochard@lri.fr> <martin@pc-stagiaire.(none)>
Martin Clochard <martin.clochard@lri.fr> <clochard@MC-MacBook.(none)>
Sylvain Dailler <dailler@adacore.com>
Sylvain Dailler <dailler@adacore.com> <sdailler@hauzar@adacore.com>
Sylvain Dailler <dailler@adacore.com> <sylvain.dailler@inria.fr>
Sylvain Dailler <dailler@adacore.com> <dailler@moloch.lri.fr>
Diego Diverio <diego.diverio@inria.fr>
Jean-Christophe Filliâtre <jean-christophe.filliatre@lri.fr> <Jean-Christophe.Filliatre@lri.fr>
Jean-Christophe Filliâtre <jean-christophe.filliatre@lri.fr> <filliatr@lri.fr>
Jean-Christophe Filliâtre <jean-christophe.filliatre@lri.fr> <jc@evariste.(none)>
......@@ -20,12 +24,14 @@ Léon Gondelman <gondelmans@lri.fr> <lgondelman@lg-PC.(none)>
Léon Gondelman <gondelmans@lri.fr> <leon@ubuntu.(none)>
David Hauzar <david.hauzar@inria.fr> <hauzar@moloch.lri.fr>
Johannes Kanig <kanig@adacore.com> <johannes.kanig@lri.fr>
Rehan Malak <rehan.malak@inria.fr>
Claude Marché <claude.marche@inria.fr> <Claude.Marche@inria.fr>
Claude Marché <claude.marche@inria.fr> <cmarche@dispater.(none)>
Claude Marché <claude.marche@inria.fr> <cmarche@orcus.(none)>
Claude Marché <claude.marche@inria.fr> <cmarche@belzebuth.(none)>
Guillaume Melquiond <guillaume.melquiond@inria.fr>
Guillaume Melquiond <guillaume.melquiond@inria.fr> <melquion@moloch.saclay.inria.fr>
David Mentré <dmentre@linux-france.org>
Kim Nguyễn <kim.nguyen@lri.fr> <kn@lri.fr>
Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <nguyen@lri.fr>
Thi-Minh-Tuyen Nguyen <thi-minh-tuyen.nguyen@inria.fr> <nguyen@acces.lri.fr>
......