logging.mli

(**************************************************************************)
(*                                                                        *)
(*  This file is part of CAISAR.                                          *)
(*                                                                        *)
(*  Copyright (C) 2023                                                    *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  You can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the          *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

(** {2 Sources} *)

val src_autodetect : Logs.src
val src_prover_spec : Logs.src
val src_prover_call : Logs.src
val src_interpret_goal : Logs.src
val src_nier : Logs.src
val src_stack_trace : Logs.src

val all_srcs : unit -> Logs.src list
(** @return all available sources. *)

(** {2 Logs} *)

val setup :
  Fmt.style_renderer option -> Logs.level option -> Logs.src list -> unit

val is_debug_level : Logs.src -> bool

val code_error : src:Logs.src -> (_, unit) Logs.msgf -> 'b
(** Terminate execution with a [code error] message. *)

val user_error : ?loc:Why3.Loc.position -> (_, unit) Logs.msgf -> 'b
(** Terminate execution with a [user error] message. *)

val not_implemented_yet : ?src:Logs.src -> (_, unit) Logs.msgf -> 'b
(** Terminate execution with a [not implemented yet] message. *)

val protect_main : (unit -> unit) -> unit