controlling compiled C code

Stream: lean4

[Bhakti Shah]

This is a very convoluted question so my apologies if it isn't formulated the most clearly / in the best way. Happy to provide more details, there's just a lot going on and I'm not sure what would be useful information.

I need to be able to call functions in the C code that my Lean code compiles to. Unfortunately it seems quite unreadable and unworkable. I technically only need a function signature that looks like C code, but the only function that has a remotely useful signature is my main function that is the entry point for a binary executable, which is just int main(int argc, char ** argv), compiled from the lean signature def main (args : List String) : IO Unit. I need to externally call a function that returns a value. All functions except this main function are compiled into a weird signature that returns a lean_object*, even if the type I'm using in lean is a primitive type.

is there a way to either a) make a function excluding the main function have a readable C-like signature, so it can be called relatively normally in code; or b) have the main function explicitly return a value via the lean code that isn't just the C exit code?

for a bit more context the C code I'm working with is the one that is found in build/ir after compilation (i hope this is the right code to use because I couldn't really find any documentation or any other ways to extract it)

thank you!

[Mac Malone]

@Bhakti Shah Some notes:

1. Some details on translating between C and Lean can be found in the Lean 4 manual.
2. Lean only has a few primitive types: UInt8/16/31/64, USize, Char, and Float, which are uint8/16/32/64_t, size_t, uint32_t, and double, respectively. Also, structures with a single (non-Prop) primitive field are that primitive type, and enum-like inductives (e.g., inductive Color | red | blue | green) are smallest of uint8/16/32/64_t which is sufficient to contain the number of constructors. All other types are boxed (i.e., lean_object*).
3. You can give a Lean definition a clean, human-readable C symbol name via the @[export] attribute. For example:

@[export my_add] def myLeanAdd (a b : UInt32) : UInt32 := a + (a + b)

Will produce essentially the C function:

uint32_t my_add(uint32_t a, uint32_t b) {
  return lean_uint32_add(a, lean_uint32_add(a,b));
}

[Jason Rute]

Does (3) mean that Lean 4 has code extraction to (nice) C or C++ code. Someone asked me about this recently and I told them that Lean doesn’t have the ability to extract (nice) code from Lean functions.

[Tomas Skrivan]

I have successfully used lean generated code in C++ project. To exchange more complicated objects use lean_external_object. Have a look at this example project https://github.com/leanprover/lean4/tree/17602d9f2844566a4ea496f989c37afc8115f35f/tests/compiler/foreign

[James Gallicchio]

Jason Rute said:

Does (3) mean that Lean 4 has code extraction to (nice) C or C++ code.

Not sure how Lean compilation compares to Agda/Coq code extraction, but Lean has a pretty specific ABI as laid out in the FFI section of the manual. So the generated C code is usually easy to interact with, and the interface is very stable across Lean versions (assuming the Lean signature remains stable).

[Bhakti Shah]

thank you very much! i wasn't aware of the FFI documentation