RFC: Stable lean.h symbols

Stream: general

[Chase Norman]

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.

[Henrik Böving]

I think you are asking for two things here. For one access to symbols that are currently only available as static inline. And secondly stability guarantees for these symbols. I think it is somewhat realistic to have the former but the Lean runtime is far away from a state where it would be stable enough to make guarantees for the functions available in lean.h I would say.