Merge remote-tracking branch 'origin/stable/iron'

opam

@@ -62,6 +62,7 @@ authors: [
   "Virgile Robles"
   "Muriel Roger"
   "Julien Signoles"
+  "Nicolas Stouls"
   "Kostyantyn Vorobyov"
   "Boris Yakobowski"
 ]
@@ -102,45 +103,53 @@ remove: [
 
 run-test: [
   ["dune" "exec" "--" "frama-c-ptests" "tests" "src/plugins/*/tests"
-  ] { arch != "ppc64" & arch != "x86_32" & arch != "arm32" }
+  ] { arch != "ppc64" & arch != "x86_32" & arch != "arm32" & os != "macos" }
   ["dune" "build" "-j%{jobs}%" "@ptests_config"
-  ] { arch != "ppc64" & arch != "x86_32" & arch != "arm32" }
+  ] { arch != "ppc64" & arch != "x86_32" & arch != "arm32" & os != "macos" }
 ]
 
-# Please keep depends and depopts sorted by package name
 depends: [
   "dune" { (>= "3.2.0" & os!="macos") | (>= "3.5.0" & os="macos") }
   "dune-configurator"
   "dune-private-libs"
   "dune-site"
-  ( ( "lablgtk" { >= "2.18.8" } & "conf-gnomecanvas" & "conf-gtksourceview"
-      & ("ocamlgraph" { < "2.0" } | "ocamlgraph_gtk" ))
-    | ( "lablgtk3" { >= "3.1.0" & os!="macos" }
-        & "lablgtk3-sourceview3" & "conf-gtksourceview3" ) )
+
   ( "alt-ergo-free" | "alt-ergo" )
   "conf-graphviz" { post }
   "conf-time" { with-test }
-  "ppx_deriving_yojson"
   "ocaml" { >= "4.11.1" }
   "ocamlfind" # needed beyond build stage, used by -load-module
   "ocamlgraph" { >= "1.8.8" }
   "why3" { >= "1.5.1" }
   "yojson" { >= "1.6.0" & < "2.0.0" }
   "zarith" { >= "1.5" }
+
+  # PPXs
   "ppx_deriving"
+  "ppx_deriving_yojson"
   "ppx_import"
+
+  # GTK3 for non-macos only
+  "lablgtk3" { >= "3.1.0" & os!="macos" }
+  "lablgtk3-sourceview3" { os!="macos" }
+  "conf-gtksourceview3" { os!="macos" }
 ]
 
+# Note: do not put particular versions here, if some version is *incompatible*,
+# use the field 'conflicts'.
 depopts: [
-  # cannot use {build}: Frama-C must be recompiled when Coq and libraries changes.
-  # Coq: because .vo would would not be loadable by another version of Coq
-  # libraries: because we use dynamic linking
   "apron"
-  "coq"
-  "mlmpfr" { >= "4.1.0-bugfix2"}
+  "mlmpfr"
   "zmq"
 ]
 
+conflicts: [
+  "cairo2" { < "0.6.2" }
+  "mlmpfr" { < "4.1.0-bugfix2" }
+  "pilat"  { <= "1.6" }
+  "result" { < "1.5" }
+]
+
 post-messages: [
 "The Frama-C/WP plug-in requires one or more external prover(s).
 Recommended provers are:
@@ -148,12 +157,12 @@ Recommended provers are:
 - CVC4     (https://cvc4.github.io)
 - Z3       (https://github.com/Z3Prover/z3)
 Use 'why3 config detect' to configure new provers.
- "
+ " { success }
 "Ivette is a new GUI for Frama-C, currently in development.
 Run 'ivette' once to finalize installation (requires an internet connection).
 Once finalized, 'ivette' will work offline.
 Finalization also requires Node v16 and Yarn:
 - install NVM (https://github.com/nvm-sh/nvm)
 - run 'nvm use 16'
-- run 'npm install --global yarn'"
+- run 'npm install --global yarn'" { success }
 ]

src/plugins/gui/help_manager.ml

@@ -65,6 +65,7 @@ let show main_ui =
     "Virgile Robles";
     "Muriel Roger";
     "Julien Signoles";
+    "Nicolas Stouls";
     "Kostyantyn Vorobyov";
     "Boris Yakobowski"
   ]