Debugging infinite loops

Stream: general

[Oliver Flatt]

Newbie question here- how should I run lake build so I can see debug printouts while running? Small example:

partial def infiniteInc : Nat → Nat
  | n =>
    dbg_trace "Iteration {n}"
    infiniteInc (n + 1)


#eval infiniteInc 0

I only get the print outs at the end after the stack overflow

[Andrés Goens]

I don't know if that's really possible, I imagine from playing around with your example that dbg_trace collects the string while executing it and only prints it once the execution ended...

I don't know if this works for your use case, but one common way to deal with potentially non-terminating functions could be using "fuel", another parameter that stops execution if you run out of it. Something like:

def infiniteIncFuel (fuel : Nat) : Nat → Nat :=
  match fuel with
    | 0 => fun n => n
    | .succ fuel' => fun n =>
        dbg_trace "Iteration {n}"
        infiniteIncFuel fuel' (n + 1)

#eval infiniteIncFuel 10 0
/-
Iteration 0
Iteration 1
Iteration 2
Iteration 3
Iteration 4
Iteration 5
Iteration 6
Iteration 7
Iteration 8
Iteration 9
10
-/

[Oliver Flatt]

That's unfortunate, thanks for the advice!