How to Print to Stdout and Stderr🔗

You can print to stdout and stderr using the IO.println and IO.eprintln functions, respectively. Just like any other language, the ln is used to add a newline at the end of the output.

def printToStdout : IO Unit := do
  IO.print "This is printed to stdout without a newline."
  IO.println "This is printed to stdout with a newline."

def printToStderr : IO Unit := do
  IO.eprint "This is printed to stderr without a newline."
  IO.eprintln "This is printed to stderr with a newline."

Fun Example: Overwriting and Flushing🔗

By default, standard output is often "line-buffered," meaning Lean won't actually show the text in your terminal until it sees a newline (\n) or the buffer is full. If you want to show a prompt or a progress message without a newline, you should manually flush the buffer.

Using the carriage return (\r) along with flush, we can create effects like progress bars or spinners that update the same line.

def showProgressBar (n: Nat) : IO Unit := do
  for i in [1:n] do
    let progress := i * 10
    let filled := String.ofList (List.replicate i '#')
    let empty := String.ofList (List.replicate (10-i) '-')
    -- \r moves the cursor back to the
    -- start of the current line
    IO.print s!"\rProgress: [{filled}{empty}] {progress}%"
    (← IO.getStdout).flush
    IO.sleep 200 -- Sleep for 200ms
  IO.println "\nTask Complete!"

def showSpinner (n: Nat) : IO Unit := do
  let spinChars := ["|", "/", "-", "\\"]
  for i in [1:n] do
    let spinChar := spinChars[i % spinChars.length]!
    IO.print s!"\rProcessing... {spinChar}"
    (← IO.getStdout).flush
    IO.sleep 100 -- 100ms is a better speed for a spinner
  IO.print "\rDone!          "
  IO.println ""


-- run `main` to see the progress bar in action like 
-- `lean --run test.lean` in your terminal.
-- def main : IO Unit := do 
--   showProgressBar 10
--   showSpinner 20

Fun Example: Using ANSI Colors and Helpers🔗

If you want to bold, italics, or add colors to the text, you can do so with ANSI escape codes. Instead of manually typing these codes every time, it's better to define a helper function.

/-- Wraps a string in ANSI escape codes for coloring. -/
def colorize (msg : String) (colorCode : String) : String :=
  s!"\x1b[{colorCode}m{msg}\x1b[0m"

def printStatus : IO Unit := do
  IO.println s!"Status: {colorize "SUCCESS" "32"}" -- Green
  IO.println s!"Status: {colorize "WARNING" "33"}" -- Yellow
  IO.println s!"Status: {colorize "FAILURE" "31"}" -- Red
  IO.println s!"Status: {colorize "BOLD" "1"}"    -- Bold

These are standard ANSI sequences; check here for a full reference.