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 :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: 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]

For what is worth, I have hit the same issue when creating the libclang-shim. Basically, the current instructions do not scale for larger shims exactly because of this lack of .c and .h separation.

This is the path I took:

First, I place .c and .h alongside .lean files. So for a Clang/CXString.lean file, I also have a Clang/CXString.shim.c and Clang/CXString.shim.h. This keeps shim and lean files together and helps avoid a separate folder structure getting out of sync ending up a pile of .c and .h without structure. Besides, when creating FFI shims it is usually a good idea to keep the FFI code (.lean + .c/.h) as a separate project/library so that it can be reused.

Then I have a bit of lake-foo to automatically process these .h and .c files:

import Lake
open Lake DSL

package "libclang" where
  srcDir := "src"
  buildType := BuildType.debug
  moreLinkArgs := #[
    "-L/nix/store/rf4rw53zl322zj1jnbnyqvi9dxhndjwi-clang-16.0.6-lib/lib",
    "-lclang"
  ]

require leanffi from "../lean-ffi"

module_data shim.c.o.export : BuildJob FilePath
module_data shim.c.o.noexport : BuildJob FilePath

lean_lib "Clang" where
  buildType := BuildType.debug
  nativeFacets := (#[Module.oExportFacet, if · then `shim.c.o.export else `shim.c.o.noexport])

@[default_target]
lean_exe "libclang" where
  buildType := BuildType.debug
  root := `Main

The alternative was to have a humongous .c file with all the libclang functions.

It has been working well for me and I have been it anger in the libclang project.