[wp/gui] disable non-used native provers

src/plugins/wp/GuiConfig.ml

@@ -24,7 +24,7 @@
 (* ---  Prover List in Configuration                                    --- *)
 (* ------------------------------------------------------------------------ *)
 
-class enabled key =
+class provers key =
   object(self)
     inherit [Why3.Whyconf.Sprover.t] Wutil.selector Why3.Whyconf.Sprover.empty
 
@@ -63,7 +63,7 @@ class enabled key =
         let selection = List.fold_left
             (fun acc e ->
                match Why3Provers.find_opt e with
-               | None-> acc
+               | None -> acc
                | Some p -> Why3.Whyconf.Sprover.add p acc)
             settings cmdline
         in
@@ -79,7 +79,7 @@ class enabled key =
 
 class dp_chooser
     ~(main:Design.main_window_extension_points)
-    ~(enabled:enabled)
+    ~(provers:provers)
   =
   let dialog = new Wpane.dialog
     ~title:"Why3 Provers"
@@ -123,7 +123,7 @@ class dp_chooser
       end
 
     method private apply () =
-      enabled#set
+      provers#set
         (Why3.Whyconf.Mprover.map_filter
            (function
              | true -> Some ()
@@ -132,7 +132,7 @@ class dp_chooser
 
     method run () =
       let dps = Why3Provers.provers_set () in
-      let sel = enabled#get in
+      let sel = provers#get in
       selected <- Why3.Whyconf.Mprover.merge
           (fun _ avail enab ->
              match avail, enab with

src/plugins/wp/GuiConfig.mli

@@ -24,11 +24,11 @@
 (* ---  WP Provers Configuration Panel                                  --- *)
 (* ------------------------------------------------------------------------ *)
 
-class enabled : string -> [Why3.Whyconf.Sprover.t] Widget.selector
+class provers : string -> [Why3.Whyconf.Sprover.t] Widget.selector
 
 class dp_chooser :
   main:Design.main_window_extension_points ->
-  enabled:enabled ->
+  provers:provers ->
   object
     method run : unit -> unit (** Edit enabled provers *)
   end

src/plugins/wp/GuiGoal.ml

@@ -73,7 +73,7 @@ class iformat =
 (* --- Goal Panel                                                         --- *)
 (* -------------------------------------------------------------------------- *)
 
-class pane (enabled : GuiConfig.enabled) =
+class pane (gprovers : GuiConfig.provers) =
   let icon = new Widget.image GuiProver.no_status in
   let status = new Widget.label () in
   let text = new Wtext.text () in
@@ -127,7 +127,7 @@ class pane (enabled : GuiConfig.enabled) =
           VCS.([ new GuiProver.prover ~console:text ~prover:NativeAltErgo ] @
                List.map
                  (fun dp -> new GuiProver.prover text (VCS.Why3 dp))
-                 (Why3.Whyconf.Sprover.elements enabled#get)) ;
+                 (Why3.Whyconf.Sprover.elements gprovers#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 (enabled : GuiConfig.enabled) =
              tactics <- gtac :: tactics ;
              palette#add_tool gtac#tool) ;
         tactics <- List.rev tactics ;
-        self#register_provers enabled#get;
+        self#register_provers gprovers#get;
         printer#on_selection (fun () -> self#update) ;
         scripter#on_click self#goto ;
         scripter#on_backtrack self#backtrack ;
-        enabled#connect self#register_provers ;
+        gprovers#connect self#register_provers ;
         delete#connect (fun () -> self#interrupt ProofEngine.reset) ;
         cancel#connect (fun () -> self#interrupt ProofEngine.cancel) ;
         forward#connect (fun () -> self#forward) ;

src/plugins/wp/GuiGoal.mli

@@ -24,7 +24,7 @@
 (* --- PO Details View                                                    --- *)
 (* -------------------------------------------------------------------------- *)
 
-class pane : GuiConfig.enabled ->
+class pane : GuiConfig.provers ->
   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.enabled) =
+class pane (gprovers:GuiConfig.provers) =
   let model = new model in
   let list = new Wtable.list ~headers:true ~rules:true model#coerce in
   object(self)
@@ -147,11 +147,16 @@ class pane (enabled:GuiConfig.enabled) =
         ignore (list#add_column_text ~title:"Model" [] render) ;
         List.iter
           self#create_prover
-          [ VCS.Qed ; VCS.Tactical ; VCS.NativeAltErgo ; VCS.NativeCoq ] ;
+          [ VCS.Qed ; VCS.Tactical ] ;
+        let prv = Wp_parameters.Provers.get () in
+        if List.mem "native:alt-ergo" prv then
+          self#create_prover VCS.NativeAltErgo ;
+        if List.mem "native:coq" prv then
+          self#create_prover VCS.NativeCoq ;
         ignore (list#add_column_empty) ;
         list#set_selection_mode `MULTIPLE ;
-        enabled#connect self#configure ;
-        self#configure enabled#get ;
+        gprovers#connect self#configure ;
+        self#configure gprovers#get ;
       end
 
     method private on_cell f w c = f w (self#prover_of_column c)

src/plugins/wp/GuiList.mli

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

src/plugins/wp/GuiNavigator.ml

@@ -397,9 +397,9 @@ let make (main : main_window_extension_points) =
     (* --- Provers                                                            --- *)
     (* -------------------------------------------------------------------------- *)
 
-    let enabled = new GuiConfig.enabled "wp.enabled" in
+    let provers = new GuiConfig.provers "wp.provers" in
 
-    let dp_chooser = new GuiConfig.dp_chooser ~main ~enabled in
+    let dp_chooser = new GuiConfig.dp_chooser ~main ~provers in
 
     (* -------------------------------------------------------------------------- *)
     (* --- Focus Bar                                                          --- *)
@@ -423,7 +423,7 @@ let make (main : main_window_extension_points) =
         (index :> widget) ;
         (next :> widget) ;
       ] in
-    let provers = new Widget.button ~label:"Provers..." () in
+    let pvrs = new Widget.button ~label:"Provers..." () in
     let clear = new Widget.button ~label:"Clear" ~icon:`DELETE () in
     let focusbar = GPack.hbox ~spacing:0 () in
     begin
@@ -431,8 +431,8 @@ let make (main : main_window_extension_points) =
       focusbar#pack ~padding:20 ~expand:false scope#coerce ;
       focusbar#pack ~padding:20 ~expand:false filter#coerce ;
       focusbar#pack ~from:`END ~expand:false clear#coerce ;
-      focusbar#pack ~from:`END ~expand:false provers#coerce ;
-      provers#connect dp_chooser#run ;
+      focusbar#pack ~from:`END ~expand:false pvrs#coerce ;
+      pvrs#connect dp_chooser#run ;
     end ;
 
     (* -------------------------------------------------------------------------- *)
@@ -452,8 +452,8 @@ let make (main : main_window_extension_points) =
     (* -------------------------------------------------------------------------- *)
 
     let book = new Wpane.notebook ~default:`List () in
-    let list = new GuiList.pane enabled in
-    let goal = new GuiGoal.pane enabled in
+    let list = new GuiList.pane provers in
+    let goal = new GuiGoal.pane provers in
     begin
       book#add `List list#coerce ;
       book#add `Goal goal#coerce ;

src/plugins/wp/ProverWhy3.ml

@@ -1107,7 +1107,7 @@ let get_miss () = !miss
 let get_removed () = !removed
 
 let mark_cache ~mode hash =
-  if mode = Cleanup then Hashtbl.replace cleanup hash ()
+  if mode = Cleanup || !Config.is_gui then Hashtbl.replace cleanup hash ()
 
 let cleanup_cache ~mode =
   if mode = Cleanup && (!hits > 0 || !miss > 0) then