FFI: lean_io_promise_new

Stream: lean4

[Max Nowak 🐉]

I am trying to create a promise (context: doing some wgpu bindings).
I have the following code MWE. Oddly enough, lean_io_promise_new does return something, but it doesn't seem to return a valid lean object, since the tag is 0, so I am confused. I expect the tag to be 252, which is a LeanTask. What's the proper way to create a promise in FFI?

There are functions for managing tasks in lean.h, which work and I can spawn a lean task object with the 252 tag.
But lean_io_promise_new is from the runtime, not from lean.h, so maybe that breaks things in some way. Is there a reason why lean.h doesn't have functions for managing promises?

import Alloy.C
open scoped Alloy.C
open IO

alloy c section
  #include <stdio.h>
  #include <stdlib.h>
  #include <lean/lean.h>

  -- hacky. Copied from the compiled output from lean runtime, search `lean_io_promise_new` in the lean4 repo source.
  extern lean_object* lean_io_promise_new(lean_object* seemsNotUsed);
  extern lean_object* lean_io_promise_resolve(lean_object* value, lean_object* promise, lean_object* seemsNotUsed);
end

alloy c extern
def foo : IO (Promise UInt32) := {
  lean_object *promise = lean_io_promise_new(lean_box(1337)); -- call Promise.new
  fprintf(stderr, "promise tag is %d\n", lean_ptr_tag(promise));
  if (lean_ptr_tag((lean_object*) promise) != LeanTask) {
    abort();
  }
  fprintf(stderr, "checkpoint\n");
  return lean_io_result_mk_ok(promise);
}

And then in another file:

import TheAboveFile

def main : IO Unit := do
  let p : Promise UInt32 <- foo
  eprintln s!"got {p.result.get}"

[Eric Wieser]

lean_io_promise_new returns an docs#EStateM.Result, I think?

[Eric Wieser]

So you need to unpack that to get at the task

[Eric Wieser]

You probably want to call get_io_result?

[Max Nowak 🐉]

The signature is the following, which doesn't mention Result. Whatever it returns, shouldn't it still return a valid lean object though? The tag 0 doesn't seem to denote any valid lean object.

@[extern "lean_io_promise_new"]
opaque Promise.new [Nonempty α] : BaseIO (Promise α)

get_io_result is a c++ thing in the runtime and not tagged extern :/

[Max Nowak 🐉]

Ohhh wait I think you are right, it's just called differently in lean.h

[Max Nowak 🐉]

Yep the following works. Awesome. Thanks.

  lean_object *io_res = lean_io_promise_new(lean_box(1337)); -- call Promise.new
  lean_object *promise = lean_io_result_get_value(io_res);

[Eric Wieser]

The signature is the following, which doesn't mention Result.

It returns BaseIO, which is

-- fun α => IO.RealWorld → EStateM.Result Empty PUnit.{1} α
#reduce BaseIO

[Eric Wieser]

I think this means that lean_io_promise_new is incorrect, and should take an extra (ignored) IO.RealWorld argument?

[Max Nowak 🐉]

Yeah that's what I thought as well, but if you look at the generated C code, it only takes one lean_object. And this way I do get a closure back, so it works.

[Max Nowak 🐉]

Great success!

def triangle : IO Unit := do
  let desc <- WGPUInstanceDescriptor.mk
  let inst <- WGPUInstance.mk desc
  let adapter : Promise WGPUAdapter <- WGPUAdapter.mk inst
  eprintln "created adapter promise!"
  dostuff adapter.result.get

[Eric Wieser]

Ah nevermind; what I meant is that you should be using lean_io_promise_new(io_mk_world())

[Max Nowak 🐉]

Ah yeah. But it’s irrelevant because the argument is entirely ignored.

[Max Nowak 🐉]

Thanks for you help!

[Henrik Böving]

Eric Wieser said:

Ah nevermind; what I meant is that you should be using lean_io_promise_new(io_mk_world())

Usually we just use the world argument that we get passed in over the FFI boundary

[Eric Wieser]

What does that look like in alloy?

[Henrik Böving]

Good question actually. @Mac Malone did you think about that?

[Mac Malone]

Henrik Böving said:

Usually we just use the world argument that we get passed in over the FFI boundary

While one might think you would do this (and did at first as well), Lean C code usually just creates a new world rather than reusing the old. Part of the reason is that a world is just the scalar 1 (box(0)).

[Mac Malone]

Henrik Böving said:

Mac Malone did you think about that?

Unnamed arguments (such as the embedded in BaseIO) are named by their numerical index. In this case, it would be _0.