runtime support for platform specific code

Stream: lean4

[Yuri]

More specifically, I want to be able to load dynamic libraries in Lean code on multiple platforms.

My understanding so far:

• Runtime source code is located in lean4/src/include and lean4/src/runtime.
• Compiled code only needs to #import <lean/lean.h> (I did not find any code in Lean4 sources using lean/lean_gmp.h).
• leanc will link the libLeanc.a library when building an executable (this is not shown by lake build -v).

In the runtime code, I see two platform-specific macros:

• Windows: LEAN_WINDOWS
• Emscripten (WASM): LEAN_EMSCRIPTEN
• *nix: not(LEAN_WINDOWS)

There are two places in the compiler sources that already provide this functionality for Windows and non-Windows, but these are not available at runtime, so they are not useful for me at this point.

What are the plans going forward?

I see two options from here:

A) (Tactical) Add this functionality to the runtime. We could argue that specifically loading shared libraries is core enough that it should live in the runtime (I am happy to add that if desired), but this solution obviously does not scale since the runtime will end up being a garbage can for everything that needs a cross-platform API.

B) (Likely long-term plan) Another option is to expose platform-specific flags to the Lean code so that anyone could add cross-platform code as Lake packages outside of core Lean.

My workaround for now is to add a C shim that relies on LEAN_WINDOWS and not(LEAN_WINDOWS) to load libraries and expose that to my Lean code using standard Lean FFI.

I could just use the workaround above and go about my business, but I am curious about the longer-term direction here and, if possible, align efforts.

At this point, I am going ahead with creating something like the libloading crate from Rust. At least, this could be useful to the broader community. First, using the FFI workaround and then migrate to the long term solution once in place.

Thanks,

[Mac Malone]

docs#Lean.loadDynlib

[Mac Malone]

(Is that what you are looking for?)

[Yuri]

Hi, @Mac Malone, thanks for the nudge.

I did see loadDynlib, but I wrongly assumed it was not available at runtime. I should have double checked. Let me see if that is enough for my needs.

thanks,