RFC: Exported `lean.h` symbols

Proposal

Many of the most important functions in src/include/lean/lean.h are sensibly declared inline for performance. However, this means that they do not export symbols in the leanshared dynamically-linked library. In order to write @[extern] functions, it is essential that the external code can construct Lean objects with lean_alloc_small_object, lean_alloc_ctor, and lean_alloc_array, access data from objects with lean_ctor_get, and manipulate reference counting with lean_inc_ref and lean_dec_ref. In each of these cases, the functions are inaccessible.

The current workaround is to copy and transpile the needed inline functions from lean.h into the target language. This is done in lean-sys and Canonical. This works in some cases but has a number of issues:

1. The FFI binaries no longer work for users when updates to these inline functions are made, even if the signature stays consistent.
2. Developers must update the transpiled code to consistently mirror changes, such as the switch to mimalloc coming in v4.19.0.
3. Developers must make assumptions about how preprocessor directives will be evaluated for the user's compiled version of Lean, and bake that into their FFI binary as well. If the user's configuration does not meet the assumption, the binary will not work.
4. Discrepancies in how different languages represent and allocate structures and primitives can lead to (platform dependent) issues that are complex to debug.

I am suggesting the following simple change: For each inline function f in src/include/lean/lean.h, add

LEAN_EXPORT [type] f_export([args]) { return f([args]); }

to declare an exported version of f. These functions should not be used by Lean internally, but rather make these functions accessible to programs linking with the leanshared dynamically-linked library. The primary beneficiaries are:

1. Users of FFI programs, like lean-cvc5 and CanonicalLean, who continue using the same binaries across updates.
2. Developers of FFI programs, who can rely on stable bindings for essential functions.
3. Maintainers of transpiled versions of lean.h.

As a further comment, I noticed that these most common symbols are placed in Init_shared.dll instead of leanshared.dll on Windows. While I am fine with adding a special build rule for this platform (although, it would be nice for this to be documented), I am curious about why some symbols needed to be moved and why, of all symbols, these most common ones were moved.

Community Feedback

It was recommended that I submitted an RFC after explaining this issue to Sebastian Ullrich in private communications. I made a public thread about the topic, with the only comment being that the symbols would not necessarily have a guarantee of being stable (naturally).

Start with src/include/lean/lean.h and inspect the inline functions named in the proposal, then trace how leanshared and Init_shared.dll are built on Windows. Review the linked FFI examples and existing symbol-generation or build rules. Done means the export approach and platform placement are resolved and documented well enough for FFI users to rely on it.