[wp_strategies] generate opam file to ease install

README.md

@@ -43,16 +43,30 @@ If you want to generate ACSL specifications and prove them on the
 generated C code, you will need [Frama-C](https://www.frama-c.com
 "Link to Frama-C homepage") and SMT solvers.
 
-First, install Frama-C through opam (we are currently using version
-26.1 `Iron` of Frama-C):
+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:
+
+```sh
+opam install .
+```
+
+Frama-C should also be installed. Notice that if you have installed a
+local Opam switch, Frama-C should be installed in this local switch.
+
+When starting Frama-C, you should now see the following message:
 
 ```sh
-opam install frama-c
+[lustrec-wp-strategies] LustreC WP strategies available.
+```
+
+You may uninstall the plugin by executing
 
+```sh
+opam uninstall .
 ```
 
-Notice that if you have installed a local Opam switch, Frama-C should
-be installed in this local switch.
+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
@@ -73,29 +87,6 @@ used by Frama-C for deductive verification:
 why3 config detect
 ```
 
-LustreC use custom strategies for the Frama-C WP plugin that must be
-compiled (TODO: add detail here). Go to the `lustrec_wp_strategies`
-directory and execute the following commands:
-
-```sh
-dune build @install
-dune install
-```
-
-When starting Frama-C, you should now see the following message:
-
-```sh
-[lustrec-wp-strategies] LustreC WP strategies available.
-```
-
-You may uninstall the plugin by executing
-
-```sh
-dune uninstall
-```
-
-in the `lustrec_wp_strategies` directory.
-
 ## Usage
 
 To see a summary of options:

lustrec_wp_strategies/dune-project

 (lang dune 3.2)
 (using dune_site 0.1)
 
+(generate_opam_files true)
+
 (name frama-c-lustrec-wp-strategies)
-(maintainers "Lélio Brun, Christophe Garion, Pierre-Loïc Garoche, Xavier Thirioux")
+
+(license LGPL-3.0-or-later)
+
+(authors "Lélio Brun <lb@leliobrun.net>"
+         "Pierre-Loic Garoche <ploc@garoche.net>"
+         "Xavier Thirioux <xavier.thirioux@isae-supaero.fr>"
+)
+
+(maintainers "Pierre-Loic Garoche <ploc@garoche.net>"
+             "Xavier Thirioux <xavier.thirioux@isae-supaero.fr>"
+)
+
+(source (uri git+https://gitlab.isae-supaero.fr/lustrec/lustrec.git))
+(bug_reports https://gitlab.isae-supaero.fr/lustrec/lustrec/-/issues)
+(homepage https://gitlab.isae-supaero.fr/lustrec/lustrec)
 
 (package (name frama-c-lustrec-wp-strategies)
+ (synopsis "Strategies to be used with Frama-C WP plugin")
+ (description
+   "This package defines custom strategies to be used with Frama-C WP
+   plugin. They are mainly used to prove ACSL statements generated by
+   LustreC, particularly to unfold complex predicate definitions and
+   to more easily find witnesses for existential quantifiers.")
  (depends
   ("frama-c" (>= 26.1))
  )

lustrec_wp_strategies/frama-c-lustrec-wp-strategies.opam

+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "Strategies to be used with Frama-C WP plugin"
+description: """
+This package defines custom strategies to be used with Frama-C WP
+   plugin. They are mainly used to prove ACSL statements generated by
+   LustreC, particularly to unfold complex predicate definitions and
+   to more easily find witnesses for existential quantifiers."""
+maintainer: [
+  "Pierre-Loic Garoche <ploc@garoche.net>"
+  "Xavier Thirioux <xavier.thirioux@isae-supaero.fr>"
+]
+authors: [
+  "Lélio Brun <lb@leliobrun.net>"
+  "Pierre-Loic Garoche <ploc@garoche.net>"
+  "Xavier Thirioux <xavier.thirioux@isae-supaero.fr>"
+]
+license: "LGPL-3.0-or-later"
+tags: ["Frama-C LustreC WP strategies"]
+homepage: "https://gitlab.isae-supaero.fr/lustrec/lustrec"
+bug-reports: "https://gitlab.isae-supaero.fr/lustrec/lustrec/-/issues"
+depends: [
+  "dune" {>= "3.2"}
+  "frama-c" {>= "26.1"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "--promote-install-files=false"
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+  ["dune" "install" "-p" name "--create-install-files" name]
+]
+dev-repo: "git+https://gitlab.isae-supaero.fr/lustrec/lustrec.git"