[wp] Print qualified only when shell key is active

src/plugins/wp/VCS.ml

@@ -24,6 +24,7 @@
 (* --- Prover Results                                                     --- *)
 (* -------------------------------------------------------------------------- *)
 
+let dkey_shell = Wp_parameters.register_category "shell"
 let dkey_no_time_info = Wp_parameters.register_category "no-time-info"
 let dkey_no_step_info = Wp_parameters.register_category "no-step-info"
 let dkey_no_goals_info = Wp_parameters.register_category "no-goals-info"
@@ -328,10 +329,10 @@ let pp_cache_miss fmt st prover r =
     | NativeAltErgo | NativeCoq -> r.verdict <> Timeout
     | Why3 _ -> r.cached || r.prover_time < Rformat.epsilon
   in
-  if qualified then
-    Format.pp_print_string fmt (if is_valid r then "Valid" else "Unsuccess")
-  else
+  if not qualified && Wp_parameters.has_dkey dkey_shell then
     Format.fprintf fmt "%s%a (unqualified)" st pp_perf r
+  else
+    Format.pp_print_string fmt (if is_valid r then "Valid" else "Unsuccess")
 
 let pp_result_qualif prover fmt r =
   if Wp_parameters.has_dkey dkey_success_only then

src/plugins/wp/VCS.mli

@@ -126,6 +126,7 @@ val merge : result -> result -> result
 val choose : result -> result -> result
 val best : result list -> result
 
+val dkey_shell: Wp_parameters.category
 val dkey_no_time_info: Wp_parameters.category
 val dkey_no_step_info: Wp_parameters.category
 val dkey_no_goals_info: Wp_parameters.category

src/plugins/wp/register.ml

@@ -24,7 +24,6 @@ open Factory
 
 let dkey_main = Wp_parameters.register_category "main"
 let dkey_raised = Wp_parameters.register_category "raised"
-let dkey_shell = Wp_parameters.register_category "shell"
 let wkey_smoke = Wp_parameters.register_warn_category "smoke"
 
 (* --------- Command Line ------------------- *)
@@ -306,7 +305,7 @@ let do_progress goal msg =
 
 let do_report_cache_usage mode =
   if !exercised > 0 &&
-     not (Wp_parameters.has_dkey dkey_shell) &&
+     not (Wp_parameters.has_dkey VCS.dkey_shell) &&
      not (Wp_parameters.has_dkey VCS.dkey_no_cache_info)
   then
     let hits = Cache.get_hits () in
@@ -739,7 +738,7 @@ let do_cache_cleanup () =
     Cache.cleanup_cache () ;
     let removed = Cache.get_removed () in
     if removed > 0 &&
-       not (Wp_parameters.has_dkey dkey_shell) &&
+       not (Wp_parameters.has_dkey VCS.dkey_shell) &&
        not (Wp_parameters.has_dkey VCS.dkey_no_cache_info)
     then
       Wp_parameters.result "[Cache] removed:%d" removed
@@ -933,7 +932,7 @@ let pp_wp_parameters fmt =
 
 let () = Cmdline.run_after_setting_files
     (fun _ ->
-       if Wp_parameters.has_dkey dkey_shell then
+       if Wp_parameters.has_dkey VCS.dkey_shell then
          Log.print_on_output pp_wp_parameters)
 
 (* -------------------------------------------------------------------------- *)