lean_dbg_trace

Stream: lean4

[Marcus Rossel]

What's the correct way to call lean_dbg_trace? I've only managed to get garbage output or crashes. I'm especially confused about what the fn parameter is for.

[Mario Carneiro]

that's the C counterpart to the dbgTrace function, used like this:

#eval show IO _ from do
  let n ← (← IO.mkRef 5).get
  let y := dbgTrace "y is evaluated" fun _ => n + 1
  let x := dbgTrace "x is evaluated" fun _ =>
    (dbgTrace "n is evaluated" fun _ => n) + 1
  println! x

x is evaluated
n is evaluated
6

[Mario Carneiro]

You can use this to see in what order things are evaluated, or whether they are evaluated at all; because it is considered a pure function by the compiler you can use it to tell when a computation is optimized out

[Mario Carneiro]

The reason for the thunk in the first argument is to sequence it before the body computation (note that x is evaluated comes before n is evaluated)

[Mario Carneiro]

if you want to call lean_dbg_trace from C code, you probably don't need the sequencing behavior, so you can just pass fun _ => () to the function and ignore the result. But you do have to pass a function which can be called by lean_apply_1, the usual way to do this from C is to use lean_alloc_closure(&thunk, 1, 0) where &thunk is a pointer to lean_object * thunk(lean_object *) { return lean_box(0); }