From 68ebd47f4607f25f34922ffd08acbeee5689c527 Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Wed, 24 Jan 2024 15:39:30 +0100
Subject: [PATCH] More consistant logging
---
src/language.ml | 3 +--
src/logging.ml | 3 +++
src/logging.mli | 3 +++
src/verification.ml | 7 +++----
tests/nier_to_onnx.t | 4 +++-
5 files changed, 13 insertions(+), 7 deletions(-)
diff --git a/src/language.ml b/src/language.ml
index 09c4813..6d9a186 100644
--- a/src/language.ml
+++ b/src/language.ml
@@ -244,8 +244,7 @@ let create_nn_onnx =
Logs.warn (fun m ->
m "Cannot build network intermediate representation:@ %s" msg);
None
- | Ok nier ->
- Some nier
+ | Ok nier -> Some nier
in
{
nn_nb_inputs = n_inputs;
diff --git a/src/logging.ml b/src/logging.ml
index 78b3cfd..e9642b4 100644
--- a/src/logging.ml
+++ b/src/logging.ml
@@ -81,6 +81,9 @@ let code_error ?src f =
exception User_error
+let info ?src f =
+ Logs.info ?src f
+
let user_error ?src f =
Logs.err ?src f;
raise User_error
diff --git a/src/logging.mli b/src/logging.mli
index 7ebf4c3..417e35c 100644
--- a/src/logging.mli
+++ b/src/logging.mli
@@ -38,6 +38,9 @@ val setup :
val is_debug_level : Logs.src -> bool
+val info : ?src:Logs.src -> (_, unit) Logs.msgf -> unit
+(** Log a message to the user and continue the execution. *)
+
val code_error : ?src:Logs.src -> (_, unit) Logs.msgf -> 'b
(** Terminate execution with a [code error] message. *)
diff --git a/src/verification.ml b/src/verification.ml
index e59c1bc..2fc3646 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -261,11 +261,10 @@ let answer_generic limit config prover config_prover driver ~proof_strategy
| Some { nn_nier = Some g; _ } -> (
try
Onnx.write g f;
- Logs.info (fun m -> m "@[Wrote ONNX file at '%s'@]" f)
+ Logging.info (fun m -> m "@[Wrote ONNX file at '%s'@]" f)
with Sys_error msg ->
- Logs.err (fun m ->
- m "@[System error: tried to write ONNX file a '%s', got '%s'@]"
- f msg))
+ Logging.user_error (fun m ->
+ m "@[Tried to write ONNX file at '%s', got '%s'@]" f msg))
| None -> ()
| _ -> ()
in
diff --git a/tests/nier_to_onnx.t b/tests/nier_to_onnx.t
index bda0cef..8cd9fb3 100644
--- a/tests/nier_to_onnx.t
+++ b/tests/nier_to_onnx.t
@@ -4,7 +4,7 @@ Test verify
$ bin/pyrat.py --version
PyRAT 1.1
- $ caisar verify --format whyml --prover=PyRAT --onnx-out-file="out.onnx" - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify --format whyml --prover=PyRAT -v --onnx-out-file="out.onnx" - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory NIER_to_ONNX
> use ieee_float.Float64
> use bool.Bool
@@ -21,6 +21,8 @@ Test verify
> (0.5:t) .< (nn@@i)[0] .< (0.5:t)
> end
> EOF
+ [INFO] Wrote ONNX file at 'out.onnx'
+ [INFO] Verification results for theory 'NIER_to_ONNX'
Goal G: Unknown ()
Data should be 0.135
--
GitLab