From 3d6402443baf6887c3acf68426bb193773371b06 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Mon, 8 Jul 2019 19:14:23 +0200
Subject: [PATCH] [opam] add why3 as mandatory dependence
---
INSTALL.md | 3 +--
opam/opam | 4 +---
2 files changed, 2 insertions(+), 5 deletions(-)
diff --git a/INSTALL.md b/INSTALL.md
index 7c8de3fe757..fd85b7bfcb4 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -82,7 +82,7 @@ Frama-C 19 (Potassium):
- lablgtk.2.18.5 | lablgtk3.3.0.beta5 + lablgtk3-sourceview3.3.0.beta5
- mlgmpidl.1.2.9 (optional)
- ocamlgraph.1.8.8
-- why3.1.2.0 (optional)
+- why3.1.2.0
- why3-coq.1.2.0 (optional)
- yojson.1.4.1
- zarith.1.7
@@ -225,7 +225,6 @@ We recommend to rely on it for the installation of Frama-C.
```shell
brew install graphviz
- opam install why3
```
5. Install *optional* dependencies for Frama-C/WP:
diff --git a/opam/opam b/opam/opam
index 3b6424cf61d..b430aac839e 100644
--- a/opam/opam
+++ b/opam/opam
@@ -97,6 +97,7 @@ depends: [
( "alt-ergo-free" | "alt-ergo" )
"conf-graphviz" { post }
"yojson"
+ "why3"
]
depopts: [
@@ -104,7 +105,6 @@ depopts: [
# Coq: because .vo would would not be loadable by another version of Coq
# libraries: because we use dynamic linking
"coq"
- "why3"
"why3-coq"
"mlgmpidl"
"apron"
@@ -121,8 +121,6 @@ conflicts: [
]
messages: [
- "Why3 can be used by the WP plug-in for running additional automatic solvers"
- {!why3:installed}
"Coq can be used with the WP plug-in for proving interactively proof obligations"
{!coq:installed}
"Alt-Ergo Graphical Interface can be used by the WP plug-in"
--
GitLab