[Policy] Adds the remove policy

         allows to remove completely some prover version

src/driver/whyconf.ml

@@ -117,12 +117,14 @@ type prover_upgrade_policy =
   | CPU_keep
   | CPU_upgrade of prover
   | CPU_duplicate of prover
+  | CPU_remove
 
 let print_prover_upgrade_policy fmt p =
   match p with
   | CPU_keep -> Format.fprintf fmt "keep"
   | CPU_upgrade p -> Format.fprintf fmt "upgrade to %a" print_prover p
   | CPU_duplicate p -> Format.fprintf fmt "copy to %a" print_prover p
+  | CPU_remove -> Format.fprintf fmt "remove"
 
 
 
@@ -376,6 +378,8 @@ let set_prover_upgrade_policy prover policy (i, family) =
     match policy with
       | CPU_keep ->
         set_string section "policy" "keep"
+      | CPU_remove ->
+        set_string section "policy" "remove"
       | CPU_upgrade p ->
         let section = set_string section "target_name" p.prover_name in
         let section = set_string section "target_version" p.prover_version in
@@ -470,6 +474,7 @@ let load_policy provers acc (_,section) =
     try
       match get_string section "policy" with
       | "keep" -> Mprover.add source CPU_keep acc
+      | "remove" -> Mprover.add source CPU_remove acc
       | "upgrade" ->
         let target =
           { prover_name = get_string section "target_name";

src/driver/whyconf.mli

@@ -173,6 +173,7 @@ type prover_upgrade_policy =
   | CPU_keep
   | CPU_upgrade of prover
   | CPU_duplicate of prover
+  | CPU_remove
 
 val print_prover_upgrade_policy : Format.formatter -> prover_upgrade_policy -> unit
 

src/ide/gconfig.ml

@@ -1026,6 +1026,7 @@ let alternatives_frame c (notebook:GPack.notebook) =
   let iter p policy =
     let label =
       match policy with
+        | CPU_remove -> Pp.sprintf_wnl "proofs with %a removed" print_prover p
         | CPU_keep -> Pp.sprintf_wnl "proofs with %a kept as they are" print_prover p
         | CPU_upgrade t ->
           Pp.sprintf_wnl "proofs with %a moved to %a" print_prover p print_prover t

src/ide/why3ide.ml

@@ -1383,6 +1383,7 @@ let on_selected_row r =
          | Controller_itp.InternalFailure e ->
             (Pp.sprintf "internal failure: %a" Exn_printer.exn_printer e)
          | Controller_itp.Uninstalled _p -> "uninstalled prover"
+         | Controller_itp.Removed _p -> "removed proof attempt"
          | Controller_itp.UpgradeProver _p -> "upgraded prover"
        in
        let output_text =
@@ -1603,6 +1604,7 @@ let image_of_pa_status ~obsolete pa =
   | Controller_itp.InternalFailure _e -> !image_failure
   | Controller_itp.Detached -> !image_undone (* TODO !image_detached *)
   | Controller_itp.Uninstalled _p -> !image_undone (* TODO !image_uninstalled *)
+  | Controller_itp.Removed _p -> !image_undone (* TODO !image_removed *)
   | Controller_itp.UpgradeProver _p -> !image_undone
   | Controller_itp.Done r ->
     let pr_answer = r.Call_provers.pr_answer in
@@ -1695,6 +1697,7 @@ let set_status_and_time_column ?limit row =
         | C.Undone -> "(undone)"
         | C.Uninstalled _ -> "(uninstalled prover)"
         | C.UpgradeProver _ -> "(upgraded prover)"
+        | C.Removed _ -> "(removed prover)"
         | C.Scheduled -> "(scheduled)"
         | C.Running -> "(running)"
         | C.Detached -> "(detached)"

src/session/controller_itp.ml

@@ -31,6 +31,7 @@ type proof_attempt_status =
   | InternalFailure of exn (** external proof aborted by internal error *)
   | Uninstalled of Whyconf.prover (** prover is uninstalled *)
   | UpgradeProver of Whyconf.prover (** prover is upgraded *)
+  | Removed of Whyconf.prover (** prover has been removed or upgraded *)
 
 let print_status fmt st =
   match st with
@@ -47,6 +48,8 @@ let print_status fmt st =
       fprintf fmt "Prover %a is uninstalled" Whyconf.print_prover pr
   | UpgradeProver pr    ->
       fprintf fmt "Prover upgrade to %a" Whyconf.print_prover pr
+  | Removed pr    ->
+      fprintf fmt "Prover %a removed" Whyconf.print_prover pr
 
 type transformation_status =
   | TSscheduled | TSdone of transID | TSfailed of (proofNodeID * exn)
@@ -496,7 +499,7 @@ let schedule_proof_attempt c id pr ?save_to ~limit ~callback ~notification =
   let callback panid s =
     begin
       match s with
-      | UpgradeProver _ -> ()
+      | UpgradeProver _ | Removed _ -> ()
       | Scheduled ->
          Hpan.add c.controller_running_proof_attempts panid ();
          update_goal_node notification ses id
@@ -656,7 +659,7 @@ let schedule_edition c id pr ~callback ~notification =
       | Interrupted
       | InternalFailure _ ->
          update_goal_node notification session id
-      | Undone | Detached | Uninstalled _ | Scheduled -> assert false
+      | Undone | Detached | Uninstalled _ | Scheduled | Removed _ -> assert false
     end;
     callback panid s
   in
@@ -731,7 +734,7 @@ let run_strategy_on_goal
               callback (STSgoto (g,pc+1));
               let run_next () = exec_strategy (pc+1) strat g; false in
               S.idle ~prio:0 run_next
-           | Undone | Detached | Uninstalled _ ->
+           | Undone | Detached | Uninstalled _ | Removed _ ->
                          (* should not happen *)
                          assert false
          in
@@ -910,22 +913,23 @@ let copy_paste ~notification ~callback_pa ~callback_tr c from_any to_any =
 let debug_replay = Debug.register_flag "replay" ~desc:"Debug@ info@ for@ replay"
 
 let find_prover notification c goal_id pr =
-  if Hprover.mem c.controller_provers pr then Some pr else
+  if Hprover.mem c.controller_provers pr then `Found pr else
    match Whyconf.get_prover_upgrade_policy c.controller_config pr with
-   | exception Not_found -> None
-   | Whyconf.CPU_keep -> None
+   | exception Not_found -> `Keep
+   | Whyconf.CPU_keep -> `Keep
    | Whyconf.CPU_upgrade new_pr ->
       (* does a proof using new_pr already exists ? *)
       if Hprover.mem (get_proof_attempt_ids c.controller_session goal_id) new_pr
-      then (* yes, then we do nothing *)
-        None
+      then (* yes, then we remove the attempt *)
+        `Remove
       else
         begin
           (* we modify the prover in-place *)
           Session_itp.change_prover notification c.controller_session goal_id pr new_pr;
-          Some new_pr
+          `Found new_pr
         end
-   | Whyconf.CPU_duplicate _new_pr ->
+   | Whyconf.CPU_remove -> `Remove
+   | Whyconf.CPU_duplicate _ (* _new_pr *) ->
       assert false (* TODO *)
 (*
       (* does a proof using new_p already exists ? *)
@@ -946,8 +950,11 @@ let replay_proof_attempt c pr limit (parid: proofNodeID) id ~callback ~notificat
   (* The replay can be done on a different machine so we need
      to check more things before giving the attempt to the scheduler *)
   match find_prover notification c parid pr with
-  | None -> callback id (Uninstalled pr)
-  | Some pr' ->
+  | `Keep -> callback id (Uninstalled pr)
+  | `Remove ->
+      remove_proof_attempt c.controller_session parid pr;
+      callback id (Removed pr)
+  | `Found pr' ->
      try
        if pr' <> pr then callback id (UpgradeProver pr');
        let _ = get_task c.controller_session parid in
@@ -1004,7 +1011,7 @@ let replay ~valid_only ~obsolete_only ?(use_steps=false) ?(filter=fun _ -> true)
 
   let craft_report s id pr limits pa =
     match s with
-    | UpgradeProver _ -> found_upgraded_prover := true
+    | UpgradeProver _ | Removed _ -> found_upgraded_prover := true
     | Scheduled | Running -> ()
     | Undone | Interrupted ->
        decr count;
@@ -1144,7 +1151,7 @@ let bisect_proof_attempt ~callback_tr ~callback_pa ~notification ~removed c pa_i
                   callback_pa paid st;
                   begin match st with
                   | UpgradeProver _ | Scheduled | Running -> ()
-                  | Detached | Uninstalled _ -> assert false
+                  | Detached | Uninstalled _ | Removed _ -> assert false
                   | Undone | Interrupted -> Debug.dprintf debug "Bisecting interrupted.@."
                   | InternalFailure exn ->
                      (* Perhaps the test can be considered false in this case? *)
@@ -1206,7 +1213,7 @@ later on. We do has if proof fails. *)
               callback_pa paid st;
               begin
               match st with
-              | UpgradeProver _ -> ()
+              | UpgradeProver _ | Removed _ -> ()
               | Scheduled ->
                  Debug.dprintf
                    debug "[Bisect] prover on subtask is scheduled@."

src/session/controller_itp.mli

@@ -26,6 +26,7 @@ type proof_attempt_status =
   | InternalFailure of exn (** external proof aborted by internal error *)
   | Uninstalled of Whyconf.prover (** prover is uninstalled *)
   | UpgradeProver of Whyconf.prover (** prover is upgraded *)
+  | Removed of Whyconf.prover (** prover has been removed or upgraded *)
 
 val print_status : Format.formatter -> proof_attempt_status -> unit
 

src/session/json_util.ml

@@ -106,6 +106,9 @@ let convert_proof_attempt (pas: proof_attempt_status) =
   | Uninstalled p ->
       convert_record ["proof_attempt", String "Uninstalled";
                       "prover", convert_prover_to_json "prover_" p]
+  | Removed p ->
+      convert_record ["proof_attempt", String "Removed";
+                      "prover", convert_prover_to_json "prover_" p]
   | UpgradeProver p ->
       convert_record ["proof_attempt", String "UpgradeProver";
                       "prover", convert_prover_to_json "prover_" p])
@@ -175,6 +178,7 @@ open Whyconf
 
 let convert_policy u =
   match u with
+  | CPU_remove -> ["policy", String "remove"]
   | CPU_keep -> ["policy", String "keep"]
   | CPU_upgrade p ->
      ["policy", String "upgrade"] @ convert_prover "target_" p