[tests] CLI for log categories (option 2 without custom formatter)

src/logging.ml

@@ -53,34 +53,6 @@ let pp_header =
     | Logs.Debug ->
       pp_h ppf debug_style (match h with None -> "DEBUG" | Some h -> h)
 
-let reporter ppf =
-  let report _src level ~over k msgf =
-    let k _ =
-      over ();
-      k ()
-    in
-    let filter_tag (h : string option) (tags : Logs.Tag.set option) k ppf fmt =
-      let has_spec_tag =
-        match tags with
-        | None -> false
-        | Some tags -> Logs.Tag.mem spec_tag_def tags
-      in
-      if has_spec_tag
-      then
-        (* TODO: prepend the SPEC tag to each new line of
-         * fmt? *)
-        Caml.(
-          Format.kfprintf k ppf
-            ("%a[%s]\n@[" ^^ fmt ^^ "@]@.")
-            pp_header (level, h) "SPEC")
-      else
-        Caml.(
-          Format.kfprintf k ppf ("%a@[" ^^ fmt ^^ "@]@.") pp_header (level, h))
-    in
-    msgf @@ fun ?header ?tags fmt -> filter_tag header tags k ppf fmt
-  in
-  { Logs.report }
-
 let specification_enabled = ref false
 
 let setup_log level category =
@@ -91,4 +63,4 @@ let setup_log level category =
     | Some Category.Specification -> specification_enabled := true
     | _ -> ()
   in
-  Logs.set_reporter (reporter Format.std_formatter)
+  Logs.set_reporter (Logs_fmt.reporter ~pp_header ())

src/verification.ml

@@ -165,7 +165,7 @@ let build_command config_prover ~nn_filename =
 let log_prover_task driver task =
   let print fmt task = ignore (Driver.print_task_prepared driver fmt task) in
   Logs.info (fun m ->
-    m ~tags:(Logging.spec_tag ()) "%a" print task)
+      m ~tags:(Logging.spec_tag ()) "[SPEC]\n@[%a@]" print task)
 
 let call_prover_on_task limit config command driver task =
   if !Logging.specification_enabled then log_prover_task driver task;