NLog Notes

We have added logging within our project and have chosen to use NLog.

Since NLog needs a configuration to tell it what to do, the code uses NLog.config in the NHol directory where the fs files are located. The scripts on the other hand use the function configureNLogPrgramatically in init.fsx which does not use the configuration file but builds the configuration in the function itself.

The code configuration file is setup to send messages to the console and to a log file named log.txt in the NHol project directory where the fs files are located. The script is set to send messages only to the file, but currently the autoflush feature is not working, so the messages are not appearing when they are written, but after the file is closed.

The entries in the log are each one line and start with a standard part based on the layout property in the configuration file, e.g.

layout="${time} ${callsite} ${level} ${message}"  

and a message passed from the log function. The layout property has many choices.

If one wants to add a logging capability to an fs file in NHol, they just have to call the log method, e.g.

logger.Trace("A log message.")  

If one wants to trace a function such as

/// Attempts to prove a boolean term using the supplied tactic.
let prove(t, tac) = 
    let th = TAC_PROOF(([], t), tac)
    let t' = concl th
    if t' = t
    then th
    else 
        try 
            EQ_MP (ALPHA t' t) th
        with
        | Failure _ -> failwith "prove: justification generated wrong theorem"

then they can modify it as such

/// Attempts to prove a boolean term using the supplied tactic.
let proveOrig(t, tac) = 
    let th = TAC_PROOF(([], t), tac)
    let t' = concl th
    if t' = t
    then th
    else 
        try 
            EQ_MP (ALPHA t' t) th
        with
        | Failure _ -> failwith "prove: justification generated wrong theorem"

let prove(t, tac) =
    logger.Trace("prove <--")
    logger.Trace(Printf.sprintf "(t : term)     %s" (string_of_term t)) 
    logger.Trace(Printf.sprintf "(tac: tactic)  %s" (string_of_tactic tac)) 
    let result = proveOrig (t,tac)
    logger.Trace(Printf.sprintf "(result : thm) %s" (string_of_thm result))
    logger.Trace("prove -->")
    result

Notice that prove(t, tac) was converted to proveOrig(t, tac) and that the new prove calls proveOrig.

For use with logging are now standard string_of functions for pretty printing values related to theorems.

Type                                 Function  
NHol.fusion.Hol_kernel.hol_type      HOl.printer.pp_print_type  
NHol.fusion.Hol_kernel.term          HOl.printer.pp_print_term  
NHol.fusion.Hol_kernel.thm           HOl.printer.pp_print_thm  
NHol.drule.instantiation             NHol.drule.pp_print_instantiation  
NHol.tactics.goal                    NHol.tactics.pp_print_goal  
NHol.tactics.justification           NHol.tactics.pp_print_justification  
NHol.tactics.goalstate               NHol.tactics.pp_print_goalstate    
NHol.tactics.goalstack               NHol.tactics.pp_print_goalstack  
NHol.tactics.refinement              NHol.tactics.pp_print_refinement  
NHol.tactics.tactic                  NHol.tactics.pp_print_tactic  
NHol.tactics.thm_tactic              NHol.tactics.pp_print_thm_tactic  
NHol.tactics.thm_tactical            NHol.tactics.pp_print_thm_tactical