diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h
index 5bb09ac4f5..cc76e4791f 100644
--- a/src/include/lean/lean.h
+++ b/src/include/lean/lean.h
@@ -272,7 +272,7 @@ typedef struct {
     lean_external_foreach_proc  m_foreach;
 } lean_external_class;
 
-lean_external_class * lean_register_external_class(lean_external_finalize_proc, lean_external_foreach_proc);
+LEAN_SHARED lean_external_class * lean_register_external_class(lean_external_finalize_proc, lean_external_foreach_proc);
 
 /* Object for wrapping external data. */
 typedef struct {
@@ -285,16 +285,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; }
 
-void lean_set_exit_on_panic(bool flag);
+LEAN_SHARED void lean_set_exit_on_panic(bool flag);
 /* Enable/disable panic messages */
-void lean_set_panic_messages(bool flag);
+LEAN_SHARED void lean_set_panic_messages(bool flag);
 
-lean_object * lean_panic_fn(lean_object * default_val, lean_object * msg);
+LEAN_SHARED lean_object * lean_panic_fn(lean_object * default_val, lean_object * msg);
 
-__attribute__((noreturn)) void lean_internal_panic(char const * msg);
-__attribute__((noreturn)) void lean_internal_panic_out_of_memory();
-__attribute__((noreturn)) void lean_internal_panic_unreachable();
-__attribute__((noreturn)) void lean_internal_panic_rc_overflow();
+LEAN_SHARED __attribute__((noreturn)) void lean_internal_panic(char const * msg);
+LEAN_SHARED __attribute__((noreturn)) void lean_internal_panic_out_of_memory();
+LEAN_SHARED __attribute__((noreturn)) void lean_internal_panic_unreachable();
+LEAN_SHARED __attribute__((noreturn)) void lean_internal_panic_rc_overflow();
 
 static inline size_t lean_align(size_t v, size_t a) {
     return (v / a)*a + a * (v % a != 0);
@@ -306,10 +306,10 @@ static inline unsigned lean_get_slot_idx(unsigned sz) {
     return sz / LEAN_OBJECT_SIZE_DELTA - 1;
 }
 
-void * lean_alloc_small(unsigned sz, unsigned slot_idx);
-void lean_free_small(void * p);
-unsigned lean_small_mem_size(void * p);
-void lean_inc_heartbeat();
+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();
 
 static inline lean_object * lean_alloc_small_object(unsigned sz) {
 #ifdef LEAN_SMALL_ALLOCATOR
@@ -367,8 +367,8 @@ static inline void lean_free_small_object(lean_object * o) {
 #endif
 }
 
-lean_object * lean_alloc_object(size_t sz);
-void lean_free_object(lean_object * o);
+LEAN_SHARED lean_object * lean_alloc_object(size_t sz);
+LEAN_SHARED void lean_free_object(lean_object * o);
 
 static inline uint8_t lean_ptr_tag(lean_object * o) {
     return o->m_tag;
@@ -383,7 +383,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 */
-size_t lean_object_byte_size(lean_object * o);
+LEAN_SHARED size_t lean_object_byte_size(lean_object * o);
 
 static inline bool lean_is_mt(lean_object * o) {
     return o->m_rc < 0;
@@ -406,8 +406,8 @@ static inline _Atomic(int) * lean_get_rc_mt_addr(lean_object* o) {
     return (_Atomic(int)*)(&(o->m_rc));
 }
 
-void lean_inc_ref_cold(lean_object * o);
-void lean_inc_ref_n_cold(lean_object * o, unsigned n);
+LEAN_SHARED void lean_inc_ref_cold(lean_object * o);
+LEAN_SHARED 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))) {
@@ -425,7 +425,7 @@ static inline void lean_inc_ref_n(lean_object * o, size_t n) {
     }
 }
 
-void lean_dec_ref_cold(lean_object * o);
+LEAN_SHARED void lean_dec_ref_cold(lean_object * o);
 
 static inline void lean_dec_ref(lean_object * o) {
     if (LEAN_LIKELY(o->m_rc > 1)) {
@@ -439,7 +439,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 */
-void lean_dealloc(lean_object * o);
+LEAN_SHARED 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; }
@@ -482,8 +482,8 @@ static inline bool lean_is_shared(lean_object * o) {
     }
 }
 
-void lean_mark_mt(lean_object * o);
-void lean_mark_persistent(lean_object * o);
+LEAN_SHARED void lean_mark_mt(lean_object * o);
+LEAN_SHARED 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;
@@ -640,34 +640,34 @@ 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_object* lean_apply_1(lean_object* f, lean_object* a1);
-lean_object* lean_apply_2(lean_object* f, lean_object* a1, lean_object* a2);
-lean_object* lean_apply_3(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3);
-lean_object* lean_apply_4(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4);
-lean_object* lean_apply_5(lean_object* f, lean_object* a1, lean_object* a2, lean_object* a3, lean_object* a4, lean_object* a5);
-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_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_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_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_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_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_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_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_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_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_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_object* lean_apply_n(lean_object* f, unsigned n, lean_object** args);
+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);
 /* Pre: n > 16 */
-lean_object* lean_apply_m(lean_object* f, unsigned n, lean_object** args);
+LEAN_SHARED lean_object* lean_apply_m(lean_object* f, unsigned n, lean_object** args);
 
 /* Fixpoint */
 
-lean_obj_res lean_fixpoint(lean_obj_arg rec, lean_obj_arg a);
-lean_obj_res lean_fixpoint2(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2);
-lean_obj_res lean_fixpoint3(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2, lean_obj_arg a3);
-lean_obj_res lean_fixpoint4(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2, lean_obj_arg a3, lean_obj_arg a4);
-lean_obj_res lean_fixpoint5(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2, lean_obj_arg a3, lean_obj_arg a4, lean_obj_arg a5);
-lean_obj_res lean_fixpoint6(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2, lean_obj_arg a3, lean_obj_arg a4, lean_obj_arg a5, lean_obj_arg a6);
+LEAN_SHARED lean_obj_res lean_fixpoint(lean_obj_arg rec, lean_obj_arg a);
+LEAN_SHARED lean_obj_res lean_fixpoint2(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2);
+LEAN_SHARED lean_obj_res lean_fixpoint3(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2, lean_obj_arg a3);
+LEAN_SHARED lean_obj_res lean_fixpoint4(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2, lean_obj_arg a3, lean_obj_arg a4);
+LEAN_SHARED lean_obj_res lean_fixpoint5(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2, lean_obj_arg a3, lean_obj_arg a4, lean_obj_arg a5);
+LEAN_SHARED lean_obj_res lean_fixpoint6(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2, lean_obj_arg a3, lean_obj_arg a4, lean_obj_arg a5, lean_obj_arg a6);
 
 /* Arrays of objects (low level API) */
 static inline lean_obj_res lean_alloc_array(size_t size, size_t capacity) {
@@ -700,8 +700,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_object * lean_array_mk(lean_obj_arg l);
-lean_object * lean_array_data(lean_obj_arg a);
+LEAN_SHARED lean_object * lean_array_mk(lean_obj_arg l);
+LEAN_SHARED lean_object * lean_array_data(lean_obj_arg a);
 
 /* Arrays of objects (high level API) */
 
@@ -733,7 +733,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_obj_res lean_array_get_panic(lean_obj_arg def_val);
+LEAN_SHARED 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)) {
@@ -750,7 +750,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_obj_res lean_copy_expand_array(lean_obj_arg a, bool expand);
+LEAN_SHARED 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);
@@ -773,7 +773,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_obj_res lean_array_set_panic(lean_obj_arg a, lean_obj_arg v);
+LEAN_SHARED 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)) {
@@ -818,8 +818,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_object * lean_array_push(lean_obj_arg a, lean_obj_arg v);
-lean_object * lean_mk_array(lean_obj_arg n, lean_obj_arg v);
+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);
 
 /* Array of scalars */
 
@@ -850,9 +850,9 @@ static inline uint8_t* lean_sarray_cptr(lean_object * o) { return lean_to_sarray
 
 /* ByteArray (special case of Array of Scalars) */
 
-lean_obj_res lean_byte_array_mk(lean_obj_arg a);
-lean_obj_res lean_byte_array_data(lean_obj_arg a);
-lean_obj_res lean_copy_byte_array(lean_obj_arg a);
+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);
 
 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();
@@ -873,7 +873,7 @@ static inline uint8_t lean_byte_array_get(b_lean_obj_arg a, b_lean_obj_arg i) {
     }
 }
 
-lean_obj_res lean_byte_array_push(lean_obj_arg a, uint8_t b);
+LEAN_SHARED lean_obj_res lean_byte_array_push(lean_obj_arg a, uint8_t b);
 
 static inline lean_obj_res lean_byte_array_set(lean_obj_arg a, b_lean_obj_arg i, uint8_t b) {
     if (!lean_is_scalar(i)) {
@@ -895,9 +895,9 @@ static inline lean_obj_res lean_byte_array_set(lean_obj_arg a, b_lean_obj_arg i,
 
 /* FloatArray (special case of Array of Scalars) */
 
-lean_obj_res lean_float_array_mk(lean_obj_arg a);
-lean_obj_res lean_float_array_data(lean_obj_arg a);
-lean_obj_res lean_copy_float_array(lean_obj_arg a);
+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);
 
 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();
@@ -922,7 +922,7 @@ static inline double lean_float_array_get(b_lean_obj_arg a, b_lean_obj_arg i) {
     }
 }
 
-lean_obj_res lean_float_array_push(lean_obj_arg a, double d);
+LEAN_SHARED lean_obj_res lean_float_array_push(lean_obj_arg a, double d);
 
 static inline lean_obj_res lean_float_array_set(lean_obj_arg a, b_lean_obj_arg i, double d) {
     if (!lean_is_scalar(i)) {
@@ -967,42 +967,42 @@ static inline lean_obj_res lean_alloc_string(size_t size, size_t capacity, size_
     o->m_length = len;
     return (lean_object*)o;
 }
-size_t lean_utf8_strlen(char const * str);
-size_t lean_utf8_n_strlen(char const * str, size_t n);
+LEAN_SHARED size_t lean_utf8_strlen(char const * str);
+LEAN_SHARED 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_obj_res lean_mk_string(char const * s);
+LEAN_SHARED 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_obj_res lean_string_push(lean_obj_arg s, uint32_t c);
-lean_obj_res lean_string_append(lean_obj_arg s1, b_lean_obj_arg s2);
+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);
 static inline lean_obj_res lean_string_length(b_lean_obj_arg s) { return lean_box(lean_string_len(s)); }
-lean_obj_res lean_string_mk(lean_obj_arg cs);
-lean_obj_res lean_string_data(lean_obj_arg s);
-uint32_t  lean_string_utf8_get(b_lean_obj_arg s, b_lean_obj_arg i);
-lean_obj_res lean_string_utf8_next(b_lean_obj_arg s, b_lean_obj_arg i);
-lean_obj_res lean_string_utf8_prev(b_lean_obj_arg s, b_lean_obj_arg i);
-lean_obj_res lean_string_utf8_set(lean_obj_arg s, b_lean_obj_arg i, uint32_t c);
+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 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_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);
 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_obj_res lean_string_utf8_extract(b_lean_obj_arg s, b_lean_obj_arg b, b_lean_obj_arg e);
+LEAN_SHARED 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); }
 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) && memcmp(lean_string_cstr(s1), lean_string_cstr(s2), lean_string_size(s1)) == 0);
 }
 static inline bool lean_string_ne(b_lean_obj_arg s1, b_lean_obj_arg s2) { return !lean_string_eq(s1, s2); }
-bool lean_string_lt(b_lean_obj_arg s1, b_lean_obj_arg s2);
+LEAN_SHARED 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); }
-uint64_t lean_string_hash(b_lean_obj_arg);
+LEAN_SHARED uint64_t lean_string_hash(b_lean_obj_arg);
 
 /* Thunks */
 
@@ -1023,7 +1023,7 @@ static inline lean_obj_res lean_thunk_pure(lean_obj_arg v) {
     return (lean_object*)o;
 }
 
-lean_object * lean_thunk_get_core(lean_object * t);
+LEAN_SHARED 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;
@@ -1040,21 +1040,21 @@ static inline lean_obj_res lean_thunk_get_own(b_lean_obj_arg t) {
 
 /* Tasks */
 
-void lean_init_task_manager();
-void lean_init_task_manager_using(unsigned num_workers);
+LEAN_SHARED void lean_init_task_manager();
+LEAN_SHARED void lean_init_task_manager_using(unsigned num_workers);
 
-lean_obj_res lean_task_spawn_core(lean_obj_arg c, unsigned prio, bool keep_alive);
+LEAN_SHARED 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_obj_res lean_task_pure(lean_obj_arg a);
-lean_obj_res lean_task_bind_core(lean_obj_arg x, lean_obj_arg f, unsigned prio, bool keep_alive);
+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 keep_alive);
 /* Task.bind (x : Task A) (f : A -> Task B) (prio : Nat) : Task B */
 static inline lean_obj_res lean_task_bind(lean_obj_arg x, lean_obj_arg f, lean_obj_arg prio) { return lean_task_bind_core(x, f, lean_unbox(prio), false); }
-lean_obj_res lean_task_map_core(lean_obj_arg f, lean_obj_arg t, unsigned prio, bool keep_alive);
+LEAN_SHARED lean_obj_res lean_task_map_core(lean_obj_arg f, lean_obj_arg t, unsigned prio, bool keep_alive);
 /* Task.map (f : A -> B) (t : Task A) (prio : Nat) : Task B */
 static inline lean_obj_res lean_task_map(lean_obj_arg f, lean_obj_arg t, lean_obj_arg prio) { return lean_task_map_core(f, t, lean_unbox(prio), false); }
-b_lean_obj_res lean_task_get(b_lean_obj_arg t);
+LEAN_SHARED 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);
@@ -1064,13 +1064,13 @@ static inline lean_obj_res lean_task_get_own(lean_obj_arg t) {
 }
 
 /* primitive for implementing `IO.checkCanceled : IO Bool` */
-bool lean_io_check_canceled_core();
+LEAN_SHARED bool lean_io_check_canceled_core();
 /* primitive for implementing `IO.cancel : Task a -> IO Unit` */
-void lean_io_cancel_core(b_lean_obj_arg t);
+LEAN_SHARED void lean_io_cancel_core(b_lean_obj_arg t);
 /* primitive for implementing `IO.hasFinished : Task a -> IO Unit` */
-bool lean_io_has_finished_core(b_lean_obj_arg t);
+LEAN_SHARED bool lean_io_has_finished_core(b_lean_obj_arg t);
 /* primitive for implementing `IO.waitAny : List (Task a) -> IO (Task a)` */
-b_lean_obj_res lean_io_wait_any_core(b_lean_obj_arg task_list);
+LEAN_SHARED b_lean_obj_res lean_io_wait_any_core(b_lean_obj_arg task_list);
 
 /* External objects */
 
@@ -1094,23 +1094,23 @@ static inline void * lean_get_external_data(lean_object * o) {
 
 #define LEAN_MAX_SMALL_NAT (SIZE_MAX >> 1)
 
-lean_object * lean_nat_big_succ(lean_object * a);
-lean_object * lean_nat_big_add(lean_object * a1, lean_object * a2);
-lean_object * lean_nat_big_sub(lean_object * a1, lean_object * a2);
-lean_object * lean_nat_big_mul(lean_object * a1, lean_object * a2);
-lean_object * lean_nat_overflow_mul(size_t a1, size_t a2);
-lean_object * lean_nat_big_div(lean_object * a1, lean_object * a2);
-lean_object * lean_nat_big_mod(lean_object * a1, lean_object * a2);
-bool lean_nat_big_eq(lean_object * a1, lean_object * a2);
-bool lean_nat_big_le(lean_object * a1, lean_object * a2);
-bool lean_nat_big_lt(lean_object * a1, lean_object * a2);
-lean_object * lean_nat_big_land(lean_object * a1, lean_object * a2);
-lean_object * lean_nat_big_lor(lean_object * a1, lean_object * a2);
-lean_object * lean_nat_big_xor(lean_object * a1, lean_object * a2);
+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_obj_res lean_cstr_to_nat(char const * n);
-lean_obj_res lean_big_usize_to_nat(size_t n);
-lean_obj_res lean_big_uint64_to_nat(uint64_t n);
+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);
 static inline lean_obj_res lean_usize_to_nat(size_t n) {
     if (LEAN_LIKELY(n <= LEAN_MAX_SMALL_NAT))
         return lean_box(n);
@@ -1260,30 +1260,30 @@ static inline lean_obj_res lean_nat_lxor(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     }
 }
 
-lean_obj_res lean_nat_shiftl(b_lean_obj_arg a1, b_lean_obj_arg a2);
-lean_obj_res lean_nat_shiftr(b_lean_obj_arg a1, b_lean_obj_arg a2);
-lean_obj_res lean_nat_pow(b_lean_obj_arg a1, b_lean_obj_arg a2);
-lean_obj_res lean_nat_gcd(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);
 
 /* Integers */
 
 #define LEAN_MAX_SMALL_INT (sizeof(void*) == 8 ? INT_MAX : (1 << 30))
 #define LEAN_MIN_SMALL_INT (sizeof(void*) == 8 ? INT_MIN : -(1 << 30))
-lean_object * lean_int_big_neg(lean_object * a);
-lean_object * lean_int_big_add(lean_object * a1, lean_object * a2);
-lean_object * lean_int_big_sub(lean_object * a1, lean_object * a2);
-lean_object * lean_int_big_mul(lean_object * a1, lean_object * a2);
-lean_object * lean_int_big_div(lean_object * a1, lean_object * a2);
-lean_object * lean_int_big_mod(lean_object * a1, lean_object * a2);
-bool lean_int_big_eq(lean_object * a1, lean_object * a2);
-bool lean_int_big_le(lean_object * a1, lean_object * a2);
-bool lean_int_big_lt(lean_object * a1, lean_object * a2);
-bool lean_int_big_nonneg(lean_object * a);
+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 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_object * lean_cstr_to_int(char const * n);
-lean_object * lean_big_int_to_int(int n);
-lean_object * lean_big_size_t_to_int(size_t n);
-lean_object * lean_big_int64_to_int(int64_t n);
+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);
 
 static inline lean_obj_res lean_int_to_int(int n) {
     if (sizeof(void*) == 8)
@@ -1444,7 +1444,7 @@ static inline bool lean_int_lt(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     }
 }
 
-lean_obj_res lean_big_int_to_nat(lean_obj_arg a);
+LEAN_SHARED 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)) {
@@ -1479,7 +1479,7 @@ static inline uint8_t lean_int_dec_nonneg(b_lean_obj_arg a) {
 
 /* UInt8 */
 
-uint8_t lean_uint8_of_big_nat(b_lean_obj_arg a);
+LEAN_SHARED 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; }
@@ -1503,7 +1503,7 @@ static inline uint8_t lean_uint8_dec_le(uint8_t a1, uint8_t a2) { return a1 <= a
 
 /* UInt16 */
 
-uint16_t lean_uint16_of_big_nat(b_lean_obj_arg a);
+LEAN_SHARED 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; }
@@ -1527,7 +1527,7 @@ static inline uint8_t lean_uint16_dec_le(uint16_t a1, uint16_t a2) { return a1 <
 
 /* UInt32 */
 
-uint32_t lean_uint32_of_big_nat(b_lean_obj_arg a);
+LEAN_SHARED 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; }
@@ -1537,7 +1537,7 @@ static inline uint32_t lean_uint32_sub(uint32_t a1, uint32_t a2) { return a1-a2;
 static inline uint32_t lean_uint32_mul(uint32_t a1, uint32_t a2) { return a1*a2; }
 static inline uint32_t lean_uint32_div(uint32_t a1, uint32_t a2) { return a2 == 0 ? 0  : a1/a2; }
 static inline uint32_t lean_uint32_mod(uint32_t a1, uint32_t a2) { return a2 == 0 ? a1 : a1%a2; }
-uint32_t lean_uint32_big_modn(uint32_t a1, b_lean_obj_arg a2);
+LEAN_SHARED 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);
@@ -1556,7 +1556,7 @@ static inline uint8_t lean_uint32_dec_le(uint32_t a1, uint32_t a2) { return a1 <
 
 /* UInt64 */
 
-uint64_t lean_uint64_of_big_nat(b_lean_obj_arg a);
+LEAN_SHARED 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; }
@@ -1565,7 +1565,7 @@ static inline uint64_t lean_uint64_sub(uint64_t a1, uint64_t a2) { return a1-a2;
 static inline uint64_t lean_uint64_mul(uint64_t a1, uint64_t a2) { return a1*a2; }
 static inline uint64_t lean_uint64_div(uint64_t a1, uint64_t a2) { return a2 == 0 ? 0  : a1/a2; }
 static inline uint64_t lean_uint64_mod(uint64_t a1, uint64_t a2) { return a2 == 0 ? a1 : a1%a2; }
-uint64_t lean_uint64_big_modn(uint64_t a1, b_lean_obj_arg a2);
+LEAN_SHARED 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);
@@ -1577,11 +1577,11 @@ static inline uint64_t lean_uint64_modn(uint64_t a1, b_lean_obj_arg a2) {
 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; }
-uint64_t lean_uint64_mix_hash(uint64_t a1, uint64_t a2);
+LEAN_SHARED uint64_t lean_uint64_mix_hash(uint64_t a1, uint64_t a2);
 
 /* USize */
 
-size_t lean_usize_of_big_nat(b_lean_obj_arg a);
+LEAN_SHARED 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; }
@@ -1590,7 +1590,7 @@ static inline size_t lean_usize_sub(size_t a1, size_t a2) { return a1-a2; }
 static inline size_t lean_usize_mul(size_t a1, size_t a2) { return a1*a2; }
 static inline size_t lean_usize_div(size_t a1, size_t a2) { return a2 == 0 ? 0  : a1/a2; }
 static inline size_t lean_usize_mod(size_t a1, size_t a2) { return a2 == 0 ? a1 : a1%a2; }
-size_t lean_usize_big_modn(size_t a1, b_lean_obj_arg a2);
+LEAN_SHARED 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);
@@ -1602,12 +1602,12 @@ static inline size_t lean_usize_modn(size_t a1, b_lean_obj_arg a2) {
 static inline uint8_t lean_usize_dec_eq(size_t a1, size_t a2) { return a1 == a2; }
 static inline uint8_t lean_usize_dec_lt(size_t a1, size_t a2) { return a1 < a2; }
 static inline uint8_t lean_usize_dec_le(size_t a1, size_t a2) { return a1 <= a2; }
-size_t lean_usize_mix_hash(size_t a1, size_t a2);
+LEAN_SHARED size_t lean_usize_mix_hash(size_t a1, size_t a2);
 
 /* Float */
 
-double lean_float_of_nat(b_lean_obj_arg a);
-lean_obj_res lean_float_to_string(double a);
+LEAN_SHARED double lean_float_of_nat(b_lean_obj_arg a);
+LEAN_SHARED lean_obj_res lean_float_to_string(double a);
 
 /* Boxing primitives */
 
@@ -1665,21 +1665,21 @@ static inline double lean_unbox_float(b_lean_obj_arg o) {
 
 /* Debugging helper functions */
 
-lean_object * lean_dbg_trace(lean_obj_arg s, lean_obj_arg fn);
-lean_object * lean_dbg_sleep(uint32_t ms, lean_obj_arg fn);
-lean_object * lean_dbg_trace_if_shared(lean_obj_arg s, lean_obj_arg a);
+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);
 
 /* IO Helper functions */
 
-lean_obj_res lean_decode_io_error(int errnum, b_lean_obj_arg fname);
+LEAN_SHARED 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); }
-void lean_io_result_show_error(b_lean_obj_arg r);
-void lean_io_mark_end_initialization();
+LEAN_SHARED void lean_io_result_show_error(b_lean_obj_arg r);
+LEAN_SHARED void lean_io_mark_end_initialization();
 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);
@@ -1693,45 +1693,45 @@ static inline lean_obj_res lean_io_result_mk_error(lean_obj_arg e) {
     return r;
 }
 
-lean_obj_res lean_mk_io_error_already_exists(uint32_t, lean_obj_arg);
-lean_obj_res lean_mk_io_error_already_exists_file(lean_obj_arg, uint32_t, lean_obj_arg);
-lean_obj_res lean_mk_io_error_eof(lean_obj_arg);
-lean_obj_res lean_mk_io_error_hardware_fault(uint32_t, lean_obj_arg);
-lean_obj_res lean_mk_io_error_illegal_operation(uint32_t, lean_obj_arg);
-lean_obj_res lean_mk_io_error_inappropriate_type(uint32_t, lean_obj_arg);
-lean_obj_res lean_mk_io_error_inappropriate_type_file(lean_obj_arg, uint32_t, lean_obj_arg);
-lean_obj_res lean_mk_io_error_interrupted(lean_obj_arg, uint32_t, lean_obj_arg);
-lean_obj_res lean_mk_io_error_invalid_argument(uint32_t, lean_obj_arg);
-lean_obj_res lean_mk_io_error_invalid_argument_file(lean_obj_arg, uint32_t, lean_obj_arg);
-lean_obj_res lean_mk_io_error_no_file_or_directory(lean_obj_arg, uint32_t, lean_obj_arg);
-lean_obj_res lean_mk_io_error_no_such_thing(uint32_t, lean_obj_arg);
-lean_obj_res lean_mk_io_error_no_such_thing_file(lean_obj_arg, uint32_t, lean_obj_arg);
-lean_obj_res lean_mk_io_error_other_error(uint32_t, lean_obj_arg);
-lean_obj_res lean_mk_io_error_permission_denied(uint32_t, lean_obj_arg);
-lean_obj_res lean_mk_io_error_permission_denied_file(lean_obj_arg, uint32_t, lean_obj_arg);
-lean_obj_res lean_mk_io_error_protocol_error(uint32_t, lean_obj_arg);
-lean_obj_res lean_mk_io_error_resource_busy(uint32_t, lean_obj_arg);
-lean_obj_res lean_mk_io_error_resource_exhausted(uint32_t, lean_obj_arg);
-lean_obj_res lean_mk_io_error_resource_exhausted_file(lean_obj_arg, uint32_t, lean_obj_arg);
-lean_obj_res lean_mk_io_error_resource_vanished(uint32_t, lean_obj_arg);
-lean_obj_res lean_mk_io_error_time_expired(uint32_t, lean_obj_arg);
-lean_obj_res lean_mk_io_error_unsatisfied_constraints(uint32_t, lean_obj_arg);
-lean_obj_res lean_mk_io_error_unsupported_operation(uint32_t, lean_obj_arg);
-lean_obj_res lean_mk_io_user_error(lean_obj_arg str);
+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);
 
 
 /* ST Ref primitives */
-lean_obj_res lean_st_mk_ref(lean_obj_arg, lean_obj_arg);
-lean_obj_res lean_st_ref_get(b_lean_obj_arg, lean_obj_arg);
-lean_obj_res lean_st_ref_set(b_lean_obj_arg, lean_obj_arg, lean_obj_arg);
-lean_obj_res lean_st_ref_reset(b_lean_obj_arg, lean_obj_arg);
-lean_obj_res lean_st_ref_swap(b_lean_obj_arg, lean_obj_arg, lean_obj_arg);
+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);
 
 /* pointer address unsafe primitive  */
 static inline size_t lean_ptr_addr(b_lean_obj_arg a) { return (size_t)a; }
 
 /* Name primitives */
-uint8_t lean_name_eq(b_lean_obj_arg n1, b_lean_obj_arg n2);
+LEAN_SHARED 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));
diff --git a/src/include/lean/lean_gmp.h b/src/include/lean/lean_gmp.h
index f9a33debff..9bf971e818 100644
--- a/src/include/lean/lean_gmp.h
+++ b/src/include/lean/lean_gmp.h
@@ -12,12 +12,12 @@ Author: Leonardo de Moura
 extern "C" {
 #endif
 
-lean_object * lean_alloc_mpz(mpz_t);
+LEAN_SHARED 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).
 */
-void lean_extract_mpz_value(lean_object * o, mpz_t v);
+LEAN_SHARED void lean_extract_mpz_value(lean_object * o, mpz_t v);
 
 #ifdef __cplusplus
 }