diff --git a/README.md b/README.md index d5bd52566e798aa9c6191b229843c0aa06027e6b..531387289f44ff77b97078ef513bed00d2e4f403 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 085469555677cdb0afdd742e6f946a6c58ae1d26..d384210db5f05a4ea79478d7f21c35800c9862dc 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 bef2b9073c80aad3434fe5713de9990bfc2bb83d..c264add1780fb5b706cf5866ff0eafa3130af4ae 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} [