Function leanpy_keep_alive

LeanPy/native/python_bridge.c:35–44

* Called from Lean @[extern "leanpy_keep_alive"] to force the compiler * to treat the parameter as owned (consumed). The function simply * decrements the refcount (consuming the owned reference) and returns * IO.ok (). Without this, the Lean compiler's borrowing inference may * make @[export] functions borrow arguments instead of consuming them, * which breaks Python's FFI assumption that all

 * which breaks Python's FFI assumption that all parameters are owned.
 */
LEAN_EXPORT lean_obj_res leanpy_keep_alive(lean_obj_arg x, lean_obj_arg w) {
#ifdef LEANPY_RC_DEBUG
    if (!lean_is_scalar(x)) {
        fprintf(stderr, "[keepAlive] ptr=%p m_rc=%d tag=%u  -> dec\n",
                (void*)x, (int)x->m_rc, (unsigned)lean_ptr_tag(x));
    }
#endif
    lean_dec(x);
    return lean_io_result_mk_ok(lean_box(0));
}

/*
 * Debug helper: read the m_rc of a lean_object* passed from Python.