From daf735d67c197b393a0d1107a71aa7481aaaf23f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lb@leliobrun.net>
Date: Thu, 2 Mar 2023 16:29:40 +0900
Subject: [PATCH] remove frama-c from optional dependencies

---
 README.md    | 15 ++++++---------
 dune-project | 12 ++++--------
 lustrec.opam |  1 -
 3 files changed, 10 insertions(+), 18 deletions(-)

diff --git a/README.md b/README.md
index d5bd5256..53138728 100644
--- a/README.md
+++ b/README.md
@@ -15,7 +15,7 @@ The easiest is to use [opam](https://opam.ocaml.org/ "Link to opam
 homepage"), the OCaml package manager. We suppose here that opam
 version `2.1` is used.
 
-### 1. Set a (local) opam switch using OCaml 4.14.1
+### 1. Set a (local) opam switch using OCaml ≥ 4.11.1
 
 ```sh
 opam switch create --no-install . 4.14.1
@@ -44,11 +44,10 @@ generated C code, you will need [Frama-C](https://www.frama-c.com
 "Link to Frama-C homepage") and SMT solvers.
 
 LustreC use custom strategies for the Frama-C WP plugin that must be
-installed. Go to the `lustrec_wp_strategies` directory and execute the
-following commands:
+installed. 
 
 ```sh
-opam install .
+opam install lustrec_wp_strategies/
 ```
 
 Frama-C should also be installed. Notice that if you have installed a
@@ -63,14 +62,12 @@ When starting Frama-C, you should now see the following message:
 You may uninstall the plugin by executing
 
 ```sh
-opam uninstall .
+opam uninstall lustrec_wp_strategies
 ```
 
-in the `lustrec_wp_strategies` directory.
 
-The [Alt-Ergo](https://alt-ergo.ocamlpro.com/ "Link to Alt-Ergo
-homepage") is installed with Frama-C. We also recommend to use two
-others SMT solvers:
+The [Alt-Ergo](https://alt-ergo.ocamlpro.com/ "Link to Alt-Ergo homepage") SMT
+solver is installed with Frama-C. We also recommend to use two others solvers:
 
 * [Z3](https://github.com/Z3Prover/z3 "Link to Z3 Github page"), that
   can be installed through opam with `opam install z3` (or through
diff --git a/dune-project b/dune-project
index 08546955..d384210d 100644
--- a/dune-project
+++ b/dune-project
@@ -44,11 +44,7 @@
    yojson
    ppx_deriving_yojson
    dune-site
-  (re :with-test)
-  (yojson :with-test)
-  (conf-mpfr :with-test)
-  (conf-cmake :with-test)
-  (conf-openjdk :with-test)
-  (conf-python-2-7 :with-test))
- (depopts
-   frama-c))
+   (conf-mpfr :with-test)
+   (conf-cmake :with-test)
+   (conf-openjdk :with-test)
+   (conf-python-2-7 :with-test)))
diff --git a/lustrec.opam b/lustrec.opam
index bef2b907..c264add1 100644
--- a/lustrec.opam
+++ b/lustrec.opam
@@ -33,7 +33,6 @@ depends: [
   "conf-python-2-7" {with-test}
   "odoc" {with-doc}
 ]
-depopts: ["frama-c"]
 build: [
   ["dune" "subst"] {dev}
   [
-- 
GitLab