From 9e1bfc9c65d923cb1aeaccf65c962e6e5f3415c6 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Wed, 7 Jun 2023 14:44:37 +0200
Subject: [PATCH] [log] Create and use new tag for call prover logging.
---
src/logging.ml | 14 ++++++++++++--
src/logging.mli | 1 +
src/verification.ml | 4 ++--
3 files changed, 15 insertions(+), 4 deletions(-)
diff --git a/src/logging.ml b/src/logging.ml
index 3a258a2..2d93d00 100644
--- a/src/logging.ml
+++ b/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 =
diff --git a/src/logging.mli b/src/logging.mli
index ab1dbf8..e406e0d 100644
--- a/src/logging.mli
+++ b/src/logging.mli
@@ -25,6 +25,7 @@
type tag =
| Autodetect
| Specification
+ | CallProver
[@@deriving show { with_path = false }]
val tags_available : unit -> tag list
diff --git a/src/verification.ml b/src/verification.ml
index 82019fe..1361fdd 100644
--- a/src/verification.ml
+++ b/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 =
--
GitLab