More consistant logging

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;

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

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. *)
 

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

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