Skip to content
Snippets Groups Projects
Commit daf735d6 authored by BRUN Lelio's avatar BRUN Lelio Committed by GARION Christophe
Browse files

remove frama-c from optional dependencies

parent 9a8649cc
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 ...@@ -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 homepage"), the OCaml package manager. We suppose here that opam
version `2.1` is used. 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 ```sh
opam switch create --no-install . 4.14.1 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 ...@@ -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. "Link to Frama-C homepage") and SMT solvers.
LustreC use custom strategies for the Frama-C WP plugin that must be LustreC use custom strategies for the Frama-C WP plugin that must be
installed. Go to the `lustrec_wp_strategies` directory and execute the installed.
following commands:
```sh ```sh
opam install . opam install lustrec_wp_strategies/
``` ```
Frama-C should also be installed. Notice that if you have installed a 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: ...@@ -63,14 +62,12 @@ When starting Frama-C, you should now see the following message:
You may uninstall the plugin by executing You may uninstall the plugin by executing
```sh ```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 The [Alt-Ergo](https://alt-ergo.ocamlpro.com/ "Link to Alt-Ergo homepage") SMT
homepage") is installed with Frama-C. We also recommend to use two solver is installed with Frama-C. We also recommend to use two others solvers:
others SMT solvers:
* [Z3](https://github.com/Z3Prover/z3 "Link to Z3 Github page"), that * [Z3](https://github.com/Z3Prover/z3 "Link to Z3 Github page"), that
can be installed through opam with `opam install z3` (or through can be installed through opam with `opam install z3` (or through
......
...@@ -44,11 +44,7 @@ ...@@ -44,11 +44,7 @@
yojson yojson
ppx_deriving_yojson ppx_deriving_yojson
dune-site dune-site
(re :with-test) (conf-mpfr :with-test)
(yojson :with-test) (conf-cmake :with-test)
(conf-mpfr :with-test) (conf-openjdk :with-test)
(conf-cmake :with-test) (conf-python-2-7 :with-test)))
(conf-openjdk :with-test)
(conf-python-2-7 :with-test))
(depopts
frama-c))
...@@ -33,7 +33,6 @@ depends: [ ...@@ -33,7 +33,6 @@ depends: [
"conf-python-2-7" {with-test} "conf-python-2-7" {with-test}
"odoc" {with-doc} "odoc" {with-doc}
] ]
depopts: ["frama-c"]
build: [ build: [
["dune" "subst"] {dev} ["dune" "subst"] {dev}
[ [
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment