Global Logging Control

Provides a global verbosity flag to control debug output during inference.

How to silence Hesper logs

Three options, in order of convenience:

1. Environment variable (recommended for notebooks and CLI):

   HESPER_LOG_LEVEL=quiet   # or: silent, error, off, 0, false, none
   

   This is read once at process start by both the Lean and C++ bridge sides. Anything else (or unset) keeps logs ON for backward compat.

2. Programmatic override (inside a notebook cell, after a stray verbose call has already happened):

   import Hesper.Logging
   #eval Hesper.Logging.setVerbose false
   

   This flips both Lean and C++ flags at runtime. Subsequent getDevice / createBuffer / etc. calls run silently.

3. Per-cell suppression: wrap the noisy code in IO.FS.withIsolatedStreams.

opaque Hesper.Logging.verboseRef : IO.Ref Bool

Global verbosity flag. Default reflects HESPER_LOG_LEVEL; falls back to true for backward compatibility when the env var is unset.

@[extern lean_hesper_set_verbose]

opaque Hesper.Logging.setNativeVerbose : Bool → IO Unit

FFI: Set C++ bridge verbose flag

def Hesper.Logging.setVerbose (v : Bool) : IO Unit

Set global verbosity (both Lean and C++ bridge)

Equations

• Hesper.Logging.setVerbose v = do ST.Ref.set Hesper.Logging.verboseRef v Hesper.Logging.setNativeVerbose v

def Hesper.Logging.isVerbose : IO Bool

Check if verbose logging is enabled

Equations

• Hesper.Logging.isVerbose = ST.Ref.get Hesper.Logging.verboseRef

def Hesper.Logging.logVerbose (msg : String) : IO Unit

Print only when verbose mode is on

Equations

• Hesper.Logging.logVerbose msg = do let __do_lift ← Hesper.Logging.isVerbose if __do_lift = true then IO.println msg else pure PUnit.unit