From ca93e2f0be92a023abc902384cd5c6b4aba88c28 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 7 Oct 2020 15:45:04 +0200
Subject: [PATCH] [wp] fix why3 config in gitlab-ci
---
devel_tools/docker/frama-c.dev/Dockerfile | 2 +-
nix/default.nix | 8 +++-----
2 files changed, 4 insertions(+), 6 deletions(-)
diff --git a/devel_tools/docker/frama-c.dev/Dockerfile b/devel_tools/docker/frama-c.dev/Dockerfile
index 564d7180755..22961c32a9b 100644
--- a/devel_tools/docker/frama-c.dev/Dockerfile
+++ b/devel_tools/docker/frama-c.dev/Dockerfile
@@ -33,7 +33,7 @@ RUN apt-get update && opam update -y && opam depext --install -y --verbose \
zmq.5.1.3 \
&& rm -rf /var/lib/apt/lists/*
-RUN why3 config --full-config
+RUN why3 config --detect
# with_source: keep Frama-C sources
ARG with_source=no
diff --git a/nix/default.nix b/nix/default.nix
index 230879d9bfa..39ca3878ecc 100644
--- a/nix/default.nix
+++ b/nix/default.nix
@@ -159,7 +159,7 @@ rec {
wp-qualif = mk_deriv {
name = "frama-c-wp-qualif";
- buildInputs = mk_buildInputs { opamPackages = []; };
+ buildInputs = mk_buildInputs { };
build_dir = main.build_dir;
src = main.build_dir + "/dir.tar";
sourceRoot = ".";
@@ -187,9 +187,7 @@ rec {
aorai-prove = mk_deriv {
name = "frama-c-aorai-prove";
- buildInputs = mk_buildInputs { opamPackages = [
- { name = "alt-ergo"; constraint = "=2.0.0"; }
- ]; };
+ buildInputs = mk_buildInputs { };
build_dir = main.build_dir;
src = main.build_dir + "/dir.tar";
sourceRoot = ".";
@@ -205,7 +203,7 @@ rec {
make create_share_link
mkdir home
HOME=$(pwd)/home
- why3 config --full-config
+ why3 config --detect
make src/plugins/aorai/tests/ptests_config
make PTESTS_OPTS="-config prove -error-code" Aorai_TESTS
'';
--
GitLab