You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
We currently link lean and leanpkg statically (as much as possible), which makes for very simple distribution. Interestingly, we can still dlsym symbols from these executables for use in the interpreter, but this does come with some caveats on specific platforms. Additionally, we are regularly hitting the maximum number of symbols exportable from a Windows DLL/PE (2^16). If we want to keep all (relevant) symbols reachable from the interpreter, we should partition the Lean & C++ code into reasonably-sized shared libraries, which will also reduce code duplication between lean and leanpkg (and potential future executables).
The text was updated successfully, but these errors were encountered:
We currently link
lean
andleanpkg
statically (as much as possible), which makes for very simple distribution. Interestingly, we can stilldlsym
symbols from these executables for use in the interpreter, but this does come with some caveats on specific platforms. Additionally, we are regularly hitting the maximum number of symbols exportable from a Windows DLL/PE (2^16). If we want to keep all (relevant) symbols reachable from the interpreter, we should partition the Lean & C++ code into reasonably-sized shared libraries, which will also reduce code duplication betweenlean
andleanpkg
(and potential future executables).The text was updated successfully, but these errors were encountered: