diff --git a/README.md b/README.md index 61273f5746a0b9ba229d672b040c91989af13bd7..7a49100adaf8a058ee8bcc493cde84d5516e41ba 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 4e676af6fa3e71fb48eee96f9ada313257a18fb3..d32d3d331bd3a0c8279a42d99d1d1c699ff635dc 100644 --- a/dune-project +++ b/dune-project @@ -46,6 +46,4 @@ (conf-mpfr :with-test) (conf-cmake :with-test) (conf-openjdk :with-test) - (conf-python-2-7 :with-test)) - (depopts - frama-c)) + (conf-python-2-7 :with-test))) diff --git a/lustrec.opam b/lustrec.opam index 35f2bafe5513396ea3df99784233e857329b816f..e0d75a51e8794ccdd960e1a573d69f23f33118ff 100644 --- a/lustrec.opam +++ b/lustrec.opam @@ -31,7 +31,6 @@ depends: [ "conf-python-2-7" {with-test} "odoc" {with-doc} ] -depopts: ["frama-c"] build: [ ["dune" "subst"] {dev} [