RFC: .h header files should be generated alongside the .c source files

[eric-wieser]

Proposal

When working with the Lean FFI, the user is instructed to add code along the lines of

#ifdef __cplusplus
extern "C" {
#endif
void lean_initialize_runtime_module();
void lean_initialize();
lean_object * initialize_A_B(uint8_t builtin, lean_object *);
lean_object * initialize_C(uint8_t builtin, lean_object *);
#ifdef __cplusplus
}
#endif

If the user additionally has functions like

@[export lean_foo]
def foo (x : String) : IO Unit := pure ()
@[extern "lean_bar"]
def bar (x : @& String) : IO Unit := pure ()

then they have to write

#ifdef __cplusplus
extern "C" {
#endif
lean_object* lean_foo(lean_object* x, lean_object*);
lean_object* lean_bar(lean_object* x, lean_object*);
#ifdef __cplusplus
}
#endif

even though a similar line is already present in the generated .c file.

These declarations should go where any standard C declarations go; in a .h header file, so that the user does not have to guess the right signature themselves. In the case of bar`, which the user must implement themselves anyway, this will result in an error message at compile time if the user implements the wrong signature by accident, rather than a crash at runtime.

An optional extension of this would be to generate C++-enabled header files like

#ifdef __cplusplus
extern "C" {
lean::obj_res lean_foo(lean::obj_arg x, lean::obj_arg);
lean::obj_res lean_bar(lean::b_obj_arg x, lean::obj_arg);
}
#else
lean_object* lean_foo(lean_object* x, lean_object*);
lean_object* lean_bar(lean_object* x, lean_object*);
#endif

which also captures the @& borrow information.

Community Feedback

Ideas should be discussed on the Lean Zulip prior to submitting a proposal. Summarize all prior discussions and link them here.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[Kha]

Do you have a suggestion for how these headers would be found by external compilers?

[digama0]

there could be an include/ directory inside .lake/build

[ydewit]

(sorry, I misunderstood context of this issue)