From d4ab0cd99ff81480681150d1d5c85642f4fd1dcd Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Thu, 1 Jun 2023 11:20:10 +0200
Subject: [PATCH] [tests] CLI for log categories (option 2 without custom
formatter)
---
src/logging.ml | 30 +-----------------------------
src/verification.ml | 2 +-
2 files changed, 2 insertions(+), 30 deletions(-)
diff --git a/src/logging.ml b/src/logging.ml
index c43642d..8767bc0 100644
--- a/src/logging.ml
+++ b/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 ())
diff --git a/src/verification.ml b/src/verification.ml
index 618084d..5457945 100644
--- a/src/verification.ml
+++ b/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;
--
GitLab