segfaults in SnapshotTree.waitAll.go

Stream: lean4

[Kim Morrison]

I have a little weekend project in which I'm generating very large proof objects.

To keep things sane I am using abstractProof a lot (e.g. 10s of thousands of times).

Things were going well until I started getting segfaults, which I have tracked down (via lldb) to

* thread #10, stop reason = EXC_BAD_ACCESS (code=2, address=0x173e63ff0)
  * frame #0: 0x000000010be2224c libleanshared.dylib`l___private_Lean_Language_Basic_0__Lean_Language_SnapshotTree_waitAll_go___lam__0

(the full backtrace here has 160,000 frames!)

The relevant function is:

/-- Returns a task that waits on all snapshots in the tree. -/
partial def SnapshotTree.waitAll : SnapshotTree → BaseIO (Task Unit)
  | mk _ children => go children.toList
where
  go : List (SnapshotTask SnapshotTree) → BaseIO (Task Unit)
    | [] => return .pure ()
    | t::ts => BaseIO.bindTask (sync := true) t.task fun t => go (t.children.toList ++ ts)

Any advice?

• Do we really need these snapshots? Can I avoid them somehow?
• Could waitAll.go be changed in order to be less prone to the segfault?

I think I can probably change my design to call abstractProof less often, but still often enough, so I'll try that in the meantime.

[Sebastian Ullrich]

Setting Elab.async to false should work I think?

[Kim Morrison]

Hmm... I think I am benefitting from that, however.

I've successfully reduced the density of abstractProof, and got the proof over the line.