doc: add note on Lake changes to RELEASE.md

.github/workflows/ci.yml

@@ -141,12 +141,10 @@ jobs:
                 "shell": "msys2 {0}",
                 "CMAKE_OPTIONS": "-G \"Unix Makefiles\" -DUSE_GMP=OFF",
                 // for reasons unknown, interactivetests are flaky on Windows
-                // also, the liasolver test hits “too many exported symbols”
-                "CTEST_OPTIONS": "--repeat until-pass:2 -E 'leanbenchtest_liasolver.lean'",
+                "CTEST_OPTIONS": "--repeat until-pass:2",
                 "llvm-url": "https://github.com/leanprover/lean-llvm/releases/download/15.0.1/lean-llvm-x86_64-w64-windows-gnu.tar.zst",
                 "prepare-llvm": "../script/prepare-llvm-mingw.sh lean-llvm*",
-                // TEMP while compiler tests are deactivated
-                "binary-check": "true"
+                "binary-check": "ldd"
               },
               {
                 "name": "Linux aarch64",

RELEASES.md

@@ -11,6 +11,12 @@ of each version.
 v4.8.0 (development in progress)
 ---------
 
+* **Executables configured with `supportInterpreter := true` on Windows should now be run via `lake exe` to function properly.**
+
+  The way Lean is built on Windows has changed (see PR [#3601](https://github.com/leanprover/lean4/pull/3601)). As a result, Lake now dynamically links executables with `supportInterpreter := true` on Windows to `libleanshared.dll` and `libInit_shared.dll`. Therefore, such executables will not run unless those shared libraries are co-located with the executables or part of `PATH`. Running the executable via `lake exe` will ensure these libraries are part of `PATH`.
+
+  In a related change, the signature of the `nativeFacets` Lake configuration options has changed from a static `Array` to a function `(shouldExport : Bool) → Array`. See its docstring or Lake's [README](src/lake/README.md) for further details on the changed option.
+
 * Lean now generates an error if the type of a theorem is **not** a proposition.
 
 * Importing two different files containing proofs of the same theorem is no longer considered an error. This feature is particularly useful for theorems that are automatically generated on demand (e.g., equational theorems).

nix/buildLeanPackage.nix

@@ -176,7 +176,7 @@ with builtins; let
       # make local "copy" so `drv`'s Nix store path doesn't end up in ccache's hash
       ln -s ${drv.c}/${drv.cPath} src.c
       # on the other hand, a debug build is pretty fast anyway, so preserve the path for gdb
-      leanc -c -o $out/$oPath $leancFlags -fPIC ${if debug then "${drv.c}/${drv.cPath} -g" else "src.c -O3 -DNDEBUG"}
+      leanc -c -o $out/$oPath $leancFlags -fPIC ${if debug then "${drv.c}/${drv.cPath} -g" else "src.c -O3 -DNDEBUG -DLEAN_EXPORTING"}
     '';
   };
   mkMod = mod: deps:

src/CMakeLists.txt

@@ -503,13 +503,13 @@ file(RELATIVE_PATH LIB ${LEAN_SOURCE_DIR} ${CMAKE_BINARY_DIR}/lib)
 
 # set up libInit_shared only on Windows; see also stdlib.make.in
 if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
-  set(INIT_SHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a -Wl,--no-whole-archive -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libInit_shared.dll.a")
+  set(INIT_SHARED_LINKER_FLAGS "-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libInit.a.export ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a -Wl,--no-whole-archive -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libInit_shared.dll.a")
 endif()
 
 if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
   set(LEANSHARED_LINKER_FLAGS "-Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libInit.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libLean.a -Wl,-force_load,${CMAKE_BINARY_DIR}/lib/lean/libleancpp.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
 elseif(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
-  set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lLean -lleancpp -Wl,--no-whole-archive -lInit_shared -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a")
+  set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libLean.a.export -lleancpp -Wl,--no-whole-archive -lInit_shared -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libleanshared.dll.a")
 else()
   set(LEANSHARED_LINKER_FLAGS "-Wl,--whole-archive -lInit -lLean -lleancpp -Wl,--no-whole-archive ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LEANSHARED_LINKER_FLAGS}")
 endif()

src/Leanc.lean

@@ -33,7 +33,8 @@ Interesting options:
     | none   => #[("MACOSX_DEPLOYMENT_TARGET", "99.0")]
 
   -- let compileOnly := args.contains "-c"
-  let linkStatic := !args.contains "-shared"
+  let linkStatic := !(args.contains "-shared" || args.contains "-leanshared")
+  let args := args.erase "-leanshared"
 
   -- We assume that the CMake variables do not contain escaped spaces
   let cflags := getCFlags root

src/include/lean/lean.h

@@ -50,17 +50,15 @@ void lean_notify_assert(const char * fileName, int line, const char * condition)
 #endif
 #endif
 
+// We set `LEAN_EXPORTING` when compiling objects of libleanshared, but not when including this header in any other context.
+#ifdef LEAN_EXPORTING
 #ifdef _WIN32
 #define LEAN_EXPORT __declspec(dllexport)
 #else
 #define LEAN_EXPORT __attribute__((visibility("default")))
 #endif
-
-// We set `LEAN_EXPORTING` when compiling objects of libleanshared, but not when including this header in any other context.
-#if defined LEAN_EXPORTING
-#define LEAN_SHARED LEAN_EXPORT
 #else
-#define LEAN_SHARED
+#define LEAN_EXPORT
 #endif
 
 #define LEAN_BYTE(Var, Index) *(((uint8_t*)&Var)+Index)
@@ -276,7 +274,7 @@ typedef struct {
     lean_external_foreach_proc  m_foreach;
 } lean_external_class;
 
-LEAN_SHARED lean_external_class * lean_register_external_class(lean_external_finalize_proc, lean_external_foreach_proc);
+LEAN_EXPORT lean_external_class * lean_register_external_class(lean_external_finalize_proc, lean_external_foreach_proc);
 
 /* Object for wrapping external data. */
 typedef struct {
@@ -289,16 +287,16 @@ static inline bool lean_is_scalar(lean_object * o) { return ((size_t)(o) & 1) ==
 static inline lean_object * lean_box(size_t n) { return (lean_object*)(((size_t)(n) << 1) | 1); }
 static inline size_t lean_unbox(lean_object * o) { return (size_t)(o) >> 1; }
 
-LEAN_SHARED void lean_set_exit_on_panic(bool flag);
+LEAN_EXPORT void lean_set_exit_on_panic(bool flag);
 /* Enable/disable panic messages */
-LEAN_SHARED void lean_set_panic_messages(bool flag);
+LEAN_EXPORT void lean_set_panic_messages(bool flag);
 
-LEAN_SHARED lean_object * lean_panic_fn(lean_object * default_val, lean_object * msg);
+LEAN_EXPORT lean_object * lean_panic_fn(lean_object * default_val, lean_object * msg);
 
-LEAN_SHARED __attribute__((noreturn)) void lean_internal_panic(char const * msg);
-LEAN_SHARED __attribute__((noreturn)) void lean_internal_panic_out_of_memory(void);
-LEAN_SHARED __attribute__((noreturn)) void lean_internal_panic_unreachable(void);
-LEAN_SHARED __attribute__((noreturn)) void lean_internal_panic_rc_overflow(void);
+LEAN_EXPORT __attribute__((noreturn)) void lean_internal_panic(char const * msg);
+LEAN_EXPORT __attribute__((noreturn)) void lean_internal_panic_out_of_memory(void);
+LEAN_EXPORT __attribute__((noreturn)) void lean_internal_panic_unreachable(void);
+LEAN_EXPORT __attribute__((noreturn)) void lean_internal_panic_rc_overflow(void);
 
 static inline size_t lean_align(size_t v, size_t a) {
     return (v / a)*a + a * (v % a != 0);
@@ -310,10 +308,10 @@ static inline unsigned lean_get_slot_idx(unsigned sz) {
     return sz / LEAN_OBJECT_SIZE_DELTA - 1;
 }
 
-LEAN_SHARED void * lean_alloc_small(unsigned sz, unsigned slot_idx);
-LEAN_SHARED void lean_free_small(void * p);
-LEAN_SHARED unsigned lean_small_mem_size(void * p);
-LEAN_SHARED void lean_inc_heartbeat(void);
+LEAN_EXPORT void * lean_alloc_small(unsigned sz, unsigned slot_idx);
+LEAN_EXPORT void lean_free_small(void * p);
+LEAN_EXPORT unsigned lean_small_mem_size(void * p);
+LEAN_EXPORT void lean_inc_heartbeat(void);
 
 #ifndef __cplusplus
 void * malloc(size_t);  // avoid including big `stdlib.h`
@@ -379,8 +377,8 @@ static inline void lean_free_small_object(lean_object * o) {
 #endif
 }
 
-LEAN_SHARED lean_object * lean_alloc_object(size_t sz);
-LEAN_SHARED void lean_free_object(lean_object * o);
+LEAN_EXPORT lean_object * lean_alloc_object(size_t sz);
+LEAN_EXPORT void lean_free_object(lean_object * o);
 
 static inline uint8_t lean_ptr_tag(lean_object * o) {
     return o->m_tag;
@@ -395,7 +393,7 @@ static inline unsigned lean_ptr_other(lean_object * o) {
    All constructor objects are "small", and allocated into pages.
    We retrieve their size by accessing the page header. The size of
    small objects is a multiple of LEAN_OBJECT_SIZE_DELTA */
-LEAN_SHARED size_t lean_object_byte_size(lean_object * o);
+LEAN_EXPORT size_t lean_object_byte_size(lean_object * o);
 
 static inline bool lean_is_mt(lean_object * o) {
     return o->m_rc < 0;
@@ -418,8 +416,8 @@ static inline _Atomic(int) * lean_get_rc_mt_addr(lean_object* o) {
     return (_Atomic(int)*)(&(o->m_rc));
 }
 
-LEAN_SHARED void lean_inc_ref_cold(lean_object * o);
-LEAN_SHARED void lean_inc_ref_n_cold(lean_object * o, unsigned n);
+LEAN_EXPORT void lean_inc_ref_cold(lean_object * o);
+LEAN_EXPORT void lean_inc_ref_n_cold(lean_object * o, unsigned n);
 
 static inline void lean_inc_ref(lean_object * o) {
     if (LEAN_LIKELY(lean_is_st(o))) {
@@ -437,7 +435,7 @@ static inline void lean_inc_ref_n(lean_object * o, size_t n) {
     }
 }
 
-LEAN_SHARED void lean_dec_ref_cold(lean_object * o);
+LEAN_EXPORT void lean_dec_ref_cold(lean_object * o);
 
 static inline void lean_dec_ref(lean_object * o) {
     if (LEAN_LIKELY(o->m_rc > 1)) {
@@ -451,7 +449,7 @@ static inline void lean_inc_n(lean_object * o, size_t n) { if (!lean_is_scalar(o
 static inline void lean_dec(lean_object * o) { if (!lean_is_scalar(o)) lean_dec_ref(o); }
 
 /* Just free memory */
-LEAN_SHARED void lean_dealloc(lean_object * o);
+LEAN_EXPORT void lean_dealloc(lean_object * o);
 
 static inline bool lean_is_ctor(lean_object * o) { return lean_ptr_tag(o) <= LeanMaxCtorTag; }
 static inline bool lean_is_closure(lean_object * o) { return lean_ptr_tag(o) == LeanClosure; }
@@ -494,8 +492,8 @@ static inline bool lean_is_shared(lean_object * o) {
     }
 }
 
-LEAN_SHARED void lean_mark_mt(lean_object * o);
-LEAN_SHARED void lean_mark_persistent(lean_object * o);
+LEAN_EXPORT void lean_mark_mt(lean_object * o);
+LEAN_EXPORT void lean_mark_persistent(lean_object * o);
 
 static inline void lean_set_st_header(lean_object * o, unsigned tag, unsigned other) {
     o->m_rc       = 1;
@@ -652,25 +650,25 @@ static inline void lean_closure_set(u_lean_obj_arg o, unsigned i, lean_obj_arg a
     lean_to_closure(o)->m_objs[i] = a;
 }
 
-LEAN_SHARED lean_object* lean_apply_1(lean_object* f, lean_object* a1);
-LEAN_SHARED lean_object* lean_apply_2(lean_object* f, lean_object* a1, lean_object* a2);
-LEAN_SHARED lean_object* lean_apply_3(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3);
-LEAN_SHARED lean_object* lean_apply_4(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4);
-LEAN_SHARED lean_object* lean_apply_5(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5);
-LEAN_SHARED lean_object* lean_apply_6(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6);
-LEAN_SHARED lean_object* lean_apply_7(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7);
-LEAN_SHARED lean_object* lean_apply_8(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8);
-LEAN_SHARED lean_object* lean_apply_9(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9);
-LEAN_SHARED lean_object* lean_apply_10(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10);
-LEAN_SHARED lean_object* lean_apply_11(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11);
-LEAN_SHARED lean_object* lean_apply_12(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12);
-LEAN_SHARED lean_object* lean_apply_13(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12, lean_object* a13);
-LEAN_SHARED lean_object* lean_apply_14(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12, lean_object* a13, lean_object* a14);
-LEAN_SHARED lean_object* lean_apply_15(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12, lean_object* a13, lean_object* a14, lean_object* a15);
-LEAN_SHARED lean_object* lean_apply_16(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12, lean_object* a13, lean_object* a14, lean_object* a15, lean_object* a16);
-LEAN_SHARED lean_object* lean_apply_n(lean_object* f, unsigned n, lean_object** args);
+LEAN_EXPORT lean_object* lean_apply_1(lean_object* f, lean_object* a1);
+LEAN_EXPORT lean_object* lean_apply_2(lean_object* f, lean_object* a1, lean_object* a2);
+LEAN_EXPORT lean_object* lean_apply_3(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3);
+LEAN_EXPORT lean_object* lean_apply_4(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4);
+LEAN_EXPORT lean_object* lean_apply_5(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5);
+LEAN_EXPORT lean_object* lean_apply_6(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6);
+LEAN_EXPORT lean_object* lean_apply_7(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7);
+LEAN_EXPORT lean_object* lean_apply_8(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8);
+LEAN_EXPORT lean_object* lean_apply_9(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9);
+LEAN_EXPORT lean_object* lean_apply_10(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10);
+LEAN_EXPORT lean_object* lean_apply_11(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11);
+LEAN_EXPORT lean_object* lean_apply_12(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12);
+LEAN_EXPORT lean_object* lean_apply_13(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12, lean_object* a13);
+LEAN_EXPORT lean_object* lean_apply_14(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12, lean_object* a13, lean_object* a14);
+LEAN_EXPORT lean_object* lean_apply_15(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12, lean_object* a13, lean_object* a14, lean_object* a15);
+LEAN_EXPORT lean_object* lean_apply_16(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5, lean_object* a6, lean_object* a7, lean_object* a8, lean_object* a9, lean_object* a10, lean_object* a11, lean_object* a12, lean_object* a13, lean_object* a14, lean_object* a15, lean_object* a16);
+LEAN_EXPORT lean_object* lean_apply_n(lean_object* f, unsigned n, lean_object** args);
 /* Pre: n > 16 */
-LEAN_SHARED lean_object* lean_apply_m(lean_object* f, unsigned n, lean_object** args);
+LEAN_EXPORT lean_object* lean_apply_m(lean_object* f, unsigned n, lean_object** args);
 
 /* Arrays of objects (low level API) */
 static inline lean_obj_res lean_alloc_array(size_t size, size_t capacity) {
@@ -703,8 +701,8 @@ static inline void lean_array_set_core(u_lean_obj_arg o, size_t i, lean_obj_arg
     assert(i < lean_array_size(o));
     lean_to_array(o)->m_data[i] = v;
 }
-LEAN_SHARED lean_object * lean_array_mk(lean_obj_arg l);
-LEAN_SHARED lean_object * lean_array_data(lean_obj_arg a);
+LEAN_EXPORT lean_object * lean_array_mk(lean_obj_arg l);
+LEAN_EXPORT lean_object * lean_array_data(lean_obj_arg a);
 
 /* Arrays of objects (high level API) */
 
@@ -736,7 +734,7 @@ static inline lean_obj_res lean_array_fget(b_lean_obj_arg a, b_lean_obj_arg i) {
     return lean_array_uget(a, lean_unbox(i));
 }
 
-LEAN_SHARED lean_obj_res lean_array_get_panic(lean_obj_arg def_val);
+LEAN_EXPORT lean_obj_res lean_array_get_panic(lean_obj_arg def_val);
 
 static inline lean_object * lean_array_get(lean_obj_arg def_val, b_lean_obj_arg a, b_lean_obj_arg i) {
     if (lean_is_scalar(i)) {
@@ -753,7 +751,7 @@ static inline lean_object * lean_array_get(lean_obj_arg def_val, b_lean_obj_arg
     return lean_array_get_panic(def_val);
 }
 
-LEAN_SHARED lean_obj_res lean_copy_expand_array(lean_obj_arg a, bool expand);
+LEAN_EXPORT lean_obj_res lean_copy_expand_array(lean_obj_arg a, bool expand);
 
 static inline lean_obj_res lean_copy_array(lean_obj_arg a) {
     return lean_copy_expand_array(a, false);
@@ -776,7 +774,7 @@ static inline lean_object * lean_array_fset(lean_obj_arg a, b_lean_obj_arg i, le
     return lean_array_uset(a, lean_unbox(i), v);
 }
 
-LEAN_SHARED lean_obj_res lean_array_set_panic(lean_obj_arg a, lean_obj_arg v);
+LEAN_EXPORT lean_obj_res lean_array_set_panic(lean_obj_arg a, lean_obj_arg v);
 
 static inline lean_object * lean_array_set(lean_obj_arg a, b_lean_obj_arg i, lean_obj_arg v) {
     if (lean_is_scalar(i)) {
@@ -821,8 +819,8 @@ static inline lean_object * lean_array_swap(lean_obj_arg a, b_lean_obj_arg i, b_
     return lean_array_uswap(a, ui, uj);
 }
 
-LEAN_SHARED lean_object * lean_array_push(lean_obj_arg a, lean_obj_arg v);
-LEAN_SHARED lean_object * lean_mk_array(lean_obj_arg n, lean_obj_arg v);
+LEAN_EXPORT lean_object * lean_array_push(lean_obj_arg a, lean_obj_arg v);
+LEAN_EXPORT lean_object * lean_mk_array(lean_obj_arg n, lean_obj_arg v);
 
 /* Array of scalars */
 
@@ -853,10 +851,10 @@ static inline uint8_t* lean_sarray_cptr(lean_object * o) { return lean_to_sarray
 
 /* ByteArray (special case of Array of Scalars) */
 
-LEAN_SHARED lean_obj_res lean_byte_array_mk(lean_obj_arg a);
-LEAN_SHARED lean_obj_res lean_byte_array_data(lean_obj_arg a);
-LEAN_SHARED lean_obj_res lean_copy_byte_array(lean_obj_arg a);
-LEAN_SHARED uint64_t lean_byte_array_hash(b_lean_obj_arg a);
+LEAN_EXPORT lean_obj_res lean_byte_array_mk(lean_obj_arg a);
+LEAN_EXPORT lean_obj_res lean_byte_array_data(lean_obj_arg a);
+LEAN_EXPORT lean_obj_res lean_copy_byte_array(lean_obj_arg a);
+LEAN_EXPORT uint64_t lean_byte_array_hash(b_lean_obj_arg a);
 
 static inline lean_obj_res lean_mk_empty_byte_array(b_lean_obj_arg capacity) {
     if (!lean_is_scalar(capacity)) lean_internal_panic_out_of_memory();
@@ -883,7 +881,7 @@ static inline uint8_t lean_byte_array_fget(b_lean_obj_arg a, b_lean_obj_arg i) {
     return lean_byte_array_uget(a, lean_unbox(i));
 }
 
-LEAN_SHARED lean_obj_res lean_byte_array_push(lean_obj_arg a, uint8_t b);
+LEAN_EXPORT lean_obj_res lean_byte_array_push(lean_obj_arg a, uint8_t b);
 
 static inline lean_object * lean_byte_array_uset(lean_obj_arg a, size_t i, uint8_t v) {
     lean_obj_res r;
@@ -913,9 +911,9 @@ static inline lean_obj_res lean_byte_array_fset(lean_obj_arg a, b_lean_obj_arg i
 
 /* FloatArray (special case of Array of Scalars) */
 
-LEAN_SHARED lean_obj_res lean_float_array_mk(lean_obj_arg a);
-LEAN_SHARED lean_obj_res lean_float_array_data(lean_obj_arg a);
-LEAN_SHARED lean_obj_res lean_copy_float_array(lean_obj_arg a);
+LEAN_EXPORT lean_obj_res lean_float_array_mk(lean_obj_arg a);
+LEAN_EXPORT lean_obj_res lean_float_array_data(lean_obj_arg a);
+LEAN_EXPORT lean_obj_res lean_copy_float_array(lean_obj_arg a);
 
 static inline lean_obj_res lean_mk_empty_float_array(b_lean_obj_arg capacity) {
     if (!lean_is_scalar(capacity)) lean_internal_panic_out_of_memory();
@@ -948,7 +946,7 @@ static inline double lean_float_array_get(b_lean_obj_arg a, b_lean_obj_arg i) {
     }
 }
 
-LEAN_SHARED lean_obj_res lean_float_array_push(lean_obj_arg a, double d);
+LEAN_EXPORT lean_obj_res lean_float_array_push(lean_obj_arg a, double d);
 
 static inline lean_obj_res lean_float_array_uset(lean_obj_arg a, size_t i, double d) {
     lean_obj_res r;
@@ -986,27 +984,27 @@ static inline lean_obj_res lean_alloc_string(size_t size, size_t capacity, size_
     o->m_length = len;
     return (lean_object*)o;
 }
-LEAN_SHARED size_t lean_utf8_strlen(char const * str);
-LEAN_SHARED size_t lean_utf8_n_strlen(char const * str, size_t n);
+LEAN_EXPORT size_t lean_utf8_strlen(char const * str);
+LEAN_EXPORT size_t lean_utf8_n_strlen(char const * str, size_t n);
 static inline size_t lean_string_capacity(lean_object * o) { return lean_to_string(o)->m_capacity; }
 static inline size_t lean_string_byte_size(lean_object * o) { return sizeof(lean_string_object) + lean_string_capacity(o); }
 /* instance : inhabited char := ⟨'A'⟩ */
 static inline uint32_t lean_char_default_value() { return 'A'; }
-LEAN_SHARED lean_obj_res lean_mk_string_from_bytes(char const * s, size_t sz);
-LEAN_SHARED lean_obj_res lean_mk_string(char const * s);
+LEAN_EXPORT lean_obj_res lean_mk_string_from_bytes(char const * s, size_t sz);
+LEAN_EXPORT lean_obj_res lean_mk_string(char const * s);
 static inline char const * lean_string_cstr(b_lean_obj_arg o) {
     assert(lean_is_string(o));
     return lean_to_string(o)->m_data;
 }
 static inline size_t lean_string_size(b_lean_obj_arg o) { return lean_to_string(o)->m_size; }
 static inline size_t lean_string_len(b_lean_obj_arg o) { return lean_to_string(o)->m_length; }
-LEAN_SHARED lean_obj_res lean_string_push(lean_obj_arg s, uint32_t c);
-LEAN_SHARED lean_obj_res lean_string_append(lean_obj_arg s1, b_lean_obj_arg s2);
+LEAN_EXPORT lean_obj_res lean_string_push(lean_obj_arg s, uint32_t c);
+LEAN_EXPORT lean_obj_res lean_string_append(lean_obj_arg s1, b_lean_obj_arg s2);
 static inline lean_obj_res lean_string_length(b_lean_obj_arg s) { return lean_box(lean_string_len(s)); }
-LEAN_SHARED lean_obj_res lean_string_mk(lean_obj_arg cs);
-LEAN_SHARED lean_obj_res lean_string_data(lean_obj_arg s);
-LEAN_SHARED uint32_t  lean_string_utf8_get(b_lean_obj_arg s, b_lean_obj_arg i);
-LEAN_SHARED uint32_t lean_string_utf8_get_fast_cold(char const * str, size_t i, size_t size, unsigned char c);
+LEAN_EXPORT lean_obj_res lean_string_mk(lean_obj_arg cs);
+LEAN_EXPORT lean_obj_res lean_string_data(lean_obj_arg s);
+LEAN_EXPORT uint32_t  lean_string_utf8_get(b_lean_obj_arg s, b_lean_obj_arg i);
+LEAN_EXPORT uint32_t lean_string_utf8_get_fast_cold(char const * str, size_t i, size_t size, unsigned char c);
 static inline uint32_t lean_string_utf8_get_fast(b_lean_obj_arg s, b_lean_obj_arg i) {
   char const * str = lean_string_cstr(s);
   size_t idx = lean_unbox(i);
@@ -1020,8 +1018,8 @@ static inline uint8_t lean_string_get_byte_fast(b_lean_obj_arg s, b_lean_obj_arg
   return str[idx];
 }
 
-LEAN_SHARED lean_obj_res lean_string_utf8_next(b_lean_obj_arg s, b_lean_obj_arg i);
-LEAN_SHARED lean_obj_res lean_string_utf8_next_fast_cold(size_t i, unsigned char c);
+LEAN_EXPORT lean_obj_res lean_string_utf8_next(b_lean_obj_arg s, b_lean_obj_arg i);
+LEAN_EXPORT lean_obj_res lean_string_utf8_next_fast_cold(size_t i, unsigned char c);
 static inline lean_obj_res lean_string_utf8_next_fast(b_lean_obj_arg s, b_lean_obj_arg i) {
   char const * str = lean_string_cstr(s);
   size_t idx = lean_unbox(i);
@@ -1030,22 +1028,22 @@ static inline lean_obj_res lean_string_utf8_next_fast(b_lean_obj_arg s, b_lean_o
   return lean_string_utf8_next_fast_cold(idx, c);
 }
 
-LEAN_SHARED lean_obj_res lean_string_utf8_prev(b_lean_obj_arg s, b_lean_obj_arg i);
-LEAN_SHARED lean_obj_res lean_string_utf8_set(lean_obj_arg s, b_lean_obj_arg i, uint32_t c);
+LEAN_EXPORT lean_obj_res lean_string_utf8_prev(b_lean_obj_arg s, b_lean_obj_arg i);
+LEAN_EXPORT lean_obj_res lean_string_utf8_set(lean_obj_arg s, b_lean_obj_arg i, uint32_t c);
 static inline uint8_t lean_string_utf8_at_end(b_lean_obj_arg s, b_lean_obj_arg i) {
     return !lean_is_scalar(i) || lean_unbox(i) >= lean_string_size(s) - 1;
 }
-LEAN_SHARED lean_obj_res lean_string_utf8_extract(b_lean_obj_arg s, b_lean_obj_arg b, b_lean_obj_arg e);
+LEAN_EXPORT lean_obj_res lean_string_utf8_extract(b_lean_obj_arg s, b_lean_obj_arg b, b_lean_obj_arg e);
 static inline lean_obj_res lean_string_utf8_byte_size(b_lean_obj_arg s) { return lean_box(lean_string_size(s) - 1); }
-LEAN_SHARED bool lean_string_eq_cold(b_lean_obj_arg s1, b_lean_obj_arg s2);
+LEAN_EXPORT bool lean_string_eq_cold(b_lean_obj_arg s1, b_lean_obj_arg s2);
 static inline bool lean_string_eq(b_lean_obj_arg s1, b_lean_obj_arg s2) {
     return s1 == s2 || (lean_string_size(s1) == lean_string_size(s2) && lean_string_eq_cold(s1, s2));
 }
 static inline bool lean_string_ne(b_lean_obj_arg s1, b_lean_obj_arg s2) { return !lean_string_eq(s1, s2); }
-LEAN_SHARED bool lean_string_lt(b_lean_obj_arg s1, b_lean_obj_arg s2);
+LEAN_EXPORT bool lean_string_lt(b_lean_obj_arg s1, b_lean_obj_arg s2);
 static inline uint8_t lean_string_dec_eq(b_lean_obj_arg s1, b_lean_obj_arg s2) { return lean_string_eq(s1, s2); }
 static inline uint8_t lean_string_dec_lt(b_lean_obj_arg s1, b_lean_obj_arg s2) { return lean_string_lt(s1, s2); }
-LEAN_SHARED uint64_t lean_string_hash(b_lean_obj_arg);
+LEAN_EXPORT uint64_t lean_string_hash(b_lean_obj_arg);
 
 /* Thunks */
 
@@ -1066,7 +1064,7 @@ static inline lean_obj_res lean_thunk_pure(lean_obj_arg v) {
     return (lean_object*)o;
 }
 
-LEAN_SHARED lean_object * lean_thunk_get_core(lean_object * t);
+LEAN_EXPORT lean_object * lean_thunk_get_core(lean_object * t);
 
 static inline b_lean_obj_res lean_thunk_get(b_lean_obj_arg t) {
     lean_object * r = lean_to_thunk(t)->m_value;
@@ -1083,22 +1081,22 @@ static inline lean_obj_res lean_thunk_get_own(b_lean_obj_arg t) {
 
 /* Tasks */
 
-LEAN_SHARED void lean_init_task_manager(void);
-LEAN_SHARED void lean_init_task_manager_using(unsigned num_workers);
-LEAN_SHARED void lean_finalize_task_manager(void);
+LEAN_EXPORT void lean_init_task_manager(void);
+LEAN_EXPORT void lean_init_task_manager_using(unsigned num_workers);
+LEAN_EXPORT void lean_finalize_task_manager(void);
 
-LEAN_SHARED lean_obj_res lean_task_spawn_core(lean_obj_arg c, unsigned prio, bool keep_alive);
+LEAN_EXPORT lean_obj_res lean_task_spawn_core(lean_obj_arg c, unsigned prio, bool keep_alive);
 /* Run a closure `Unit -> A` as a `Task A` */
 static inline lean_obj_res lean_task_spawn(lean_obj_arg c, lean_obj_arg prio) { return lean_task_spawn_core(c, lean_unbox(prio), false); }
 /* Convert a value `a : A` into `Task A` */
-LEAN_SHARED lean_obj_res lean_task_pure(lean_obj_arg a);
-LEAN_SHARED lean_obj_res lean_task_bind_core(lean_obj_arg x, lean_obj_arg f, unsigned prio, bool sync, bool keep_alive);
+LEAN_EXPORT lean_obj_res lean_task_pure(lean_obj_arg a);
+LEAN_EXPORT lean_obj_res lean_task_bind_core(lean_obj_arg x, lean_obj_arg f, unsigned prio, bool sync, bool keep_alive);
 /* Task.bind (x : Task A) (f : A -> Task B) (prio : Nat) (sync : Bool) : Task B */
 static inline lean_obj_res lean_task_bind(lean_obj_arg x, lean_obj_arg f, lean_obj_arg prio, uint8_t sync) { return lean_task_bind_core(x, f, lean_unbox(prio), sync, false); }
-LEAN_SHARED lean_obj_res lean_task_map_core(lean_obj_arg f, lean_obj_arg t, unsigned prio, bool sync, bool keep_alive);
+LEAN_EXPORT lean_obj_res lean_task_map_core(lean_obj_arg f, lean_obj_arg t, unsigned prio, bool sync, bool keep_alive);
 /* Task.map (f : A -> B) (t : Task A) (prio : Nat) (sync : Bool) : Task B */
 static inline lean_obj_res lean_task_map(lean_obj_arg f, lean_obj_arg t, lean_obj_arg prio, uint8_t sync) { return lean_task_map_core(f, t, lean_unbox(prio), sync, false); }
-LEAN_SHARED b_lean_obj_res lean_task_get(b_lean_obj_arg t);
+LEAN_EXPORT b_lean_obj_res lean_task_get(b_lean_obj_arg t);
 /* Primitive for implementing Task.get : Task A -> A */
 static inline lean_obj_res lean_task_get_own(lean_obj_arg t) {
     lean_object * r = lean_task_get(t);
@@ -1108,13 +1106,13 @@ static inline lean_obj_res lean_task_get_own(lean_obj_arg t) {
 }
 
 /* primitive for implementing `IO.checkCanceled : IO Bool` */
-LEAN_SHARED bool lean_io_check_canceled_core(void);
+LEAN_EXPORT bool lean_io_check_canceled_core(void);
 /* primitive for implementing `IO.cancel : Task a -> IO Unit` */
-LEAN_SHARED void lean_io_cancel_core(b_lean_obj_arg t);
+LEAN_EXPORT void lean_io_cancel_core(b_lean_obj_arg t);
 /* primitive for implementing `IO.hasFinished : Task a -> IO Unit` */
-LEAN_SHARED bool lean_io_has_finished_core(b_lean_obj_arg t);
+LEAN_EXPORT bool lean_io_has_finished_core(b_lean_obj_arg t);
 /* primitive for implementing `IO.waitAny : List (Task a) -> IO (Task a)` */
-LEAN_SHARED b_lean_obj_res lean_io_wait_any_core(b_lean_obj_arg task_list);
+LEAN_EXPORT b_lean_obj_res lean_io_wait_any_core(b_lean_obj_arg task_list);
 
 /* External objects */
 
@@ -1138,23 +1136,23 @@ static inline void * lean_get_external_data(lean_object * o) {
 
 #define LEAN_MAX_SMALL_NAT (SIZE_MAX >> 1)
 
-LEAN_SHARED lean_object * lean_nat_big_succ(lean_object * a);
-LEAN_SHARED lean_object * lean_nat_big_add(lean_object * a1, lean_object * a2);
-LEAN_SHARED lean_object * lean_nat_big_sub(lean_object * a1, lean_object * a2);
-LEAN_SHARED lean_object * lean_nat_big_mul(lean_object * a1, lean_object * a2);
-LEAN_SHARED lean_object * lean_nat_overflow_mul(size_t a1, size_t a2);
-LEAN_SHARED lean_object * lean_nat_big_div(lean_object * a1, lean_object * a2);
-LEAN_SHARED lean_object * lean_nat_big_mod(lean_object * a1, lean_object * a2);
-LEAN_SHARED bool lean_nat_big_eq(lean_object * a1, lean_object * a2);
-LEAN_SHARED bool lean_nat_big_le(lean_object * a1, lean_object * a2);
-LEAN_SHARED bool lean_nat_big_lt(lean_object * a1, lean_object * a2);
-LEAN_SHARED lean_object * lean_nat_big_land(lean_object * a1, lean_object * a2);
-LEAN_SHARED lean_object * lean_nat_big_lor(lean_object * a1, lean_object * a2);
-LEAN_SHARED lean_object * lean_nat_big_xor(lean_object * a1, lean_object * a2);
+LEAN_EXPORT lean_object * lean_nat_big_succ(lean_object * a);
+LEAN_EXPORT lean_object * lean_nat_big_add(lean_object * a1, lean_object * a2);
+LEAN_EXPORT lean_object * lean_nat_big_sub(lean_object * a1, lean_object * a2);
+LEAN_EXPORT lean_object * lean_nat_big_mul(lean_object * a1, lean_object * a2);
+LEAN_EXPORT lean_object * lean_nat_overflow_mul(size_t a1, size_t a2);
+LEAN_EXPORT lean_object * lean_nat_big_div(lean_object * a1, lean_object * a2);
+LEAN_EXPORT lean_object * lean_nat_big_mod(lean_object * a1, lean_object * a2);
+LEAN_EXPORT bool lean_nat_big_eq(lean_object * a1, lean_object * a2);
+LEAN_EXPORT bool lean_nat_big_le(lean_object * a1, lean_object * a2);
+LEAN_EXPORT bool lean_nat_big_lt(lean_object * a1, lean_object * a2);
+LEAN_EXPORT lean_object * lean_nat_big_land(lean_object * a1, lean_object * a2);
+LEAN_EXPORT lean_object * lean_nat_big_lor(lean_object * a1, lean_object * a2);
+LEAN_EXPORT lean_object * lean_nat_big_xor(lean_object * a1, lean_object * a2);
 
-LEAN_SHARED lean_obj_res lean_cstr_to_nat(char const * n);
-LEAN_SHARED lean_obj_res lean_big_usize_to_nat(size_t n);
-LEAN_SHARED lean_obj_res lean_big_uint64_to_nat(uint64_t n);
+LEAN_EXPORT lean_obj_res lean_cstr_to_nat(char const * n);
+LEAN_EXPORT lean_obj_res lean_big_usize_to_nat(size_t n);
+LEAN_EXPORT lean_obj_res lean_big_uint64_to_nat(uint64_t n);
 static inline lean_obj_res lean_usize_to_nat(size_t n) {
     if (LEAN_LIKELY(n <= LEAN_MAX_SMALL_NAT))
         return lean_box(n);
@@ -1304,33 +1302,33 @@ static inline lean_obj_res lean_nat_lxor(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     }
 }
 
-LEAN_SHARED lean_obj_res lean_nat_shiftl(b_lean_obj_arg a1, b_lean_obj_arg a2);
-LEAN_SHARED lean_obj_res lean_nat_shiftr(b_lean_obj_arg a1, b_lean_obj_arg a2);
-LEAN_SHARED lean_obj_res lean_nat_pow(b_lean_obj_arg a1, b_lean_obj_arg a2);
-LEAN_SHARED lean_obj_res lean_nat_gcd(b_lean_obj_arg a1, b_lean_obj_arg a2);
-LEAN_SHARED lean_obj_res lean_nat_log2(b_lean_obj_arg a);
+LEAN_EXPORT lean_obj_res lean_nat_shiftl(b_lean_obj_arg a1, b_lean_obj_arg a2);
+LEAN_EXPORT lean_obj_res lean_nat_shiftr(b_lean_obj_arg a1, b_lean_obj_arg a2);
+LEAN_EXPORT lean_obj_res lean_nat_pow(b_lean_obj_arg a1, b_lean_obj_arg a2);
+LEAN_EXPORT lean_obj_res lean_nat_gcd(b_lean_obj_arg a1, b_lean_obj_arg a2);
+LEAN_EXPORT lean_obj_res lean_nat_log2(b_lean_obj_arg a);
 
 /* Integers */
 
 #define LEAN_MAX_SMALL_INT (sizeof(void*) == 8 ? INT_MAX : (INT_MAX >> 1))
 #define LEAN_MIN_SMALL_INT (sizeof(void*) == 8 ? INT_MIN : (INT_MIN >> 1))
-LEAN_SHARED lean_object * lean_int_big_neg(lean_object * a);
-LEAN_SHARED lean_object * lean_int_big_add(lean_object * a1, lean_object * a2);
-LEAN_SHARED lean_object * lean_int_big_sub(lean_object * a1, lean_object * a2);
-LEAN_SHARED lean_object * lean_int_big_mul(lean_object * a1, lean_object * a2);
-LEAN_SHARED lean_object * lean_int_big_div(lean_object * a1, lean_object * a2);
-LEAN_SHARED lean_object * lean_int_big_mod(lean_object * a1, lean_object * a2);
-LEAN_SHARED lean_object * lean_int_big_ediv(lean_object * a1, lean_object * a2);
-LEAN_SHARED lean_object * lean_int_big_emod(lean_object * a1, lean_object * a2);
-LEAN_SHARED bool lean_int_big_eq(lean_object * a1, lean_object * a2);
-LEAN_SHARED bool lean_int_big_le(lean_object * a1, lean_object * a2);
-LEAN_SHARED bool lean_int_big_lt(lean_object * a1, lean_object * a2);
-LEAN_SHARED bool lean_int_big_nonneg(lean_object * a);
+LEAN_EXPORT lean_object * lean_int_big_neg(lean_object * a);
+LEAN_EXPORT lean_object * lean_int_big_add(lean_object * a1, lean_object * a2);
+LEAN_EXPORT lean_object * lean_int_big_sub(lean_object * a1, lean_object * a2);
+LEAN_EXPORT lean_object * lean_int_big_mul(lean_object * a1, lean_object * a2);
+LEAN_EXPORT lean_object * lean_int_big_div(lean_object * a1, lean_object * a2);
+LEAN_EXPORT lean_object * lean_int_big_mod(lean_object * a1, lean_object * a2);
+LEAN_EXPORT lean_object * lean_int_big_ediv(lean_object * a1, lean_object * a2);
+LEAN_EXPORT lean_object * lean_int_big_emod(lean_object * a1, lean_object * a2);
+LEAN_EXPORT bool lean_int_big_eq(lean_object * a1, lean_object * a2);
+LEAN_EXPORT bool lean_int_big_le(lean_object * a1, lean_object * a2);
+LEAN_EXPORT bool lean_int_big_lt(lean_object * a1, lean_object * a2);
+LEAN_EXPORT bool lean_int_big_nonneg(lean_object * a);
 
-LEAN_SHARED lean_object * lean_cstr_to_int(char const * n);
-LEAN_SHARED lean_object * lean_big_int_to_int(int n);
-LEAN_SHARED lean_object * lean_big_size_t_to_int(size_t n);
-LEAN_SHARED lean_object * lean_big_int64_to_int(int64_t n);
+LEAN_EXPORT lean_object * lean_cstr_to_int(char const * n);
+LEAN_EXPORT lean_object * lean_big_int_to_int(int n);
+LEAN_EXPORT lean_object * lean_big_size_t_to_int(size_t n);
+LEAN_EXPORT lean_object * lean_big_int64_to_int(int64_t n);
 
 static inline lean_obj_res lean_int_to_int(int n) {
     if (sizeof(void*) == 8)
@@ -1566,7 +1564,7 @@ static inline bool lean_int_lt(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     }
 }
 
-LEAN_SHARED lean_obj_res lean_big_int_to_nat(lean_obj_arg a);
+LEAN_EXPORT lean_obj_res lean_big_int_to_nat(lean_obj_arg a);
 static inline lean_obj_res lean_int_to_nat(lean_obj_arg a) {
     assert(!lean_int_lt(a, lean_box(0)));
     if (lean_is_scalar(a)) {
@@ -1605,7 +1603,7 @@ static inline uint64_t lean_bool_to_uint64(uint8_t a) { return ((uint64_t)a); }
 
 /* UInt8 */
 
-LEAN_SHARED uint8_t lean_uint8_of_big_nat(b_lean_obj_arg a);
+LEAN_EXPORT uint8_t lean_uint8_of_big_nat(b_lean_obj_arg a);
 static inline uint8_t lean_uint8_of_nat(b_lean_obj_arg a) { return lean_is_scalar(a) ? (uint8_t)(lean_unbox(a)) : lean_uint8_of_big_nat(a); }
 /* Remark: the following function is used to implement the constructor `UInt8.mk`. We can't annotate constructors with `@&` */
 static inline uint8_t lean_uint8_of_nat_mk(lean_obj_arg a) { uint8_t r = lean_uint8_of_nat(a); lean_dec(a); return r; }
@@ -1649,7 +1647,7 @@ static inline uint64_t lean_uint8_to_uint64(uint8_t a) { return ((uint64_t)a); }
 
 /* UInt16 */
 
-LEAN_SHARED uint16_t lean_uint16_of_big_nat(b_lean_obj_arg a);
+LEAN_EXPORT uint16_t lean_uint16_of_big_nat(b_lean_obj_arg a);
 static inline uint16_t lean_uint16_of_nat(b_lean_obj_arg a) { return lean_is_scalar(a) ? (int16_t)(lean_unbox(a)) : lean_uint16_of_big_nat(a); }
 /* Remark: the following function is used to implement the constructor `UInt16.mk`. We can't annotate constructors with `@&` */
 static inline uint16_t lean_uint16_of_nat_mk(lean_obj_arg a) { uint16_t r = lean_uint16_of_nat(a); lean_dec(a); return r; }
@@ -1692,7 +1690,7 @@ static inline uint64_t lean_uint16_to_uint64(uint16_t a) { return ((uint64_t)a);
 
 /* UInt32 */
 
-LEAN_SHARED uint32_t lean_uint32_of_big_nat(b_lean_obj_arg a);
+LEAN_EXPORT uint32_t lean_uint32_of_big_nat(b_lean_obj_arg a);
 static inline uint32_t lean_uint32_of_nat(b_lean_obj_arg a) { return lean_is_scalar(a) ? (uint32_t)(lean_unbox(a)) : lean_uint32_of_big_nat(a); }
 /* Remark: the following function is used to implement the constructor `UInt32.mk`. We can't annotate constructors with `@&` */
 static inline uint32_t lean_uint32_of_nat_mk(lean_obj_arg a) { uint32_t r = lean_uint32_of_nat(a); lean_dec(a); return r; }
@@ -1708,7 +1706,7 @@ static inline uint32_t lean_uint32_xor(uint32_t a, uint32_t b) { return a ^ b; }
 static inline uint32_t lean_uint32_shift_left(uint32_t a, uint32_t b) { return a << (b % 32); }
 static inline uint32_t lean_uint32_shift_right(uint32_t a, uint32_t b) { return a >> (b % 32); }
 static inline uint32_t lean_uint32_complement(uint32_t a) { return ~a; }
-LEAN_SHARED uint32_t lean_uint32_big_modn(uint32_t a1, b_lean_obj_arg a2);
+LEAN_EXPORT uint32_t lean_uint32_big_modn(uint32_t a1, b_lean_obj_arg a2);
 static inline uint32_t lean_uint32_modn(uint32_t a1, b_lean_obj_arg a2) {
     if (LEAN_LIKELY(lean_is_scalar(a2))) {
         size_t n2 = lean_unbox(a2);
@@ -1742,7 +1740,7 @@ static inline size_t lean_uint32_to_usize(uint32_t a) { return a; }
 
 /* UInt64 */
 
-LEAN_SHARED uint64_t lean_uint64_of_big_nat(b_lean_obj_arg a);
+LEAN_EXPORT uint64_t lean_uint64_of_big_nat(b_lean_obj_arg a);
 static inline uint64_t lean_uint64_of_nat(b_lean_obj_arg a) { return lean_is_scalar(a) ? (uint64_t)(lean_unbox(a)) : lean_uint64_of_big_nat(a); }
 /* Remark: the following function is used to implement the constructor `UInt64.mk`. We can't annotate constructors with `@&` */
 static inline uint64_t lean_uint64_of_nat_mk(lean_obj_arg a) { uint64_t r = lean_uint64_of_nat(a); lean_dec(a); return r; }
@@ -1757,7 +1755,7 @@ static inline uint64_t lean_uint64_xor(uint64_t a, uint64_t b) { return a ^ b; }
 static inline uint64_t lean_uint64_shift_left(uint64_t a, uint64_t b) { return a << (b % 64); }
 static inline uint64_t lean_uint64_shift_right(uint64_t a, uint64_t b) { return a >> (b % 64); }
 static inline uint64_t lean_uint64_complement(uint64_t a) { return ~a; }
-LEAN_SHARED uint64_t lean_uint64_big_modn(uint64_t a1, b_lean_obj_arg a2);
+LEAN_EXPORT uint64_t lean_uint64_big_modn(uint64_t a1, b_lean_obj_arg a2);
 static inline uint64_t lean_uint64_modn(uint64_t a1, b_lean_obj_arg a2) {
     if (LEAN_LIKELY(lean_is_scalar(a2))) {
         size_t n2 = lean_unbox(a2);
@@ -1777,7 +1775,7 @@ static inline uint64_t lean_uint64_log2(uint64_t a) {
 static inline uint8_t lean_uint64_dec_eq(uint64_t a1, uint64_t a2) { return a1 == a2; }
 static inline uint8_t lean_uint64_dec_lt(uint64_t a1, uint64_t a2) { return a1 < a2; }
 static inline uint8_t lean_uint64_dec_le(uint64_t a1, uint64_t a2) { return a1 <= a2; }
-LEAN_SHARED uint64_t lean_uint64_mix_hash(uint64_t a1, uint64_t a2);
+LEAN_EXPORT uint64_t lean_uint64_mix_hash(uint64_t a1, uint64_t a2);
 
 
 /* uint64 -> other */
@@ -1788,7 +1786,7 @@ static inline size_t lean_uint64_to_usize(uint64_t a) { return ((size_t)a); }
 
 /* USize */
 
-LEAN_SHARED size_t lean_usize_of_big_nat(b_lean_obj_arg a);
+LEAN_EXPORT size_t lean_usize_of_big_nat(b_lean_obj_arg a);
 static inline size_t lean_usize_of_nat(b_lean_obj_arg a) { return lean_is_scalar(a) ? lean_unbox(a) : lean_usize_of_big_nat(a); }
 /* Remark: the following function is used to implement the constructor `USize.mk`. We can't annotate constructors with `@&` */
 static inline size_t lean_usize_of_nat_mk(lean_obj_arg a) { size_t r = lean_usize_of_nat(a); lean_dec(a); return r; }
@@ -1803,7 +1801,7 @@ static inline size_t lean_usize_xor(size_t a, size_t b) { return a ^ b; }
 static inline size_t lean_usize_shift_left(size_t a, size_t b) { return a << (b %  (sizeof(size_t) * 8)); }
 static inline size_t lean_usize_shift_right(size_t a, size_t b) { return a >> (b % (sizeof(size_t) * 8)); }
 static inline size_t lean_usize_complement(size_t a) { return ~a; }
-LEAN_SHARED size_t lean_usize_big_modn(size_t a1, b_lean_obj_arg a2);
+LEAN_EXPORT size_t lean_usize_big_modn(size_t a1, b_lean_obj_arg a2);
 static inline size_t lean_usize_modn(size_t a1, b_lean_obj_arg a2) {
     if (LEAN_LIKELY(lean_is_scalar(a2))) {
         size_t n2 = lean_unbox(a2);
@@ -1832,12 +1830,12 @@ static inline uint64_t lean_usize_to_uint64(size_t a) { return ((uint64_t)a); }
 
 /* Float */
 
-LEAN_SHARED lean_obj_res lean_float_to_string(double a);
-LEAN_SHARED double lean_float_scaleb(double a, b_lean_obj_arg b);
-LEAN_SHARED uint8_t lean_float_isnan(double a);
-LEAN_SHARED uint8_t lean_float_isfinite(double a);
-LEAN_SHARED uint8_t lean_float_isinf(double a);
-LEAN_SHARED lean_obj_res lean_float_frexp(double a);
+LEAN_EXPORT lean_obj_res lean_float_to_string(double a);
+LEAN_EXPORT double lean_float_scaleb(double a, b_lean_obj_arg b);
+LEAN_EXPORT uint8_t lean_float_isnan(double a);
+LEAN_EXPORT uint8_t lean_float_isfinite(double a);
+LEAN_EXPORT uint8_t lean_float_isinf(double a);
+LEAN_EXPORT lean_obj_res lean_float_frexp(double a);
 
 /* Boxing primitives */
 
@@ -1895,21 +1893,21 @@ static inline double lean_unbox_float(b_lean_obj_arg o) {
 
 /* Debugging helper functions */
 
-LEAN_SHARED lean_object * lean_dbg_trace(lean_obj_arg s, lean_obj_arg fn);
-LEAN_SHARED lean_object * lean_dbg_sleep(uint32_t ms, lean_obj_arg fn);
-LEAN_SHARED lean_object * lean_dbg_trace_if_shared(lean_obj_arg s, lean_obj_arg a);
+LEAN_EXPORT lean_object * lean_dbg_trace(lean_obj_arg s, lean_obj_arg fn);
+LEAN_EXPORT lean_object * lean_dbg_sleep(uint32_t ms, lean_obj_arg fn);
+LEAN_EXPORT lean_object * lean_dbg_trace_if_shared(lean_obj_arg s, lean_obj_arg a);
 
 /* IO Helper functions */
 
-LEAN_SHARED lean_obj_res lean_decode_io_error(int errnum, b_lean_obj_arg fname);
+LEAN_EXPORT lean_obj_res lean_decode_io_error(int errnum, b_lean_obj_arg fname);
 
 static inline lean_obj_res lean_io_mk_world() { return lean_box(0); }
 static inline bool lean_io_result_is_ok(b_lean_obj_arg r) { return lean_ptr_tag(r) == 0; }
 static inline bool lean_io_result_is_error(b_lean_obj_arg r) { return lean_ptr_tag(r) == 1; }
 static inline b_lean_obj_res lean_io_result_get_value(b_lean_obj_arg r) { assert(lean_io_result_is_ok(r)); return lean_ctor_get(r, 0); }
 static inline b_lean_obj_res lean_io_result_get_error(b_lean_obj_arg r) { assert(lean_io_result_is_error(r)); return lean_ctor_get(r, 0); }
-LEAN_SHARED void lean_io_result_show_error(b_lean_obj_arg r);
-LEAN_SHARED void lean_io_mark_end_initialization(void);
+LEAN_EXPORT void lean_io_result_show_error(b_lean_obj_arg r);
+LEAN_EXPORT void lean_io_mark_end_initialization(void);
 static inline lean_obj_res lean_io_result_mk_ok(lean_obj_arg a) {
     lean_object * r = lean_alloc_ctor(0, 2, 0);
     lean_ctor_set(r, 0, a);
@@ -1923,45 +1921,45 @@ static inline lean_obj_res lean_io_result_mk_error(lean_obj_arg e) {
     return r;
 }
 
-LEAN_SHARED lean_obj_res lean_mk_io_error_already_exists(uint32_t, lean_obj_arg);
-LEAN_SHARED lean_obj_res lean_mk_io_error_already_exists_file(lean_obj_arg, uint32_t, lean_obj_arg);
-LEAN_SHARED lean_obj_res lean_mk_io_error_eof(lean_obj_arg);
-LEAN_SHARED lean_obj_res lean_mk_io_error_hardware_fault(uint32_t, lean_obj_arg);
-LEAN_SHARED lean_obj_res lean_mk_io_error_illegal_operation(uint32_t, lean_obj_arg);
-LEAN_SHARED lean_obj_res lean_mk_io_error_inappropriate_type(uint32_t, lean_obj_arg);
-LEAN_SHARED lean_obj_res lean_mk_io_error_inappropriate_type_file(lean_obj_arg, uint32_t, lean_obj_arg);
-LEAN_SHARED lean_obj_res lean_mk_io_error_interrupted(lean_obj_arg, uint32_t, lean_obj_arg);
-LEAN_SHARED lean_obj_res lean_mk_io_error_invalid_argument(uint32_t, lean_obj_arg);
-LEAN_SHARED lean_obj_res lean_mk_io_error_invalid_argument_file(lean_obj_arg, uint32_t, lean_obj_arg);
-LEAN_SHARED lean_obj_res lean_mk_io_error_no_file_or_directory(lean_obj_arg, uint32_t, lean_obj_arg);
-LEAN_SHARED lean_obj_res lean_mk_io_error_no_such_thing(uint32_t, lean_obj_arg);
-LEAN_SHARED lean_obj_res lean_mk_io_error_no_such_thing_file(lean_obj_arg, uint32_t, lean_obj_arg);
-LEAN_SHARED lean_obj_res lean_mk_io_error_other_error(uint32_t, lean_obj_arg);
-LEAN_SHARED lean_obj_res lean_mk_io_error_permission_denied(uint32_t, lean_obj_arg);
-LEAN_SHARED lean_obj_res lean_mk_io_error_permission_denied_file(lean_obj_arg, uint32_t, lean_obj_arg);
-LEAN_SHARED lean_obj_res lean_mk_io_error_protocol_error(uint32_t, lean_obj_arg);
-LEAN_SHARED lean_obj_res lean_mk_io_error_resource_busy(uint32_t, lean_obj_arg);
-LEAN_SHARED lean_obj_res lean_mk_io_error_resource_exhausted(uint32_t, lean_obj_arg);
-LEAN_SHARED lean_obj_res lean_mk_io_error_resource_exhausted_file(lean_obj_arg, uint32_t, lean_obj_arg);
-LEAN_SHARED lean_obj_res lean_mk_io_error_resource_vanished(uint32_t, lean_obj_arg);
-LEAN_SHARED lean_obj_res lean_mk_io_error_time_expired(uint32_t, lean_obj_arg);
-LEAN_SHARED lean_obj_res lean_mk_io_error_unsatisfied_constraints(uint32_t, lean_obj_arg);
-LEAN_SHARED lean_obj_res lean_mk_io_error_unsupported_operation(uint32_t, lean_obj_arg);
-LEAN_SHARED lean_obj_res lean_mk_io_user_error(lean_obj_arg str);
+LEAN_EXPORT lean_obj_res lean_mk_io_error_already_exists(uint32_t, lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_mk_io_error_already_exists_file(lean_obj_arg, uint32_t, lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_mk_io_error_eof(lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_mk_io_error_hardware_fault(uint32_t, lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_mk_io_error_illegal_operation(uint32_t, lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_mk_io_error_inappropriate_type(uint32_t, lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_mk_io_error_inappropriate_type_file(lean_obj_arg, uint32_t, lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_mk_io_error_interrupted(lean_obj_arg, uint32_t, lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_mk_io_error_invalid_argument(uint32_t, lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_mk_io_error_invalid_argument_file(lean_obj_arg, uint32_t, lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_mk_io_error_no_file_or_directory(lean_obj_arg, uint32_t, lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_mk_io_error_no_such_thing(uint32_t, lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_mk_io_error_no_such_thing_file(lean_obj_arg, uint32_t, lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_mk_io_error_other_error(uint32_t, lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_mk_io_error_permission_denied(uint32_t, lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_mk_io_error_permission_denied_file(lean_obj_arg, uint32_t, lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_mk_io_error_protocol_error(uint32_t, lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_mk_io_error_resource_busy(uint32_t, lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_mk_io_error_resource_exhausted(uint32_t, lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_mk_io_error_resource_exhausted_file(lean_obj_arg, uint32_t, lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_mk_io_error_resource_vanished(uint32_t, lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_mk_io_error_time_expired(uint32_t, lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_mk_io_error_unsatisfied_constraints(uint32_t, lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_mk_io_error_unsupported_operation(uint32_t, lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_mk_io_user_error(lean_obj_arg str);
 
 
 /* ST Ref primitives */
-LEAN_SHARED lean_obj_res lean_st_mk_ref(lean_obj_arg, lean_obj_arg);
-LEAN_SHARED lean_obj_res lean_st_ref_get(b_lean_obj_arg, lean_obj_arg);
-LEAN_SHARED lean_obj_res lean_st_ref_set(b_lean_obj_arg, lean_obj_arg, lean_obj_arg);
-LEAN_SHARED lean_obj_res lean_st_ref_reset(b_lean_obj_arg, lean_obj_arg);
-LEAN_SHARED lean_obj_res lean_st_ref_swap(b_lean_obj_arg, lean_obj_arg, lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_st_mk_ref(lean_obj_arg, lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_st_ref_get(b_lean_obj_arg, lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_st_ref_set(b_lean_obj_arg, lean_obj_arg, lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_st_ref_reset(b_lean_obj_arg, lean_obj_arg);
+LEAN_EXPORT lean_obj_res lean_st_ref_swap(b_lean_obj_arg, lean_obj_arg, lean_obj_arg);
 
 /* pointer address unsafe primitive  */
 static inline size_t lean_ptr_addr(b_lean_obj_arg a) { return (size_t)a; }
 
 /* Name primitives */
-LEAN_SHARED uint8_t lean_name_eq(b_lean_obj_arg n1, b_lean_obj_arg n2);
+LEAN_EXPORT uint8_t lean_name_eq(b_lean_obj_arg n1, b_lean_obj_arg n2);
 
 static inline uint64_t lean_name_hash_ptr(b_lean_obj_arg n) {
     assert(!lean_is_scalar(n));

src/include/lean/lean_gmp.h

@@ -13,12 +13,12 @@ extern "C" {
 #endif
 
 #ifdef LEAN_USE_GMP
-LEAN_SHARED lean_object * lean_alloc_mpz(mpz_t);
+LEAN_EXPORT lean_object * lean_alloc_mpz(mpz_t);
 /* Set `v` with the value stored in `o`.
    - pre: `lean_is_mpz(o)`
    - pre: `v` has already been initialized using `mpz_init` (or equivalent).
 */
-LEAN_SHARED void lean_extract_mpz_value(lean_object * o, mpz_t v);
+LEAN_EXPORT void lean_extract_mpz_value(lean_object * o, mpz_t v);
 #endif
 
 #ifdef __cplusplus

src/lake/Lake/Build/Executable.lean

@@ -15,7 +15,7 @@ protected def LeanExe.recBuildExe
 (self : LeanExe) : IndexBuildM (BuildJob FilePath) := do
   let imports ← self.root.transImports.fetch
   let mut linkJobs := #[← self.root.o.fetch]
-  for mod in imports do for facet in mod.nativeFacets do
+  for mod in imports do for facet in mod.nativeFacets self.supportInterpreter do
     linkJobs := linkJobs.push <| ← fetch <| mod.facet facet.name
   let deps := (← fetch <| self.pkg.facet `deps).push self.pkg
   for dep in deps do for lib in dep.externLibs do

src/lake/Lake/Build/Facets.lean

@@ -78,18 +78,42 @@ module_data c : BuildJob FilePath
 abbrev Module.bcFacet := `bc
 module_data bc : BuildJob FilePath
 
-/-- The object file `.c.o` built from `c`. -/
+/--
+The object file `.c.o` built from `c`.
+On Windows, this is `c.o.noexport`, on other systems it is `c.o.export`).
+-/
 abbrev Module.coFacet := `c.o
 module_data c.o : BuildJob FilePath
 
+/-- The object file `.c.o.export` built from `c` (with `-DLEAN_EXPORTING`). -/
+abbrev Module.coExportFacet := `c.o.export
+module_data c.o.export : BuildJob FilePath
+
+/-- The object file `.c.o.noexport` built from `c` (without `-DLEAN_EXPORTING`). -/
+abbrev Module.coNoExportFacet := `c.o.noexport
+module_data c.o.noexport : BuildJob FilePath
+
 /-- The object file `.bc.o` built from `bc`. -/
 abbrev Module.bcoFacet := `bc.o
 module_data bc.o : BuildJob FilePath
 
-/-- The object file built from `c`/`bc`. -/
+/--
+The object file built from `c`/`bc`.
+On Windows with the C backend, no Lean symbols are exported.
+On every other configuration, symbols are exported.
+-/
 abbrev Module.oFacet := `o
 module_data o : BuildJob FilePath
 
+/-- The object file built from `c`/`bc` (with Lean symbols exported). -/
+abbrev Module.oExportFacet := `o.export
+module_data o.export : BuildJob FilePath
+
+/-- The object file built from `c`/`bc` (without Lean symbols exported). -/
+abbrev Module.oNoExportFacet := `o.noexport
+module_data o.noexport : BuildJob FilePath
+
+
 /-! ## Package Facets -/
 
 /-- A package's cloud build release. -/
@@ -110,6 +134,10 @@ library_data leanArts : BuildJob Unit
 abbrev LeanLib.staticFacet := `static
 library_data static : BuildJob FilePath
 
+/-- A Lean library's static artifact (with exported symbols). -/
+abbrev LeanLib.staticExportFacet := `static.export
+library_data static.export : BuildJob FilePath
+
 /-- A Lean library's shared artifact. -/
 abbrev LeanLib.sharedFacet := `shared
 library_data shared : BuildJob FilePath

src/lake/Lake/Build/Info.lean

@@ -211,9 +211,21 @@ abbrev facet (facet : Name) (self : Module) : BuildInfo :=
 @[inherit_doc oFacet] abbrev o (self : Module) :=
   self.facet oFacet
 
+@[inherit_doc oExportFacet] abbrev oExport (self : Module) :=
+  self.facet oExportFacet
+
+@[inherit_doc oNoExportFacet] abbrev oNoExport (self : Module) :=
+  self.facet oNoExportFacet
+
 @[inherit_doc coFacet] abbrev co (self : Module) :=
   self.facet coFacet
 
+@[inherit_doc coExportFacet] abbrev coExport (self : Module) :=
+  self.facet coExportFacet
+
+@[inherit_doc coNoExportFacet] abbrev coNoExport (self : Module) :=
+  self.facet coNoExportFacet
+
 @[inherit_doc bcoFacet] abbrev bco (self : Module) :=
   self.facet bcoFacet
 
@@ -254,6 +266,10 @@ abbrev LeanLib.leanArts (self : LeanLib) : BuildInfo :=
 abbrev LeanLib.static (self : LeanLib) : BuildInfo :=
   self.facet staticFacet
 
+@[inherit_doc staticExportFacet]
+abbrev LeanLib.staticExport (self : LeanLib) : BuildInfo :=
+  self.facet staticExportFacet
+
 @[inherit_doc sharedFacet]
 abbrev LeanLib.shared (self : LeanLib) : BuildInfo :=
   self.facet sharedFacet

src/lake/Lake/Build/Library.lean

@@ -51,16 +51,22 @@ protected def LeanLib.recBuildLean
 def LeanLib.leanArtsFacetConfig : LibraryFacetConfig leanArtsFacet :=
   mkFacetJobConfigSmall LeanLib.recBuildLean
 
-protected def LeanLib.recBuildStatic
-(self : LeanLib) : IndexBuildM (BuildJob FilePath) := do
+@[specialize] protected def LeanLib.recBuildStatic
+(self : LeanLib) (shouldExport : Bool) : IndexBuildM (BuildJob FilePath) := do
   let mods ← self.modules.fetch
   let oJobs ← mods.concatMapM fun mod =>
-    mod.nativeFacets.mapM fun facet => fetch <| mod.facet facet.name
-  buildStaticLib self.staticLibFile oJobs
+    mod.nativeFacets shouldExport |>.mapM fun facet => fetch <| mod.facet facet.name
+  let libFile := if shouldExport then self.staticExportLibFile else self.staticLibFile
+  buildStaticLib libFile oJobs
 
 /-- The `LibraryFacetConfig` for the builtin `staticFacet`. -/
 def LeanLib.staticFacetConfig : LibraryFacetConfig staticFacet :=
-  mkFacetJobConfig LeanLib.recBuildStatic
+  mkFacetJobConfig (LeanLib.recBuildStatic · false)
+
+/-- The `LibraryFacetConfig` for the builtin `staticExportFacet`. -/
+def LeanLib.staticExportFacetConfig : LibraryFacetConfig staticExportFacet :=
+  mkFacetJobConfig (LeanLib.recBuildStatic · true)
+
 
 /-! ## Build Shared Lib -/
 
@@ -68,7 +74,7 @@ protected def LeanLib.recBuildShared
 (self : LeanLib) : IndexBuildM (BuildJob FilePath) := do
   let mods ← self.modules.fetch
   let oJobs ← mods.concatMapM fun mod =>
-    mod.nativeFacets.mapM fun facet => fetch <| mod.facet facet.name
+    mod.nativeFacets true |>.mapM fun facet => fetch <| mod.facet facet.name
   let pkgs := mods.foldl (·.insert ·.pkg) OrdPackageSet.empty |>.toArray
   let externJobs ← pkgs.concatMapM (·.externLibs.mapM (·.shared.fetch))
   buildLeanSharedLib self.sharedLibFile (oJobs ++ externJobs) self.weakLinkArgs self.linkArgs
@@ -98,5 +104,6 @@ def initLibraryFacetConfigs : DNameMap LibraryFacetConfig :=
   |>.insert modulesFacet modulesFacetConfig
   |>.insert leanArtsFacet leanArtsFacetConfig
   |>.insert staticFacet staticFacetConfig
+  |>.insert staticExportFacet staticExportFacetConfig
   |>.insert sharedFacet sharedFacetConfig
   |>.insert extraDepFacet extraDepFacetConfig

src/lake/Lake/Build/Module.lean

@@ -196,32 +196,66 @@ def Module.bcFacetConfig : ModuleFacetConfig bcFacet :=
       -- do content-aware hashing so that we avoid recompiling unchanged bitcode files
       return (mod.bcFile, ← fetchFileTrace mod.bcFile)
 
-/-- Recursively build the module's object file from its C file produced by `lean`. -/
-def Module.recBuildLeanCToO (self : Module) : IndexBuildM (BuildJob FilePath) := do
+/--
+Recursively build the module's object file from its C file produced by `lean`
+with `-DLEAN_EXPORTING` set, which exports Lean symbols defined within the C files.
+-/
+def Module.recBuildLeanCToOExport (self : Module) : IndexBuildM (BuildJob FilePath) := do
   -- TODO: add option to pass a target triplet for cross compilation
-  buildLeanO self.name.toString self.coFile (← self.c.fetch) self.weakLeancArgs self.leancArgs
+  let leancArgs := self.leancArgs ++ #["-DLEAN_EXPORTING"]
+  buildLeanO self.name.toString self.coExportFile (← self.c.fetch) self.weakLeancArgs leancArgs
+
+/-- The `ModuleFacetConfig` for the builtin `coExportFacet`. -/
+def Module.coExportFacetConfig : ModuleFacetConfig coExportFacet :=
+  mkFacetJobConfig Module.recBuildLeanCToOExport
+
+/--
+Recursively build the module's object file from its C file produced by `lean`.
+This version does not export any Lean symbols.
+-/
+def Module.recBuildLeanCToONoExport (self : Module) : IndexBuildM (BuildJob FilePath) := do
+  -- TODO: add option to pass a target triplet for cross compilation
+  buildLeanO self.name.toString self.coNoExportFile (← self.c.fetch) self.weakLeancArgs self.leancArgs
+
+/-- The `ModuleFacetConfig` for the builtin `coNoExportFacet`. -/
+def Module.coNoExportFacetConfig : ModuleFacetConfig coNoExportFacet :=
+  mkFacetJobConfig Module.recBuildLeanCToONoExport
+
+/-- The `ModuleFacetConfig` for the builtin `coFacet`. -/
+def Module.coFacetConfig : ModuleFacetConfig coFacet :=
+  mkFacetJobConfigSmall fun mod =>
+    if Platform.isWindows then mod.coNoExport.fetch else mod.coExport.fetch
 
 /-- Recursively build the module's object file from its bitcode file produced by `lean`. -/
 def Module.recBuildLeanBcToO (self : Module) : IndexBuildM (BuildJob FilePath) := do
   -- TODO: add option to pass a target triplet for cross compilation
   buildLeanO self.name.toString self.bcoFile (← self.bc.fetch) self.weakLeancArgs self.leancArgs
 
-/-- The `ModuleFacetConfig` for the builtin `coFacet`. -/
-def Module.coFacetConfig : ModuleFacetConfig coFacet :=
-  mkFacetJobConfig Module.recBuildLeanCToO
-
 /-- The `ModuleFacetConfig` for the builtin `bcoFacet`. -/
 def Module.bcoFacetConfig : ModuleFacetConfig bcoFacet :=
   mkFacetJobConfig Module.recBuildLeanBcToO
 
-/-- The `ModuleFacetConfig` for the builtin `OFacet`. -/
+/-- The `ModuleFacetConfig` for the builtin `oExportFacet`. -/
+def Module.oExportFacetConfig : ModuleFacetConfig oExportFacet :=
+  mkFacetJobConfigSmall fun mod =>
+    match mod.backend with
+    | .default | .c => mod.coExport.fetch
+    | .llvm => mod.bco.fetch
+
+/-- The `ModuleFacetConfig` for the builtin `oNoExportFacet`. -/
+def Module.oNoExportFacetConfig : ModuleFacetConfig oNoExportFacet :=
+  mkFacetJobConfigSmall fun mod =>
+    match mod.backend with
+    | .default | .c => mod.coNoExport.fetch
+    | .llvm => error "the LLVM backend only supports exporting Lean symbols"
+
+/-- The `ModuleFacetConfig` for the builtin `oFacet`. -/
 def Module.oFacetConfig : ModuleFacetConfig oFacet :=
   mkFacetJobConfigSmall fun mod =>
     match mod.backend with
     | .default | .c => mod.co.fetch
     | .llvm => mod.bco.fetch
 
-
 -- TODO: Return `BuildJob OrdModuleSet × OrdPackageSet` or `OrdRBSet Dynlib`
 /-- Recursively build the shared library of a module (e.g., for `--load-dynlib`). -/
 def Module.recBuildDynlib (mod : Module) : IndexBuildM (BuildJob Dynlib) := do
@@ -232,7 +266,7 @@ def Module.recBuildDynlib (mod : Module) : IndexBuildM (BuildJob Dynlib) := do
   let pkgs := transImports.foldl (·.insert ·.pkg)
     OrdPackageSet.empty |>.insert mod.pkg |>.toArray
   let (externJobs, pkgLibDirs) ← recBuildExternDynlibs pkgs
-  let linkJobs ← mod.nativeFacets.mapM (fetch <| mod.facet ·.name)
+  let linkJobs ← mod.nativeFacets true |>.mapM (fetch <| mod.facet ·.name)
 
   -- Collect Jobs
   let linksJob ← BuildJob.collectArray linkJobs
@@ -279,6 +313,10 @@ def initModuleFacetConfigs : DNameMap ModuleFacetConfig :=
   |>.insert cFacet cFacetConfig
   |>.insert bcFacet bcFacetConfig
   |>.insert coFacet coFacetConfig
+  |>.insert coExportFacet coExportFacetConfig
+  |>.insert coNoExportFacet coNoExportFacetConfig
   |>.insert bcoFacet bcoFacetConfig
   |>.insert oFacet oFacetConfig
+  |>.insert oExportFacet oExportFacetConfig
+  |>.insert oNoExportFacet oNoExportFacetConfig
   |>.insert dynlibFacet dynlibFacetConfig

src/lake/Lake/Config/InstallPath.lean

@@ -39,14 +39,20 @@ def leanArExe (sysroot : FilePath) :=
 def leanCcExe (sysroot : FilePath) :=
   sysroot / "bin" / "clang" |>.addExtension FilePath.exeExtension
 
-/-- Standard path of `libleanshared` in a Lean installation. -/
-def leanSharedLib (sysroot : FilePath) :=
-  let dir :=
-    if Platform.isWindows then
-      sysroot / "bin"
-    else
-      sysroot / "lib" / "lean"
-  dir / "libleanshared" |>.addExtension sharedLibExt
+/-- Standard path of shared libraries in a Lean installation. -/
+def leanSharedLibDir (sysroot : FilePath) :=
+  if Platform.isWindows then
+    sysroot / "bin"
+  else
+    sysroot / "lib" / "lean"
+
+/-- `libleanshared` file name. -/
+def leanSharedLib  :=
+  FilePath.addExtension "libleanshared" sharedLibExt
+
+/-- `Init` shared library file name. -/
+def initSharedLib : FilePath :=
+  FilePath.addExtension "libInit_shared" sharedLibExt
 
 /-- Path information about the local Lean installation. -/
 structure LeanInstall where
@@ -59,7 +65,8 @@ structure LeanInstall where
   binDir := sysroot / "bin"
   lean := leanExe sysroot
   leanc := leancExe sysroot
-  sharedLib := leanSharedLib sysroot
+  sharedLib := leanSharedLibDir sysroot / leanSharedLib
+  initSharedLib := leanSharedLibDir sysroot / initSharedLib
   ar : FilePath
   cc : FilePath
   customCc : Bool
@@ -79,9 +86,9 @@ def LeanInstall.sharedLibPath (self : LeanInstall) : SearchPath :=
 def LeanInstall.leanCc? (self : LeanInstall) : Option String :=
   if self.customCc then self.cc.toString else none
 
-/-- Lake executable file path. -/
+/-- Lake executable file name. -/
 def lakeExe : FilePath :=
-  FilePath.mk "lake" |>.addExtension FilePath.exeExtension
+  FilePath.addExtension "lake" FilePath.exeExtension
 
 /-- Path information about the local Lake installation. -/
 structure LakeInstall where
@@ -210,12 +217,23 @@ def findLakeLeanJointHome? : BaseIO (Option FilePath) := do
   return none
 
 /--
-Attempt to detect a specified Lake's executable's home by assuming
-the executable is located at `<lake-home>/.lake/build/bin/lake`.
+Get the root of Lake's installation by assuming the executable
+is located at `<lake-home>/.lake/build/bin/lake`.
 -/
-def lakePackageHome? (lake : FilePath) : Option FilePath := do
+def lakeBuildHome? (lake : FilePath) : Option FilePath := do
   (← (← (← lake.parent).parent).parent).parent
 
+/--
+Heuristically validate that `getLakeBuildHome?` is a proper Lake installation
+by check for `Lake.olean` in the installation's `lib` directory.
+-/
+def getLakeInstall? (lake : FilePath) : BaseIO (Option LakeInstall) := do
+  let some home := lakeBuildHome? lake | return none
+  let lake : LakeInstall := {home, lake}
+  if (← lake.libDir / "Lake.olean" |>.pathExists) then
+    return lake
+  return none
+
 /--
 Attempt to detect Lean's installation by first checking the
 `LEAN_SYSROOT` environment variable and then by trying `findLeanCmdHome?`.
@@ -229,9 +247,8 @@ def findLeanInstall? : BaseIO (Option LeanInstall) := do
   return none
 
 /--
-Attempt to detect Lake's installation by
-first checking the `LAKE_HOME` environment variable
-and then by trying the `lakePackageHome?` of the running executable.
+Attempt to detect Lake's installation by first checking the `lakeBuildHome?`
+of the running executable, then trying the `LAKE_HOME` environment variable.
 
 It assumes that the Lake installation is organized the same way it is built.
 That is, with its binary located at `<lake-home>/.lake/build/bin/lake` and its
@@ -239,11 +256,11 @@ static library and `.olean` files in `<lake-home>/.lake/build/lib`, and
 its source files located directly in `<lake-home>`.
 -/
 def findLakeInstall? : BaseIO (Option LakeInstall) := do
+  if let Except.ok lake ← IO.appPath.toBaseIO then
+    if let some lake ← getLakeInstall? lake then
+      return lake
   if let some home ← IO.getEnv "LAKE_HOME" then
     return some {home}
-  if let Except.ok lake ← IO.appPath.toBaseIO then
-    if let some home := lakePackageHome? lake then
-      return some {home, lake}
   return none
 
 /--

src/lake/Lake/Config/LeanExe.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+import Lean.Compiler.FFI
 import Lake.Config.Module
 
 namespace Lake
@@ -67,15 +68,24 @@ The file name of binary executable
 @[inline] def file (self : LeanExe) : FilePath :=
   self.pkg.binDir / self.fileName
 
+/-- The executable's `supportInterpreter` configuration. -/
+@[inline] def supportInterpreter (self : LeanExe) : Bool :=
+  self.config.supportInterpreter
+
 /--
 The arguments to pass to `leanc` when linking the binary executable.
+By default, the package's plus the executable's `moreLinkArgs`.
 
-That is, `-rdynamic` (if non-Windows and `supportInterpreter`) plus the
-package's and then the executable's `moreLinkArgs`.
+If `supportInterpreter := true`, Lake links directly to the Lean shared
+libraries on Windows by prepending `-leanshared` and adds `-rdynamic` on
+other systems.
 -/
 def linkArgs (self : LeanExe) : Array String :=
-  if self.config.supportInterpreter && !Platform.isWindows then
-    #["-rdynamic"] ++ self.pkg.moreLinkArgs ++ self.config.moreLinkArgs
+  if self.config.supportInterpreter then
+    if Platform.isWindows then
+      #["-leanshared"] ++ self.pkg.moreLinkArgs ++ self.config.moreLinkArgs
+    else
+      #["-rdynamic"] ++ self.pkg.moreLinkArgs ++ self.config.moreLinkArgs
   else
     self.pkg.moreLinkArgs ++ self.config.moreLinkArgs
 

src/lake/Lake/Config/LeanExeConfig.lean

@@ -43,24 +43,34 @@ structure LeanExeConfig extends LeanConfig where
   /-- An `Array` of target names to build before the executable's modules. -/
   extraDepTargets : Array Name := #[]
 
-  /--
-  An `Array` of module facets to build and combine into the executable.
-  Defaults to ``#[Module.oFacet]`` (i.e., the object file compiled from
-  the Lean source).
-  -/
-  nativeFacets : Array (ModuleFacet (BuildJob FilePath)) := #[Module.oFacet]
-
   /--
   Enables the executable to interpret Lean files (e.g., via
   `Lean.Elab.runFrontend`) by exposing symbols within the  executable
   to the Lean interpreter.
 
-  Implementation-wise, this passes `-rdynamic` to the linker when building
-  on non-Windows systems. This increases the size of the binary on Linux, so
-  this feature should only be enabled when necessary.
+  Implementation-wise, on Windows, the Lean shared libraries are linked
+  to the executable and, on other systems, the executable is linked with
+  `-rdynamic`. This increases the size of the binary on Linux and, on Windows,
+  requires `libInit_shared.dll` and `libleanshared.dll` to  be co-located
+  with the executable or part of `PATH` (e.g., via `lake exe`). Thus, this
+  feature should only be enabled when necessary.
 
   Defaults to `false`.
   -/
   supportInterpreter : Bool := false
 
+  /--
+  The module facets to build and combine into the executable.
+  If `shouldExport` is true, the module facets should export any symbols
+  a user may expect to lookup in the executable. For example, the Lean
+  interpreter will use exported symbols in the executable. Thus, `shouldExport`
+  will be `true` if `supportInterpreter := true`.
+
+  Defaults to a singleton of `Module.oExportFacet` (if `shouldExport`) or
+  `Module.oFacet`. That is, the  object file compiled from the Lean source,
+  potentially with exported Lean symbols.
+  -/
+  nativeFacets (shouldExport : Bool) : Array (ModuleFacet (BuildJob FilePath)) :=
+    #[if shouldExport then Module.oExportFacet else Module.oFacet]
+
 deriving Inhabited

src/lake/Lake/Config/LeanLib.lean

@@ -60,6 +60,10 @@ The names of the library's root modules
 @[inline] def staticLibFile (self : LeanLib) : FilePath :=
   self.pkg.nativeLibDir / self.staticLibFileName
 
+/-- The path to the static library (with exported symbols) in the package's `libDir`. -/
+@[inline] def staticExportLibFile (self : LeanLib) : FilePath :=
+  self.pkg.nativeLibDir / self.staticLibFileName.addExtension "export"
+
 /-- The file name of the library's shared binary (i.e., its `dll`, `dylib`, or `so`) . -/
 @[inline] def sharedLibFileName (self : LeanLib) : FilePath :=
   nameToSharedLib self.config.libName
@@ -92,8 +96,8 @@ Otherwise, falls back to the package's.
   self.config.defaultFacets
 
 /-- The library's `nativeFacets` configuration. -/
-@[inline] def nativeFacets (self : LeanLib) : Array (ModuleFacet (BuildJob FilePath)) :=
-  self.config.nativeFacets
+@[inline] def nativeFacets (self : LeanLib) (shouldExport : Bool) : Array (ModuleFacet (BuildJob FilePath)) :=
+  self.config.nativeFacets shouldExport
 
 /--
 The arguments to pass to `lean --server` when running the Lean language server.

src/lake/Lake/Config/LeanLibConfig.lean

@@ -69,11 +69,17 @@ structure LeanLibConfig extends LeanConfig where
   defaultFacets : Array Name := #[LeanLib.leanArtsFacet]
 
   /--
-  An `Array` of module facets to build and combine into the library's static
-  and shared libraries. Defaults to ``#[Module.oFacet]`` (i.e., the object file
-  compiled from the Lean source).
+  The module facets to build and combine into the library's static
+  and shared libraries. If `shouldExport` is true, the module facets should
+  export any symbols a user may expect to lookup in the library. For example,
+  the Lean interpreter will use exported symbols in linked libraries.
+
+  Defaults to a singleton of `Module.oExportFacet` (if `shouldExport`) or
+  `Module.oFacet`. That is, the  object files compiled from the Lean sources,
+  potentially with exported Lean symbols.
   -/
-  nativeFacets : Array (ModuleFacet (BuildJob FilePath)) := #[Module.oFacet]
+  nativeFacets (shouldExport : Bool) : Array (ModuleFacet (BuildJob FilePath)) :=
+    #[if shouldExport then Module.oExportFacet else Module.oFacet]
 
 deriving Inhabited
 

src/lake/Lake/Config/Module.lean

@@ -89,12 +89,15 @@ abbrev pkg (self : Module) : Package :=
 @[inline] def cFile (self : Module) : FilePath :=
   self.irPath "c"
 
+@[inline] def coExportFile (self : Module) : FilePath :=
+  self.irPath "c.o.export"
+
+@[inline] def coNoExportFile (self : Module) : FilePath :=
+  self.irPath "c.o.noexport"
+
 @[inline] def bcFile (self : Module) : FilePath :=
   self.irPath "bc"
 
-@[inline] def coFile (self : Module) : FilePath :=
-  self.irPath "c.o"
-
 @[inline] def bcoFile (self : Module) : FilePath :=
   self.irPath "bc.o"
 
@@ -141,8 +144,8 @@ def dynlibSuffix := "-1"
 @[inline] def shouldPrecompile (self : Module) : Bool :=
   self.lib.precompileModules
 
-@[inline] def nativeFacets (self : Module) : Array (ModuleFacet (BuildJob FilePath)) :=
-  self.lib.nativeFacets
+@[inline] def nativeFacets (self : Module) (shouldExport : Bool) : Array (ModuleFacet (BuildJob FilePath)) :=
+  self.lib.nativeFacets shouldExport
 
 /-! ## Trace Helpers -/
 

src/lake/README.md

@@ -203,7 +203,7 @@ lean_lib «target-name» where
 * `libName`: The `String` name of the library. Used as a base for the file names of its static and dynamic binaries. Defaults to the name of the target.
 * `extraDepTargets`: An `Array` of [target](#custom-targets) names to build before the library's modules.
 * `defaultFacets`: An `Array` of library facets to build on a bare `lake build` of the library. For example, setting this to `#[LeanLib.sharedLib]` will build the shared library facet.
-* `nativeFacets`: An `Array` of [module facets](#defining-new-facets) to build and combine into the library's static and shared libraries. Defaults to ``#[Module.oFacet]`` (i.e., the object file compiled from the Lean source).
+* `nativeFacets`: A function `(shouldExport : Bool) → Array` determining the [module facets](#defining-new-facets) to build and combine into the library's static and shared libraries. If `shouldExport` is true, the module facets should export any symbols a user may expect to lookup in the library. For example, the Lean interpreter will use exported symbols in linked libraries. Defaults to a singleton of `Module.oExportFacet` (if `shouldExport`) or `Module.oFacet`. That is, the object files compiled from the Lean sources, potentially with exported Lean symbols.
 * `platformIndependent`, `precompileModules`, `buildType`, `leanOptions`, `<more|weak><Lean|Leanc|Link>Args`, `moreServerOptions`: Augments the package's corresponding configuration option. The library's arguments come after, modules are precompiled if either the library or package are, `platformIndependent` falls back to the package on `none`, and the build type is the minimum of the two (`debug` is the lowest, and `release` is the highest).
 
 ### Binary Executables
@@ -223,8 +223,8 @@ lean_exe «target-name» where
 * `root`: The root module `Name` of the binary executable. Should include a `main` definition that will serve as the entry point of the program. The root is built by recursively building its local imports (i.e., fellow modules of the workspace). Defaults to the name of the target.
 * `exeName`: The `String` name of the binary executable. Defaults to the target name with any `.` replaced with a `-`.
 * `extraDepTargets`: An `Array` of [target](#custom-targets) names to build before the executable's modules.
-* `nativeFacets`: An `Array` of [module facets](#defining-new-facets) to build and combine into the executable. Defaults to ``#[Module.oFacet]`` (i.e., the object file compiled from the Lean source).
-* `supportInterpreter`: Whether to expose symbols within the executable to the Lean interpreter. This allows the executable to interpret Lean files (e.g., via `Lean.Elab.runFrontend`). Implementation-wise, this passes `-rdynamic` to the linker when building on a non-Windows systems. Defaults to `false`.
+* `nativeFacets`: A function `(shouldExport : Bool) → Array` determining the [module facets](#defining-new-facets) to build and link into the executable. If `shouldExport` is true, the module facets should export any symbols a user may expect to lookup in the library. For example, the Lean interpreter will use exported symbols in linked libraries. Defaults to a singleton of `Module.oExportFacet` (if `shouldExport`) or `Module.oFacet`. That is, the object file compiled from the Lean source, potentially with exported Lean symbols.
+* `supportInterpreter`: Whether to expose symbols within the executable to the Lean interpreter. This allows the executable to interpret Lean files (e.g., via `Lean.Elab.runFrontend`). Implementation-wise, on Windows, the Lean shared libraries are linked to the executable and, on other systems, the executable is linked with `-rdynamic`. This increases the size of the binary on Linux and, on Windows, requires `libInit_shared.dll` and `libleanshared.dll` to be co-located with the executable or part of `PATH` (e.g., via `lake exe`). Thus, this feature should only be enabled when necessary. Defaults to `false`.
 * `platformIndependent`, `precompileModules`, `buildType`, `leanOptions`, `<more|weak><Lean|Leanc|Link>Args`, `moreServerOptions`: Augments the package's corresponding configuration option. The library's arguments come after, modules are precompiled if either the library or package are, `platformIndependent` falls back to the package on `none`, and the build type is the minimum of the two (`debug` is the lowest, and `release` is the highest).
 
 ### External Libraries

src/lake/examples/targets/test.sh

@@ -39,10 +39,10 @@ test ! -f ./.lake/build/lib/Foo/Baz.olean
 $LAKE build +Foo.Baz
 test -f ./.lake/build/lib/Foo/Baz.olean
 
-# Test `.c.o` specifier
-test ! -f ./.lake/build/ir/Bar.c.o
-$LAKE build +Bar:c.o
-test -f ./.lake/build/ir/Bar.c.o
+# Test an object file specifier
+test ! -f ./.lake/build/ir/Bar.c.o.export
+$LAKE build +Bar:c.o.export
+test -f ./.lake/build/ir/Bar.c.o.export
 
 # Test default targets
 test ! -f ./.lake/build/bin/c

src/lake/tests/noBuild/test.sh

@@ -17,8 +17,8 @@ test -f .lake/build/lib/Test.olean
 $LAKE setup-file ./Irrelevant.lean Test --no-build
 
 # Test `--no-build` for file builds (`buildFileUnlessUpToDate`)
-$LAKE build +Test:o --no-build && exit 1 || [ $? = $NO_BUILD_CODE ]
-test ! -f .lake/build/ir/Test.c.o
-$LAKE build +Test:o
-test -f .lake/build/ir/Test.c.o
-$LAKE build +Test:o --no-build
+$LAKE build +Test:c.o.export --no-build && exit 1 || [ $? = $NO_BUILD_CODE ]
+test ! -f .lake/build/ir/Test.c.o.export
+$LAKE build +Test:c.o.export
+test -f .lake/build/ir/Test.c.o.export
+$LAKE build +Test:c.o.export --no-build

src/lean.mk.in

@@ -55,6 +55,7 @@ objs: $(OBJS) $(ALL_NAT_OBJS)
 bin: $(BIN_OUT)/$(BIN_NAME)
 
 lib: $(LIB_OUT)/$(STATIC_LIB_NAME)
+lib.export: $(TEMP_OUT)/$(STATIC_LIB_NAME).export
 
 depends: $(DEPS)
 
@@ -95,6 +96,21 @@ $(BC_OUT)/%.bc: $(OLEAN_OUT)/%.olean
 	@
 endif
 
+ifdef LLVM
+$(TEMP_OUT)/%.o.export: $(BC_OUT)/%.bc
+else
+$(TEMP_OUT)/%.o.export: $(C_OUT)/%.c
+endif
+ifdef CMAKE_LIKE_OUTPUT
+	@echo "[    ] Building $<"
+endif
+	@mkdir -p "$(@D)"
+	$(LEANC) -c -o $@ $< $(LEANC_OPTS) -DLEAN_EXPORTING
+
+# On Windows, rebuild .o not intended for shared libraries
+# without dllexport because of symbol limit;
+# on other platforms, no point in bothering
+ifeq (@CMAKE_SYSTEM_NAME@, Windows)
 ifdef LLVM
 $(TEMP_OUT)/%.o: $(BC_OUT)/%.bc
 else
@@ -104,27 +120,19 @@ ifdef CMAKE_LIKE_OUTPUT
 	@echo "[    ] Building $<"
 endif
 	@mkdir -p "$(@D)"
-ifdef PROFILE
-ifdef LLVM
-	\time -f "%U %S" $(LEANC) -c -o $@ $< $(LEANC_OPTS) 2>&1 > /dev/null | awk '{ printf "LLVM bitcode compilation %fs\n", $$1 + $$2 }' > /dev/stderr
-else
-	\time -f "%U %S" $(LEANC) -c -o $@ $< $(LEANC_OPTS) 2>&1 > /dev/null | awk '{ printf "C compilation %fs\n", $$1 + $$2 }' > /dev/stderr
-endif
-else
 	$(LEANC) -c -o $@ $< $(LEANC_OPTS)
+else
+$(TEMP_OUT)/%.o: $(TEMP_OUT)/%.o.export
+	ln -f $< $@
 endif
 
-$(BIN_OUT)/$(BIN_NAME): $(NAT_OBJS) | $(BIN_OUT)
+$(BIN_OUT)/$(BIN_NAME): $(TEMP_OUT)/$(STATIC_LIB_NAME).export | $(BIN_OUT)
 ifdef CMAKE_LIKE_OUTPUT
 	@echo "[    ] Linking $@"
 endif
 # on Windows, must remove binary before writing a new one (since the old one may be in use)
 	@rm -f $@
-ifdef PROFILE
-	\time -f "%U %S" $(LEANC) -o "$@" $^ $(LEANC_OPTS) $(LINK_OPTS) 2>&1 > /dev/null | awk '{ printf "C linking %fs\n", $$1 + $$2 }' > /dev/stderr
-else
-	$(LEANC) -o "$@" $^ $(LEANC_OPTS) $(LINK_OPTS)
-endif
+	$(LEANC) -o "$@" $< $(LEANC_OPTS) $(LINK_OPTS)
 
 ifeq (@CMAKE_SYSTEM_NAME@, Windows)
 $(LIB_OUT)/$(STATIC_LIB_NAME): $(NAT_OBJS) | $(LIB_OUT)
@@ -132,21 +140,24 @@ $(LIB_OUT)/$(STATIC_LIB_NAME): $(NAT_OBJS) | $(LIB_OUT)
 	$(file >$@.in) $(foreach O,$^,$(file >>$@.in,"$O"))
 	@$(LEAN_AR) rcs $@ @$@.in
 	@rm -f $@.in
+$(TEMP_OUT)/$(STATIC_LIB_NAME).export: $(addsuffix .export,$(NAT_OBJS)) | $(LIB_OUT)
+	@rm -f $@
+	$(file >$@.in) $(foreach O,$^,$(file >>$@.in,"$O"))
+	@$(LEAN_AR) rcs $@ @$@.in
+	@rm -f $@.in
 else
 $(LIB_OUT)/$(STATIC_LIB_NAME): $(NAT_OBJS) | $(LIB_OUT)
 	@rm -f $@
 # no response file support on macOS, but also no need for them
 	@$(LEAN_AR) rcs $@ $^
+$(TEMP_OUT)/$(STATIC_LIB_NAME).export: $(LIB_OUT)/$(STATIC_LIB_NAME)
+	ln -f $< $@
 endif
 
 clean:
 	rm -rf $(OUT)
 
-ifdef LLVM
-.PRECIOUS: $(C_OUT)/%.c $(BC_OUT)/%.bc
-else
-.PRECIOUS: $(C_OUT)/%.c
-endif
+.PRECIOUS: $(BC_OUT)/%.bc $(C_OUT)/%.c $(TEMP_OUT)/%.o $(TEMP_OUT)/%.o.export
 
 ifndef C_ONLY
 include $(DEPS)

src/runtime/CMakeLists.txt

@@ -16,6 +16,10 @@ set_target_properties(leanrt PROPERTIES
 if (NOT MSVC)
 target_compile_options(leanrt PRIVATE -ftls-model=local-exec)
 endif()
+# We do not export Lean symbols when statically linking on Windows.
+if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
+target_compile_options(leanrt PRIVATE -ULEAN_EXPORTING)
+endif()
 
 if(LLVM)
   if (NOT (CMAKE_CXX_COMPILER_ID MATCHES "Clang"))

src/shell/CMakeLists.txt

@@ -87,17 +87,13 @@ FOREACH(T ${LEANDOCEXS})
 ENDFOREACH(T)
 
 # LEAN COMPILER TESTS
-if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
-  message(STATUS "Skipping compiler tests on Windows because of shared library limit on number of exported symbols")
-else()
-  file(GLOB LEANCOMPTESTS "${LEAN_SOURCE_DIR}/../tests/compiler/*.lean")
-  FOREACH(T ${LEANCOMPTESTS})
-    GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
-    add_test(NAME "leancomptest_${T_NAME}"
-             WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler"
-             COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
-  ENDFOREACH(T)
-endif()
+file(GLOB LEANCOMPTESTS "${LEAN_SOURCE_DIR}/../tests/compiler/*.lean")
+FOREACH(T ${LEANCOMPTESTS})
+  GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
+  add_test(NAME "leancomptest_${T_NAME}"
+           WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler"
+           COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}")
+ENDFOREACH(T)
 
 add_test(NAME leancomptest_foreign
          WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler/foreign"

src/stdlib.make.in

@@ -36,19 +36,19 @@ Init:
 	@mkdir -p "${LIB}/lean/Lean" "${LIB}/lean/Lake"
 # Use `+` to use the Make jobserver with `leanmake` for parallelized builds
 # Build `.olean/.o`s of downstream libraries as well for better parallelism
-	+"${LEAN_BIN}/leanmake" objs lib PKG=Init $(LEANMAKE_OPTS) LEANC_OPTS+=-DLEAN_EXPORTING \
+	+"${LEAN_BIN}/leanmake" objs lib lib.export PKG=Init $(LEANMAKE_OPTS) \
 	  EXTRA_SRC_ROOTS="Lean Lean.lean"
 
 Lean: Init
-	+"${LEAN_BIN}/leanmake" lib PKG=Lean $(LEANMAKE_OPTS) LEANC_OPTS+=-DLEAN_EXPORTING
-
+	+"${LEAN_BIN}/leanmake" lib lib.export PKG=Lean $(LEANMAKE_OPTS)
+	
 ${LIB}/temp/empty.c:
 	touch $@
 
 # the following targets are all invoked by separate `make` calls; see src/CMakeLists.txt
 
 # we specify the precise file names here to avoid rebuilds
-${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${LIB}/lean/libInit.a ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LIB}/temp/empty.c
+${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${LIB}/temp/libInit.a.export ${CMAKE_BINARY_DIR}/runtime/libleanrt_initial-exec.a ${LIB}/temp/empty.c
 ifeq "${INIT_SHARED_LINKER_FLAGS}" ""
   # create empty library on platforms without restrictive symbol limits; avoids costly indirections and troubles with cross-library exceptions
 	"${CMAKE_BINARY_DIR}/leanc.sh" -shared -o $@ ${LIB}/temp/empty.c ${TOOLCHAIN_SHARED_LINKER_FLAGS} ${LEANC_OPTS}
@@ -61,7 +61,7 @@ endif
 
 Init_shared: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX}
 
-${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX} ${LIB}/lean/libLean.a ${LIB}/lean/libleancpp.a
+${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libleanshared${CMAKE_SHARED_LIBRARY_SUFFIX}: ${CMAKE_LIBRARY_OUTPUT_DIRECTORY}/libInit_shared${CMAKE_SHARED_LIBRARY_SUFFIX} ${LIB}/temp/libLean.a.export ${LIB}/lean/libleancpp.a
 	@echo "[    ] Building $@"
 # on Windows, must remove file before writing a new one (since the old one may be in use)
 	@rm -f $@

tests/compiler/link_lake.lean

@@ -1,8 +1,6 @@
 -- this should be sufficient to trigger linking against Lake's initializer symbols
--- TODO: uncomment the following line. We commented it to avoid a test failure on Windows.
--- Windows does not allow shared objects with more 2^16 exported symbols :(
 
--- import Lake
---
+import Lake
+
 def main : IO Unit :=
   return

tests/plugin/test_single.sh

@@ -1,7 +1,8 @@
 #!/usr/bin/env bash
 source ../common.sh
 
-compile_lean_c_backend -shared -o "${f%.lean}.so"
+# LEAN_EXPORTING needs to be defined for .c files included in shared libraries
+compile_lean_c_backend -shared -o "${f%.lean}.so" -DLEAN_EXPORTING
 expected_ret=1
 exec_check lean -Dlinter.all=false --plugin="${f%.lean}.so" "$f"
 diff_produced