Skip to content
Snippets Groups Projects
Commit 011d66e3 authored by BRUN Lelio's avatar BRUN Lelio
Browse files

remove frama-c from optional dependencies

parent e7729134
No related branches found
No related tags found
No related merge requests found
......@@ -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
......
......@@ -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)))
......@@ -31,7 +31,6 @@ depends: [
"conf-python-2-7" {with-test}
"odoc" {with-doc}
]
depopts: ["frama-c"]
build: [
["dune" "subst"] {dev}
[
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment