@[extern lean_gcc_jit_context_compile]

opaque LeanGccJit.Core.Context.compile : LeanGccJit.Core.Context → IO LeanGccJit.Core.Result

Compile the given context and load in into a binary module wrapped in a Result.

@[extern lean_gcc_jit_result_get_code]

opaque LeanGccJit.Core.Result.getCode : LeanGccJit.Core.Result → String → IO USize

Get the address of a function inside the compiled Result.

@[extern lean_gcc_jit_result_get_function]

opaque LeanGccJit.Core.Result.getFunction! {α : Type} [Nonempty α] (res : LeanGccJit.Core.Result) (name : String) (arity : Nat) : IO α

Wrap a function address to a closure. The closure type is specified by user.

Example

let func : IO Unit ← res.getFunction! "jit_entry_point" 1

Safety

This function must be used with care. It is up to the user's responsibility to ensure that target function conforms the Lean4's Uniform ABI (that is, roughly, inputs and outputs are boxed). Notice that apart from normal function types, IO α, as shown in the example above, can also be used as the a closure that takes a RealWorld as an input.

@[extern lean_gcc_jit_result_get_global]

opaque LeanGccJit.Core.Result.getGlobal : LeanGccJit.Core.Result → String → IO USize

Get the address of a global variable inside the compiled Result. One way to access the data behind the address is to use some self-defined inline C code.

@[extern lean_gcc_jit_result_release]

opaque LeanGccJit.Core.Result.release : LeanGccJit.Core.Result → IO PUnit

Unload and release the memory resource associated with the compiled Result.

Safety

It is up to the user's responsibility to ensure that the Result and also the symbols/functions inside it are not used after calling this function.