[log] Create and use new tag for call prover logging.

src/logging.ml

@@ -23,9 +23,10 @@
 type tag =
   | Autodetect
   | Specification
+  | CallProver
 [@@deriving show { with_path = false }]
 
-let tags_available () = [ Autodetect; Specification ]
+let tags_available () = [ Autodetect; Specification; CallProver ]
 let tag_defs_enabled = ref []
 
 let tag_def_auto =
@@ -34,13 +35,22 @@ let tag_def_auto =
 let tag_def_spec =
   Logs.Tag.def "spec" ~doc:"Prover-tailored specification" Fmt.string
 
+let tag_def_call = Logs.Tag.def "call_prover" ~doc:"Call prover" Fmt.string
+
 let tag_def_of_tag = function
   | Autodetect -> tag_def_auto
   | Specification -> tag_def_spec
+  | CallProver -> tag_def_call
 
 let tag_auto = Logs.Tag.add tag_def_auto "AUTO"
 let tag_spec = Logs.Tag.add tag_def_spec "SPEC"
-let add_tag = function Autodetect -> tag_auto | Specification -> tag_spec
+let tag_call = Logs.Tag.add tag_def_call "CALL_PROVER"
+
+let add_tag = function
+  | Autodetect -> tag_auto
+  | Specification -> tag_spec
+  | CallProver -> tag_call
+
 let tag dt = add_tag dt Logs.Tag.empty
 
 let is_tag_enabled tag =

src/logging.mli

@@ -25,6 +25,7 @@
 type tag =
   | Autodetect
   | Specification
+  | CallProver
 [@@deriving show { with_path = false }]
 
 val tags_available : unit -> tag list

src/verification.ml

@@ -304,8 +304,8 @@ let open_file ?format env file =
 
 let verify ?format ~loadpath ?memlimit ?timelimit ?dataset prover ?prover_altern
   file =
-  (if Logging.is_debug_level ()
-   then Debug.(set_flag (lookup_flag "call_prover")));
+  let debug = Logging.(is_debug_level () || is_tag_enabled CallProver) in
+  (if debug then Debug.(set_flag (lookup_flag "call_prover")));
   let env, config = create_env loadpath in
   let main = Whyconf.get_main config in
   let limit =