Module Soteria_rust_lib.L

include module type of struct include Soteria.Logs.L end
val with_section : ?is_branch:bool -> string -> (unit -> 'a) -> 'a

with_section ~is_branch name f runs f and aggregates its log messages within a collapsible section of the log file (when logs are in HTML mode).

Sections should not be used while defining symbolic processes, as branching will cause a section to be opened once but closed several times.

val log : level:Soteria.Logs.Level.t -> ('a, unit) Soteria.Logs.msgf -> unit

Logs a message at a given level.

For instance, one can log the string "The number is 42" at level Info with

  log ~level:Level.Info (fun m -> m "The number is %d" 42)
val smt : ('a, unit) Soteria.Logs.msgf -> unit

smt is log ~level:Smt

val trace : ('a, unit) Soteria.Logs.msgf -> unit

trace is log ~level:Trace

val debug : ('a, unit) Soteria.Logs.msgf -> unit

debug is log ~level:Debug

val info : ('a, unit) Soteria.Logs.msgf -> unit

info is log ~level:Info

val warn : ('a, unit) Soteria.Logs.msgf -> unit

warn is log ~level:Warn

val error : ('a, unit) Soteria.Logs.msgf -> unit

error is log ~level:Error

val entry_point_section : Charon.Types.name -> (unit -> 'a) -> 'a