IO operations inside callbacks invoked from C?

Stream: lean4

[Kiran]

I'm writing some bindings in Lean. I'd like to provide functionality for the user to supply callbacks that will eventually be called from C but have IO operations inside them:

lean_obj_res lean_test(lean_object *obj) {
  printf("calling lean test!\n");
  lean_object *result = lean_apply_1(obj,  lean_mk_string("hello"));
  printf("lean apply worked!\n");
  lean_dec_ref(result);
  return lean_io_result_mk_ok(lean_box(0));
}

with the corresponding binding:

@[extern "lean_test"]
opaque test : (String -> IO Unit) -> IO Unit

however, when I run this:

 def main : IO Unit := do
     test (fun s => do println! "message is {s}")

nothing gets printed.

Am I doing something wrong?

[Kiran]

Ah, figured it out, I needed to appy2, and pass in a world:

lean_object *result = lean_apply_2(obj, lean_mk_string("hello"), lean_io_mk_world());