profiling execution

Stream: new members

[tzlil]

i have this code

unsafe def main : IO Unit := do
  let n := 5
  let b := @Board.Initial n
  let rec grundy (b : Board n) (ref : IO.Ref (Std.HashMap (Board n) ℕ)) : IO ℕ := do
    let hm ← ref.get
    match hm[b]? with
    | some r => return r -- already computed this one
    | none => do
      let m ← @(legalMoves b).traverse _ _ _ _ sorry _ (grundy · ref)
      let t := @Nat.find (fun n => n ∉ m) _ sorry
      ref.modify (Std.HashMap.alter · b (fun _ => some t))
      return t

  let ref ← IO.mkRef (@Std.HashMap.emptyWithCapacity (Board n) ℕ _ _ (2 ^ (n*n)))

  let _ ← grundy b ref
  let hm ← ref.get
  let _ ← @(legalMoves b).traverse _ _ _ _ sorry _ fun b => do
    IO.println s!"{repr b} has measure {Move.Measure b} and grundy value {hm[b]!}"

which really should not take too long, but it takes almost 100 seconds to run just for 5x5, the mex should only be computed ~33 million times, how do i profile this and figure out whats taking the most time? my best guess is legalMoves which is implemented using Fintype.elems, but maybe im just using iorefs in a bad way or hashmap not linearly or some other way im not aware of, i could only find flags for profiling the elaboration and typechecking and not the runtime of the binary itself

[pandaman]

Regular C profilers work well with Lean executables.
I use samply to profile Lean programs for example.