Theory ML_Logger_Examples

✐‹creator "Kevin Kappelmann"›
subsection ‹Examples›
theory ML_Logger_Examples
  imports
    ML_Logger
    Setup_Result_Commands
begin

text ‹First some simple, barebone logging: print some information.›
ML_command‹
  ― ‹the following two are equivalent›
  val _ = Logger.log Logger.root Logger.INFO @{context} (K "hello root logger")
  val _ = @{log Logger.INFO Logger.root} @{context} (K "hello root logger")
›

ML_command‹
  val logger = Logger.root
  val _ = @{log} @{context} (K "hello root logger")
  ― ‹‹@{log}› is equivalent to ‹Logger.log logger Logger.INFO››
›

text ‹To guarantee the existence of a "logger" in an ML structure, one should use the
‹HAS_LOGGER› signature.›
ML‹
  structure My_Struct : sig
    include HAS_LOGGER
    val get_n :  Proof.context -> int
  end = struct
    val logger = Logger.setup_new_logger Logger.root "My_Struct"
    fun get_n ctxt = (@{log} ctxt (K "retrieving n..."); 42)
  end
›

ML_command‹val n = My_Struct.get_n @{context}›

text‹We can set up a hierarchy of loggers›
ML‹
  val logger = Logger.root
  val parent1 = Logger.setup_new_logger Logger.root "Parent1"
  val child1 = Logger.setup_new_logger parent1 "Child1"
  val child2 = Logger.setup_new_logger parent1 "Child2"

  val parent2 = Logger.setup_new_logger Logger.root "Parent2"
›

ML_command‹
  (@{log Logger.INFO Logger.root} @{context} (K "Hello root logger");
  @{log Logger.INFO parent1} @{context} (K "Hello parent1");
  @{log Logger.INFO child1} @{context} (K "Hello child1");
  @{log Logger.INFO child2} @{context} (K "Hello child2");
  @{log Logger.INFO parent2} @{context} (K "Hello parent2"))
›

text ‹We can use different log levels to show/surpress messages. The log levels are based on
Apache's Log4J 2 🌐‹https://logging.apache.org/log4j/2.x/manual/customloglevels.html›.›
ML_command‹@{log Logger.DEBUG parent1} @{context} (K "Hello parent1")› ―‹prints nothings›
declare [[ML_map_context ‹Logger.set_log_level parent1 Logger.DEBUG›]]
ML_command‹@{log Logger.DEBUG parent1} @{context} (K "Hello parent1")› ―‹prints message›
ML_command‹Logger.ALL› ―‹ctrl+click on the value to see all log levels›

text ‹We can set options for all loggers below a given logger. Below, we set the log level for all
loggers below (and including) \<^ML>‹parent1› to error, thus disabling warning messages.›
ML_command‹
  (@{log Logger.WARN parent1} @{context} (K "Warning from parent1");
  @{log Logger.WARN child1} @{context} (K "Warning from child1"))
›
declare [[ML_map_context ‹Logger.set_log_levels parent1 Logger.ERR›]]
ML_command‹
  (@{log Logger.WARN parent1} @{context} (K "Warning from parent1");
  @{log Logger.WARN child1} @{context} (K "Warning from child1"))
›
declare [[ML_map_context ‹Logger.set_log_levels parent1 Logger.INFO›]]

text ‹We can set message filters.›

declare [[ML_map_context ‹Logger.set_msg_filters Logger.root (match_string "Third")›]]
ML_command‹
  (@{log Logger.INFO parent1} @{context} (K "First message");
  @{log Logger.INFO child1} @{context} (K "Second message");
  @{log Logger.INFO child2} @{context} (K "Third message");
  @{log Logger.INFO parent2} @{context} (K "Fourth message"))
›
declare [[ML_map_context ‹Logger.set_msg_filters Logger.root (K true)›]]

text ‹One can also use different output channels (e.g. files) and hide/show some additional
logging information. Ctrl+click on below values and explore.›
ML_command‹Logger.set_output; Logger.set_show_logger; Logging_Antiquotation.show_log_pos›

text ‹To set up (local) loggers outside ML environments,
@{theory ML_Unification.Setup_Result_Commands} contains two commands,
@{command setup_result} and @{command local_setup_result}.›
experiment
begin
local_setup_result local_logger = ‹Logger.new_logger Logger.root "Local"›

ML_command‹@{log Logger.INFO local_logger} @{context} (K "Hello local world")›
end

text ‹‹local_logger› is no longer available. The follow thus does not work:›
― ‹ML_command‹@{log Logger.INFO local_logger} @{context} (K "Hello local world")››

text ‹Let us create another logger in the global context.›
setup_result some_logger = ‹Logger.new_logger Logger.root "Some_Logger"›
ML_command‹@{log Logger.INFO some_logger} @{context} (K "Hello world")›

text ‹Let us delete it again.›
declare [[ML_map_context ‹Logger.delete_logger some_logger›]]
text ‹The logger can no longer be found in the logger hierarchy›
ML_command‹@{log Logger.INFO some_logger} @{context} (K "Hello world")›

end