Merge branch '538-wp-support-for-why-3-1-0' into 'stable/potassium'

Resolve "[WP] Support for Why-3 1.0"

See merge request frama-c/frama-c!2239

INSTALL.md

@@ -81,19 +81,17 @@ The following set of packages is known to be a working configuration for
 Frama-C 18 (Argon):
 
 - OCaml 4.05.0
-- alt-ergo.1.30 or, under a non-commercial license, alt-ergo.2.0.0 (pin recommended)
+- alt-ergo-free.2.0.0 (optional)
 - apron.20160125 (optional)
-- coq.8.7.2 (optional; pin recommended)
+- coq.8.9.0 (optional)
 - lablgtk.2.18.5
 - mlgmpidl.1.2.7 (optional)
 - ocamlgraph.1.8.8
-- why3.0.88.3
+- why3.1.2.0 (optional)
+- why3-coq.1.2.0 (optional)
 - yojson.1.4.1
 - zarith.1.7
 
-Note: *pin recommended* indicates packages likely to become incompatible in
-      future releases; `opam pin` is recommended to prevent them from breaking.
-
 ### Installing Custom Versions of Frama-C via opam
 
 If you have a **non-standard** version of Frama-C available
@@ -176,7 +174,7 @@ We recommend to rely on it for the installation of Frama-C.
 4. Install *optional* dependencies for Frama-C/WP:
 
     ```shell
-    opam install coq coqide
+    opam install coq coqide why3-coq
     ```
 
 5. Install Frama-C:

headers/close-source/MODIFIED_WHY3

 
 The Why3 Verification Platform   /   The Why3 Development Team
-Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University
+Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University
 
 This software is distributed under the terms of the GNU Lesser
 General Public License version 2.1, with the special exception

headers/close-source/UNMODIFIED_WHY3

 
 The Why3 Verification Platform   /   The Why3 Development Team
-Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University
+Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University
 
 This software is distributed under the terms of the GNU Lesser
 General Public License version 2.1, with the special exception
 on linking described in file LICENSE.
+

headers/header_spec.txt

@@ -1430,6 +1430,10 @@ src/plugins/wp/ProofScript.ml: CEA_WP
 src/plugins/wp/ProofScript.mli: CEA_WP
 src/plugins/wp/ProverCoq.ml: CEA_WP
 src/plugins/wp/ProverCoq.mli: CEA_WP
+src/plugins/wp/ProverDetect.ml: CEA_WP
+src/plugins/wp/ProverDetect.mli: CEA_WP
+src/plugins/wp/ProverDetect.Why3.ml: CEA_WP
+src/plugins/wp/ProverDetect.None.ml: CEA_WP
 src/plugins/wp/ProverErgo.ml: CEA_WP
 src/plugins/wp/ProverErgo.mli: CEA_WP
 src/plugins/wp/ProverScript.ml: CEA_WP
@@ -1799,6 +1803,7 @@ src/plugins/wp/share/coqwp/Cfloat.v: CEA_WP
 src/plugins/wp/share/coqwp/Cint.v: CEA_WP
 src/plugins/wp/share/coqwp/Cmath.v: CEA_WP
 src/plugins/wp/share/coqwp/ExpLog.v: CEA_WP
+src/plugins/wp/share/coqwp/HighOrd.v: UNMODIFIED_WHY3
 src/plugins/wp/share/coqwp/Memory.v: CEA_WP
 src/plugins/wp/share/coqwp/Qed.v: CEA_WP
 src/plugins/wp/share/coqwp/Qedlib.v: CEA_WP
@@ -1809,8 +1814,10 @@ src/plugins/wp/share/coqwp/Zbits.v: CEA_WP
 src/plugins/wp/share/coqwp/bool/Bool.v: UNMODIFIED_WHY3
 src/plugins/wp/share/coqwp/int/Abs.v: UNMODIFIED_WHY3
 src/plugins/wp/share/coqwp/int/ComputerDivision.v: UNMODIFIED_WHY3
+src/plugins/wp/share/coqwp/int/Exponentiation.v: UNMODIFIED_WHY3
 src/plugins/wp/share/coqwp/int/Int.v: UNMODIFIED_WHY3
 src/plugins/wp/share/coqwp/int/MinMax.v: UNMODIFIED_WHY3
+src/plugins/wp/share/coqwp/int/Power.v: UNMODIFIED_WHY3
 src/plugins/wp/share/coqwp/map/Map.v: UNMODIFIED_WHY3
 src/plugins/wp/share/coqwp/map/Const.v: UNMODIFIED_WHY3
 src/plugins/wp/share/coqwp/real/Abs.v: UNMODIFIED_WHY3

headers/open-source/MODIFIED_WHY3

 
 The Why3 Verification Platform   /   The Why3 Development Team
-Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University
+Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University
 
 This software is distributed under the terms of the GNU Lesser
 General Public License version 2.1, with the special exception

headers/open-source/UNMODIFIED_WHY3

 
 The Why3 Verification Platform   /   The Why3 Development Team
-Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University
+Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University
 
 This software is distributed under the terms of the GNU Lesser
 General Public License version 2.1, with the special exception
 on linking described in file LICENSE.
+

nix/default.nix

@@ -150,7 +150,7 @@ rec {
         name = "frama-c-wp-qualif";
         buildInputs = mk_buildInputs { opamPackages = [
                     { name = "alt-ergo"; constraint = "=2.0.0"; }
-                    { name = "why3" ; constraint = "=0.88.3"; }
+                    { name = "why3" ; constraint = "=1.1.1"; }
                ]; };
         build_dir = main.build_dir;
         src = main.build_dir + "/dir.tar";

opam/opam

@@ -100,14 +100,14 @@ depends: [
 depopts: [
   "coq" { build }
   "why3" { build }
+  "why3-coq" { build }
   "mlgmpidl" { build }
   "apron" { build }
 ]
 
 conflicts: [
-  "why3-base" { < "0.88" } #for WP plug-in
-  "why3"      { >= "1.0.0" } #for WP plug-in
-  "coq"      { < "8.4.6" } #for WP plug-in
+  "why3-base" #for WP plug-in
+  "why3" { < "1.0.0" } #for WP plug-in
   "lablgtk" { < "2.18.2" } #for ocaml >= 4.02.1
   "frama-c-e-acsl" #avoid mixing old releases of E-ACSL, it is already
                    #distributed with this version of Frama-C

src/plugins/wp/.gitignore

@@ -3,12 +3,13 @@
 /.make-wp-why3
 
 /Wp.mli
+/gui/Wp.mli
 /.WP_API_GENERATED
 /driver.ml
 /rformat.ml
 /script.ml
 /why3_xml.ml
-/gui/Wp.mli
+/ProverDetect.ml
 
 /tests/ptests_config
 /tests/*/result

src/plugins/wp/Changelog

@@ -20,15 +20,15 @@
 #   <Prover>: prover
 ###############################################################################
 
--  Wp         [2019/28/01] Now -wp-dynamic is set by default (annotation @calls)
-
- -  Wp         [2019/01/28] New floating-point model
- - WP          [2019/02/05] Auto filter properties with name "no_wp:"
- - Wp          [2019/01/28] New floating-point model
+ - Wp          [2019/04/24] Support for Why3 1.* and Coq 8.{7-9}
+ - Wp          [2019/02/26] Support for @check ACSL annotations
  - WP          [2018/02/16] Filter out some variables from separation
  - TIP         [2018/02/15] Extend bitwise-eq auto-strategy on hypotheses
  - TIP         [2018/02/15] Fix wrong reconciliation of sub-scripts during replay
  - Wp          [2018/02/15] Better naming convention, consistent with report-classify
+ - WP          [2019/02/05] Auto filter properties with name "no_wp:"
+ - Wp          [2019/01/28] Now -wp-dynamic is set by default (annotation @calls)
+ - Wp          [2019/01/28] New floating-point model
  - Wp          [2018/01/18] Auto-Search mode, see -wp-auto
  - TIP         [2018/01/18] Auto-Search mode from the GUI
  - TIP         [2018/01/18] New Strategies for bitwise and congruence operations
@@ -38,21 +38,8 @@
  - TIP         [2017/04/25] New tactical Congruence (divisions and products)
  - Qed         [2017/10/30] Extends simplifications for lsl,lsr and div
  - Wp          [2017/10/27] Fix soundness bug when assigning non-valid ranges
- - Qed         [2017/10/27] New simplifications for validirt and ranges
+ - Qed         [2017/10/27] New simplifications for validity and ranges
  - TIP         [2017/10/27] New tacticals for validity and ranges
- - TIP         [2017/04/25] Options -wp-time-{extra|margin} for more stability
- -* Gui        [2017/04/25] Fixed bug when running prover from the TIP
- - Wp          [2017/04/25] Improved model and simplifications of logical shifts
- - Wp          [2017/04/25] New simplification logic functions (-wp-reduce)
- - Wp          [2017/04/25] New simplification of unused variables (-wp-parasite)
- - Wp          [2017/04/25] New simplification for ground terms (-wp-ground)
- - Wp          [2017/04/25] Option -wp-prenex to normalize nested binders
- - Wp          [2017/04/25] Option -wp-overflows to add explicit assumptions
- - TIP         [2017/04/25] New tactical Overflow (to cope with modulus)
- - TIP         [2017/04/25] New tactical Bitwised, BitRange and Shift
- - TIP         [2017/04/25] New tactical Rewrite (two apply equalities)
- - Wp          [2017/03/12] Reduction of equalities with logic functions
- - Wp          [2017/03/12] More simplifications wrt integer domains
 
 ######################
 Plugin WP 18.0 (Argon)

src/plugins/wp/GuiConfig.ml

@@ -20,35 +20,50 @@
 (*                                                                        *)
 (**************************************************************************)
 
-open ProverWhy3
+open VCS
 
 (* ------------------------------------------------------------------------ *)
 (* ---  Prover List in Configuration                                    --- *)
 (* ------------------------------------------------------------------------ *)
 
-class provers config =
+class available () =
   object(self)
-    inherit [dp list] Wutil.selector []
+    val mutable dps = []
+    method get = dps
+    method detect =
+      try dps <- ProverDetect.detect ()
+      with exn ->
+        Wp_parameters.error "Why3 detection error:@\n%s"
+          (Printexc.to_string exn)
+    initializer self#detect
+  end
+
+class enabled key =
+  object(self)
+    inherit [string list] Wutil.selector []
 
     method private load () =
       let open Gtk_helper.Configuration in
       let rec collect w = function
-        | ConfString s -> ProverWhy3.parse s :: w
+        | ConfString s -> s :: w
         | ConfList fs -> List.fold_left collect w fs
         | _ -> w in
       try
-        let data = Gtk_helper.Configuration.find config in
-        self#set (List.rev (collect [] data))
-      with Not_found -> ()
+        let data = Gtk_helper.Configuration.find key in
+        List.rev (collect [] data)
+      with Not_found -> []
 
     method private save () =
       let open Gtk_helper.Configuration in
-      Gtk_helper.Configuration.set config
-        (ConfList (List.map (fun dp -> ConfString dp.dp_prover) self#get))
+      Gtk_helper.Configuration.set key
+        (ConfList (List.map (fun s -> ConfString s) self#get))
 
     initializer
       begin
-        self#load () ;
+        let settings = self#load () in
+        let cmdline = Wp_parameters.Provers.get () in
+        let selection = List.sort_uniq String.compare (settings @ cmdline) in
+        self#set selection ;
         self#on_event self#save ;
       end
 
@@ -60,8 +75,8 @@ class provers config =
 
 class dp_chooser
     ~(main:Design.main_window_extension_points)
-    ~(available:provers)
-    ~(enabled:provers)
+    ~(available:available)
+    ~(enabled:enabled)
   =
   let dialog = new Wpane.dialog
     ~title:"Why3 Provers"
@@ -70,7 +85,7 @@ class dp_chooser
   let array = new Wpane.warray () in
   object(self)
 
-    val mutable provers = []
+    val mutable selected = []
 
     method private enable dp e =
       let rec hook dp e = function
@@ -78,14 +93,14 @@ class dp_chooser
         | head :: tail ->
             if fst head = dp then (dp,e) :: tail
             else head :: hook dp e tail
-      in provers <- hook dp e provers
+      in selected <- hook dp e selected
 
     method private lookup dp =
-      try List.assoc dp provers
+      try List.assoc dp selected
       with Not_found -> false
 
     method private entry dp =
-      let text = Printf.sprintf "%s (%s)" dp.dp_name dp.dp_version in
+      let text = Pretty_utils.to_string VCS.pretty dp in
       let sw = new Widget.switch () in
       let lb = new Widget.label ~align:`Left ~text () in
       sw#set (self#lookup dp) ;
@@ -101,24 +116,30 @@ class dp_chooser
 
     method private configure dps =
       begin
-        available#set dps ;
         array#set dps ;
-        provers <- List.map (fun dp -> dp , self#lookup dp) dps ;
         array#update () ;
       end
 
-    method private detect () = ProverWhy3.detect_provers self#configure
+    method private detect () =
+      begin
+        available#detect ;
+        self#configure available#get ;
+      end
 
-    method private select () =
-      let dps = List.fold_right
-          (fun (dp,e) dps -> if e then dp :: dps else dps)
-          provers []
-      in enabled#set dps
+    method private apply () =
+      let rec choose = function
+        | ({dp_shortcuts=key::_},true)::dps -> key :: choose dps
+        | _::dps -> choose dps
+        | [] -> []
+      in enabled#set (choose selected)
 
     method run () =
-      available#send self#configure () ;
-      List.iter (fun dp -> self#enable dp true) enabled#get ;
-      array#update () ;
+      let dps = available#get in
+      let sel = enabled#get in
+      selected <- List.map
+          (fun dp -> dp,List.exists (fun k -> List.mem k sel) dp.dp_shortcuts)
+          dps ;
+      self#configure dps ;
       dialog#run ()
 
     initializer
@@ -128,7 +149,7 @@ class dp_chooser
         dialog#button ~action:(`APPLY) ~label:"Apply" () ;
         array#set_entry self#entry ;
         dialog#add_block array#coerce ;
-        dialog#on_value `APPLY self#select ;
+        dialog#on_value `APPLY self#apply ;
       end
 
   end
@@ -138,86 +159,63 @@ class dp_chooser
 (* ------------------------------------------------------------------------ *)
 
 type mprover =
-  | NoProver
-  | AltErgo
-  | Coq
-  | Why3ide
-  | Why3 of dp
+  | NONE
+  | ERGO
+  | COQ
+  | WHY of VCS.dp
 
-class dp_button ~(available:provers) ~(enabled:provers) =
+class dp_button ~(available:available) =
   let render = function
-    | NoProver -> "None"
-    | AltErgo -> "Alt-Ergo (native)"
-    | Coq -> "Coq (native,ide)"
-    | Why3ide -> "Why3 (ide)"
-    | Why3 dp -> Printf.sprintf "Why3: %s (%s)" dp.dp_name dp.dp_version
+    | NONE -> "(none)"
+    | ERGO -> "Alt-Ergo (native)"
+    | COQ -> "Coq (native)"
+    | WHY { dp_shortcuts = keys } when List.mem "alt-ergo" keys ->
+        "Alt-Ergo (why3)"
+    | WHY dp -> Pretty_utils.to_string VCS.pretty dp in
+  let select = function
+    | ERGO -> "alt-ergo"
+    | COQ -> "coq"
+    | WHY { dp_shortcuts=[] } | NONE -> "none"
+    | WHY { dp_shortcuts=key::_ } -> "why3:"^key in
+  let rec import = function
+    | [] -> ERGO
+    | spec::others ->
+        match VCS.prover_of_name spec with
+        | None | Some (Why3ide|Qed) -> NONE
+        | Some (AltErgo|Tactical) -> ERGO
+        | Some Coq -> COQ
+        | Some (Why3 s) ->
+            try
+              let dps = available#get in
+              WHY (List.find (fun dp -> List.mem s dp.dp_shortcuts) dps)
+            with Not_found -> import others
   in
-  let items = [ NoProver ; AltErgo ; Coq ; Why3ide ] in
-  let button = new Widget.menu ~default:AltErgo ~render ~items () in
+  let items = [ NONE ; ERGO ; COQ ] in
+  let button = new Widget.menu ~default:ERGO ~render ~items () in
   object(self)
     method coerce = button#coerce
     method widget = (self :> Widget.t)
     method set_enabled = button#set_enabled
     method set_visible = button#set_visible
 
-    method private import =
-      match Wp_parameters.Provers.get () with
-      | [] -> ()
-      | spec :: _ ->
-          match VCS.prover_of_name spec with
-          | Some (VCS.Why3 p) ->
-              let dps = available#get in
-              let dp = ProverWhy3.find p dps in
-              if not (List.mem dp dps) then available#set (dps @ [dp]) ;
-              let en = dp :: enabled#get in
-              enabled#set
-                (List.filter (fun q -> List.mem q en) available#get)
-          | _ -> ()
-
-    method private set_provers dps =
-      button#set_items (items @ List.map (fun dp -> Why3 dp) dps)
-
-    method private get_selection = function
-      | NoProver -> "none"
-      | AltErgo -> "alt-ergo"
-      | Coq -> "coqide"
-      | Why3ide -> "why3ide"
-      | Why3 dp -> "why3:" ^ dp.dp_prover
-
-    method private set_selection = function
-      | [] -> ()
-      | spec :: _ ->
-          match VCS.prover_of_name spec with
-          | None | Some VCS.Qed | Some VCS.Tactical -> button#set NoProver
-          | Some VCS.AltErgo -> button#set AltErgo
-          | Some VCS.Coq -> button#set Coq
-          | Some VCS.Why3ide -> button#set Why3ide
-          | Some (VCS.Why3 spec) ->
-              let dp = ProverWhy3.find spec enabled#get in
-              button#set (Why3 dp)
-
-    val mutable last = []
-    val mutable init = true
+    val mutable dps = []
 
     method update () =
+      (* called in polling mode *)
       begin
-        if init then self#import ;
-        let current = Wp_parameters.Provers.get () in
-        if current <> last then
-          self#set_selection (Wp_parameters.Provers.get ()) ;
-        last <- current ;
-        if init then
+        let avl = available#get in
+        if avl != dps then
           begin
-            self#set_provers enabled#get ;
-            enabled#connect self#set_provers ;
-            init <- false ;
-          end
-      end
-
-    initializer
-      begin
-        button#connect
-          (fun mp -> Wp_parameters.Provers.set [self#get_selection mp]) ;
+            dps <- avl ;
+            let items = [NONE;ERGO] @ List.map (fun p -> WHY p) dps @ [COQ] in
+            button#set_items items
+          end ;
+        let cur = Wp_parameters.Provers.get () |> import in
+        if cur <> button#get then button#set cur ;
       end
 
+    initializer button#connect
+        (fun s -> Wp_parameters.Provers.set [select s])
   end
+
+(* ------------------------------------------------------------------------ *)

src/plugins/wp/GuiConfig.mli

@@ -24,21 +24,25 @@
 (* ---  WP Provers Configuration Panel                                  --- *)
 (* ------------------------------------------------------------------------ *)
 
-open ProverWhy3
+open VCS
 
-class provers : string -> [dp list] Widget.selector
+class available : unit ->
+  object
+    method detect : unit
+    method get : dp list
+  end
+
+class enabled : string -> [string list] Widget.selector
 
 class dp_chooser :
   main:Design.main_window_extension_points ->
-  available:provers ->
-  enabled:provers ->
+  available:available ->
+  enabled:enabled ->
   object
     method run : unit -> unit (** Edit enabled provers *)
   end
 
-class dp_button :
-  available:provers ->
-  enabled:provers ->
+class dp_button : available:available ->
   object
     inherit Widget.widget
     method update : unit -> unit

src/plugins/wp/GuiGoal.ml

@@ -73,7 +73,7 @@ class iformat =
 (* --- Goal Panel                                                         --- *)
 (* -------------------------------------------------------------------------- *)
 
-class pane (proverpane : GuiConfig.provers) =
+class pane (enabled : GuiConfig.enabled) =
   let icon = new Widget.image GuiProver.no_status in
   let status = new Widget.label () in
   let text = new Wtext.text () in
@@ -126,8 +126,8 @@ class pane (proverpane : GuiConfig.provers) =
         provers <-
           VCS.([ new GuiProver.prover ~console:text ~prover:AltErgo ] @
                List.map
-                 (fun dp -> new GuiProver.prover text (ProverWhy3.prover dp))
-                 proverpane#get) ;
+                 (fun dp -> new GuiProver.prover text (Why3 dp))
+                 enabled#get) ;
         List.iter (fun p -> palette#add_tool p#tool) provers ;
         palette#add_tool strategies#tool ;
         Strategy.iter strategies#register ;
@@ -137,11 +137,11 @@ class pane (proverpane : GuiConfig.provers) =
              tactics <- gtac :: tactics ;
              palette#add_tool gtac#tool) ;
         tactics <- List.rev tactics ;
-        self#register_provers proverpane#get ;
+        self#register_provers enabled#get ;
         printer#on_selection (fun () -> self#update) ;
         scripter#on_click self#goto ;
         scripter#on_backtrack self#backtrack ;
-        proverpane#connect self#register_provers ;
+        enabled#connect self#register_provers ;
         delete#connect (fun () -> self#interrupt ProofEngine.reset) ;
         cancel#connect (fun () -> self#interrupt ProofEngine.cancel) ;
         forward#connect (fun () -> self#forward) ;
@@ -292,7 +292,7 @@ class pane (proverpane : GuiConfig.provers) =
     method private register_provers dps =
       begin
         (* register missing provers *)
-        let prvs = List.map ProverWhy3.prover dps in
+        let prvs = List.map (fun p -> VCS.Why3 p) dps in
         (* set visible provers *)
         List.iter
           (fun prover ->

src/plugins/wp/GuiGoal.mli

@@ -24,7 +24,7 @@
 (* --- PO Details View                                                    --- *)
 (* -------------------------------------------------------------------------- *)
 
-class pane : GuiConfig.provers ->
+class pane : GuiConfig.enabled ->
   object
 
     method select : Wpo.t option -> unit

src/plugins/wp/GuiList.ml

@@ -72,7 +72,7 @@ let render_prover_result p =
         end
     | { verdict=r } , _ -> icon_of_verdict r
 
-class pane (enabled:GuiConfig.provers) =
+class pane (enabled:GuiConfig.enabled) =
   let model = new model in
   let list = new Wtable.list ~headers:true ~rules:true model#coerce in
   object(self)
@@ -111,31 +111,26 @@ class pane (enabled:GuiConfig.provers) =
     method private create_prover p =
       begin
         let title = VCS.title_of_prover p in
-        let column = list#add_column_pixbuf ~title [] (render_prover_result p) in
-        if p <> VCS.Qed then provers <- (p,column) :: provers
+        let column = list#add_column_pixbuf ~title [] (render_prover_result p)
+        in if p <> VCS.Qed then provers <- (p,column) :: provers
       end
 
     method private configure dps =
-      let open ProverWhy3 in
       begin
-        let rec wanted p = function
-          | [] -> false
-          | dp :: dps -> dp.dp_prover = p || dp.dp_name = p || wanted p dps
-        in
         (* Removing Useless Columns *)
         List.iter
           (fun (vcs,column) ->
              match vcs with
-             | VCS.Why3 p when not (wanted p dps) ->
+             | VCS.Why3 p when not (List.mem p dps) ->
                  ignore (list#view#remove_column column)
              | _ -> ()
           ) provers ;
         (* Installing Missing Columns *)
         List.iter
           (fun dp ->
-             let p = VCS.Why3 dp.dp_prover in
-             match self#column_of_prover p with
-             | None -> self#create_prover p
+             let prv = VCS.Why3 dp in
+             match self#column_of_prover prv with
+             | None -> self#create_prover prv
              | Some _ -> ()
           ) dps ;
       end

src/plugins/wp/GuiList.mli

@@ -24,7 +24,7 @@
 (* --- PO List View                                                       --- *)
 (* -------------------------------------------------------------------------- *)
 
-class pane : GuiConfig.provers ->
+class pane : GuiConfig.enabled ->
   object
 
     method show : Wpo.t -> unit

src/plugins/wp/GuiNavigator.ml

@@ -406,9 +406,8 @@ let make (main : main_window_extension_points) =
     (* --- Provers                                                            --- *)
     (* -------------------------------------------------------------------------- *)
 
-    let available = new GuiConfig.provers "wp.available" in
-    let enabled = new GuiConfig.provers "wp.enabled" in
-    if Wp_parameters.Detect.get () then ProverWhy3.detect_provers available#set ;
+    let available = new GuiConfig.available () in
+    let enabled = new GuiConfig.enabled "wp.enabled" in
 
     let dp_chooser = new GuiConfig.dp_chooser ~main ~available ~enabled in
 
@@ -504,7 +503,6 @@ let make (main : main_window_extension_points) =
     main#register_source_selector popup#register ;
     GuiPanel.register ~main
       ~available_provers:available
-      ~enabled_provers:enabled
       ~configure_provers:dp_chooser#run ;
   end
 

src/plugins/wp/GuiPanel.ml

@@ -192,8 +192,7 @@ let wp_update_script label () =
 
 let wp_panel
     ~(main:Design.main_window_extension_points)
-    ~(available_provers:GuiConfig.provers)
-    ~(enabled_provers:GuiConfig.provers)
+    ~(available_provers:GuiConfig.available)
     ~(configure_provers:unit -> unit)
   =
   let vbox = GPack.vbox () in
@@ -222,9 +221,7 @@ let wp_panel
     ~label:"Provers..." ~tooltip:"Detect WP Provers" () in
   prover_cfg#connect configure_provers ;
   form#add_label_widget prover_cfg#coerce ;
-  let prover_menu = new GuiConfig.dp_button
-    ~available:available_provers
-    ~enabled:enabled_provers in
+  let prover_menu = new GuiConfig.dp_button ~available:available_provers in
   form#add_field prover_menu#coerce ;
   Gtk_form.register demon prover_menu#update ;
   (* End Form *)
@@ -317,8 +314,8 @@ let wp_panel
     "WP" , vbox#coerce , Some (Gtk_form.refresh demon) ;
   end
 
-let register ~main ~available_provers ~enabled_provers ~configure_provers =
+let register ~main ~available_provers ~configure_provers =
   main#register_panel
-    (fun main -> wp_panel ~main ~available_provers ~enabled_provers ~configure_provers)
+    (fun main -> wp_panel ~main ~available_provers ~configure_provers)
 
 (* -------------------------------------------------------------------------- *)

src/plugins/wp/GuiPanel.mli

@@ -31,6 +31,5 @@ val run_and_prove :
 
 val register :
   main:Design.main_window_extension_points ->
-  available_provers:GuiConfig.provers ->
-  enabled_provers:GuiConfig.provers ->
+  available_provers:GuiConfig.available ->
   configure_provers:(unit -> unit) -> unit

src/plugins/wp/Makefile.in

@@ -34,8 +34,10 @@ ifneq ("$(FRAMAC_INTERNAL)","yes")
 include $(FRAMAC_SHARE)/Makefile.config
 endif
 
-# Coq Resources Installation
+# Why3 API Available
+WHY3API=@WHY3API@
 
+# Coq Resources Installation
 include $(PLUGIN_DIR)/share/Makefile.resources
 
 # Extension of the GUI for wp is compilable
@@ -87,7 +89,8 @@ PLUGIN_CMO:= \
 	TacCongruence TacOverflow Auto \
 	ProofSession ProofScript ProofEngine \
 	why3_xml \
-	ProverTask ProverErgo ProverCoq ProverWhy3 ProverWhy3ide \
+	ProverTask ProverErgo ProverCoq \
+	ProverDetect ProverWhy3 ProverWhy3ide \
 	driver prover ProverSearch ProverScript \
 	Generator Factory \
 	calculus cfgDump cfgWP \
@@ -100,7 +103,13 @@ PLUGIN_GENERATED:= \
    $(PLUGIN_DIR)/rformat.ml \
    $(PLUGIN_DIR)/driver.ml \
    $(PLUGIN_DIR)/why3_xml.ml \
+   $(PLUGIN_DIR)/ProverDetect.ml \
    $(PLUGIN_DIR)/Wp.mli
+
+ifeq ($(WHY3API),yes)
+PLUGIN_REQUIRES:= why3
+endif
+
 PLUGIN_DEPENDENCIES:= rtegen qed
 PLUGIN_UNDOC+=
 PLUGIN_INTRO:=$(PLUGIN_DIR)/intro_wp.txt
@@ -108,6 +117,8 @@ PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
 PLUGIN_DISTRIB_EXTERNAL:= \
 	Changelog \
 	Makefile.in \
+	ProverDetect.Why3.ml \
+	ProverDetect.None.ml \
         MakeAPI \
 	configure.ac \
 	configure \
@@ -281,6 +292,23 @@ wp-coq-uninstall:
 	@rm -f $(FRAMAC_DATADIR)/wp/coqwp/*.vo
 	@rm -f $(FRAMAC_DATADIR)/wp/coqwp/*/*.vo
 
+# --------------------------------------------------------------------------
+# --- Provers Detection
+# --------------------------------------------------------------------------
+
+$(Wp_DIR)/ProverDetect.ml: config.status $(Wp_DIR)/Makefile.in
+
+ifeq ($(WHY3API),yes)
+$(Wp_DIR)/ProverDetect.ml: $(Wp_DIR)/ProverDetect.Why3.ml
+	$(PRINT_MAKING) "$@ (why3)"
+	@cp -f $< $@
+	$(CHMOD_RO) $@
+else
+$(Wp_DIR)/ProverDetect.ml: $(Wp_DIR)/ProverDetect.None.ml
+	$(PRINT_MAKING) "$@ (none)"
+	@cp -f $< $@
+	$(CHMOD_RO) $@
+endif
 
 # --------------------------------------------------------------------------
 # --- Why3 configuration
@@ -303,7 +331,6 @@ $(Wp_DIR)/share/why3/why3.conf:
 	@printf "option=\"--eval \\\\\"(setq coq-load-path (cons '(\\\\\\\\\\\\\"$(FRAMAC_DATADIR)/wp/why3\\\\\\\\\\\\\" \\\\\\\\\\\\\"\\\\\\\\\\\\\") coq-load-path))\\\\\"\"\n"  >> $@
 	@chmod u-w $@
 
-
 # --------------------------------------------------------------------------
 # --- Installation                                                       ---
 # --------------------------------------------------------------------------