alexf91 / lean4-ctypes

FFI for Lean 4
Apache License 2.0
3 stars 0 forks source link

Assigning arguments to a reference produces segfault #12

Closed alexf91 closed 8 months ago

alexf91 commented 8 months ago

See testCallClosureSegfault testcase added in b4bf5fd. The error is not directly caused by the assignment or reading the reference, but in another testcase.

alexf91 commented 8 months ago

The problem doesn't seem to be caused by references, but somewhere else. See the second testcase that causes the same problem.

Deleting the closure causes the problem.

alexf91 commented 8 months ago

Closed for now. The error still exists, but it's likely more broad then described here. Not calling lean_dec() in the destructor of the Callback class avoids it, but then we keep callbacks alive when they are not needed anymore.