lean-rs-sys 0.1.0

Raw FFI bindings for the Lean 4 C ABI. See `lean-rs` for the safe front door.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233

//! Link-time probe: take the address of every symbol in [`REQUIRED_SYMBOLS`].
//! If `libleanshared` is missing any of them the test binary fails to link.

use lean_rs_sys::REQUIRED_SYMBOLS;

#[test]
fn all_required_symbols_resolve_at_link_time() {
    let addresses: &[(*const (), &str)] = &[
        // init / runtime
        (lean_rs_sys::init::lean_initialize as *const (), "lean_initialize"),
        (
            lean_rs_sys::init::lean_initialize_runtime_module as *const (),
            "lean_initialize_runtime_module",
        ),
        (
            lean_rs_sys::init::lean_initialize_thread as *const (),
            "lean_initialize_thread",
        ),
        (
            lean_rs_sys::init::lean_finalize_thread as *const (),
            "lean_finalize_thread",
        ),
        (lean_rs_sys::init::lean_setup_args as *const (), "lean_setup_args"),
        (
            lean_rs_sys::init::lean_init_task_manager as *const (),
            "lean_init_task_manager",
        ),
        (
            lean_rs_sys::init::lean_init_task_manager_using as *const (),
            "lean_init_task_manager_using",
        ),
        (
            lean_rs_sys::init::lean_finalize_task_manager as *const (),
            "lean_finalize_task_manager",
        ),
        // refcount + marking
        (
            lean_rs_sys::refcount::lean_dec_ref_cold as *const (),
            "lean_dec_ref_cold",
        ),
        (lean_rs_sys::refcount::lean_mark_mt as *const (), "lean_mark_mt"),
        (
            lean_rs_sys::refcount::lean_mark_persistent as *const (),
            "lean_mark_persistent",
        ),
        // object / allocators
        (lean_rs_sys::object::lean_alloc_object as *const (), "lean_alloc_object"),
        (lean_rs_sys::object::lean_free_object as *const (), "lean_free_object"),
        (
            lean_rs_sys::object::lean_object_byte_size as *const (),
            "lean_object_byte_size",
        ),
        (
            lean_rs_sys::object::lean_object_data_byte_size as *const (),
            "lean_object_data_byte_size",
        ),
        // arrays
        (lean_rs_sys::array::lean_array_mk as *const (), "lean_array_mk"),
        (lean_rs_sys::array::lean_array_push as *const (), "lean_array_push"),
        (
            lean_rs_sys::array::lean_array_to_list as *const (),
            "lean_array_to_list",
        ),
        (
            lean_rs_sys::array::lean_array_get_panic as *const (),
            "lean_array_get_panic",
        ),
        (
            lean_rs_sys::array::lean_array_set_panic as *const (),
            "lean_array_set_panic",
        ),
        // strings
        (lean_rs_sys::string::lean_mk_string as *const (), "lean_mk_string"),
        (
            lean_rs_sys::string::lean_mk_string_unchecked as *const (),
            "lean_mk_string_unchecked",
        ),
        (
            lean_rs_sys::string::lean_mk_string_from_bytes as *const (),
            "lean_mk_string_from_bytes",
        ),
        (
            lean_rs_sys::string::lean_mk_string_from_bytes_unchecked as *const (),
            "lean_mk_string_from_bytes_unchecked",
        ),
        (
            lean_rs_sys::string::lean_mk_ascii_string_unchecked as *const (),
            "lean_mk_ascii_string_unchecked",
        ),
        (lean_rs_sys::string::lean_string_push as *const (), "lean_string_push"),
        (
            lean_rs_sys::string::lean_string_append as *const (),
            "lean_string_append",
        ),
        (lean_rs_sys::string::lean_string_mk as *const (), "lean_string_mk"),
        (lean_rs_sys::string::lean_string_data as *const (), "lean_string_data"),
        (
            lean_rs_sys::string::lean_string_utf8_get as *const (),
            "lean_string_utf8_get",
        ),
        (
            lean_rs_sys::string::lean_string_utf8_next as *const (),
            "lean_string_utf8_next",
        ),
        (
            lean_rs_sys::string::lean_string_utf8_prev as *const (),
            "lean_string_utf8_prev",
        ),
        (
            lean_rs_sys::string::lean_string_utf8_set as *const (),
            "lean_string_utf8_set",
        ),
        (
            lean_rs_sys::string::lean_string_utf8_extract as *const (),
            "lean_string_utf8_extract",
        ),
        (
            lean_rs_sys::string::lean_string_eq_cold as *const (),
            "lean_string_eq_cold",
        ),
        (lean_rs_sys::string::lean_string_lt as *const (), "lean_string_lt"),
        (lean_rs_sys::string::lean_string_hash as *const (), "lean_string_hash"),
        (lean_rs_sys::string::lean_utf8_strlen as *const (), "lean_utf8_strlen"),
        (
            lean_rs_sys::string::lean_utf8_n_strlen as *const (),
            "lean_utf8_n_strlen",
        ),
        // Nat bignum
        (
            lean_rs_sys::nat_int::lean_nat_big_succ as *const (),
            "lean_nat_big_succ",
        ),
        (lean_rs_sys::nat_int::lean_nat_big_add as *const (), "lean_nat_big_add"),
        (lean_rs_sys::nat_int::lean_nat_big_sub as *const (), "lean_nat_big_sub"),
        (lean_rs_sys::nat_int::lean_nat_big_mul as *const (), "lean_nat_big_mul"),
        (lean_rs_sys::nat_int::lean_nat_big_div as *const (), "lean_nat_big_div"),
        (lean_rs_sys::nat_int::lean_nat_big_mod as *const (), "lean_nat_big_mod"),
        (lean_rs_sys::nat_int::lean_nat_big_eq as *const (), "lean_nat_big_eq"),
        (lean_rs_sys::nat_int::lean_nat_big_le as *const (), "lean_nat_big_le"),
        (lean_rs_sys::nat_int::lean_nat_big_lt as *const (), "lean_nat_big_lt"),
        (
            lean_rs_sys::nat_int::lean_nat_overflow_mul as *const (),
            "lean_nat_overflow_mul",
        ),
        // Int bignum
        (lean_rs_sys::nat_int::lean_int_big_neg as *const (), "lean_int_big_neg"),
        (lean_rs_sys::nat_int::lean_int_big_add as *const (), "lean_int_big_add"),
        (lean_rs_sys::nat_int::lean_int_big_sub as *const (), "lean_int_big_sub"),
        (lean_rs_sys::nat_int::lean_int_big_mul as *const (), "lean_int_big_mul"),
        (lean_rs_sys::nat_int::lean_int_big_div as *const (), "lean_int_big_div"),
        (lean_rs_sys::nat_int::lean_int_big_mod as *const (), "lean_int_big_mod"),
        (lean_rs_sys::nat_int::lean_int_big_eq as *const (), "lean_int_big_eq"),
        (lean_rs_sys::nat_int::lean_int_big_le as *const (), "lean_int_big_le"),
        (lean_rs_sys::nat_int::lean_int_big_lt as *const (), "lean_int_big_lt"),
        (
            lean_rs_sys::nat_int::lean_int_big_nonneg as *const (),
            "lean_int_big_nonneg",
        ),
        // Widening
        (
            lean_rs_sys::nat_int::lean_big_usize_to_nat as *const (),
            "lean_big_usize_to_nat",
        ),
        (
            lean_rs_sys::nat_int::lean_big_uint64_to_nat as *const (),
            "lean_big_uint64_to_nat",
        ),
        (lean_rs_sys::nat_int::lean_cstr_to_nat as *const (), "lean_cstr_to_nat"),
        (
            lean_rs_sys::nat_int::lean_big_int_to_int as *const (),
            "lean_big_int_to_int",
        ),
        (
            lean_rs_sys::nat_int::lean_big_size_t_to_int as *const (),
            "lean_big_size_t_to_int",
        ),
        (
            lean_rs_sys::nat_int::lean_big_int64_to_int as *const (),
            "lean_big_int64_to_int",
        ),
        (lean_rs_sys::nat_int::lean_cstr_to_int as *const (), "lean_cstr_to_int"),
        (
            lean_rs_sys::nat_int::lean_uint8_of_big_nat as *const (),
            "lean_uint8_of_big_nat",
        ),
        // closure dispatch
        (lean_rs_sys::closure::lean_apply_1 as *const (), "lean_apply_1"),
        (lean_rs_sys::closure::lean_apply_2 as *const (), "lean_apply_2"),
        (lean_rs_sys::closure::lean_apply_3 as *const (), "lean_apply_3"),
        (lean_rs_sys::closure::lean_apply_4 as *const (), "lean_apply_4"),
        (lean_rs_sys::closure::lean_apply_5 as *const (), "lean_apply_5"),
        (lean_rs_sys::closure::lean_apply_6 as *const (), "lean_apply_6"),
        (lean_rs_sys::closure::lean_apply_7 as *const (), "lean_apply_7"),
        (lean_rs_sys::closure::lean_apply_8 as *const (), "lean_apply_8"),
        (lean_rs_sys::closure::lean_apply_9 as *const (), "lean_apply_9"),
        (lean_rs_sys::closure::lean_apply_10 as *const (), "lean_apply_10"),
        (lean_rs_sys::closure::lean_apply_11 as *const (), "lean_apply_11"),
        (lean_rs_sys::closure::lean_apply_12 as *const (), "lean_apply_12"),
        (lean_rs_sys::closure::lean_apply_13 as *const (), "lean_apply_13"),
        (lean_rs_sys::closure::lean_apply_14 as *const (), "lean_apply_14"),
        (lean_rs_sys::closure::lean_apply_15 as *const (), "lean_apply_15"),
        (lean_rs_sys::closure::lean_apply_16 as *const (), "lean_apply_16"),
        (lean_rs_sys::closure::lean_apply_n as *const (), "lean_apply_n"),
        (lean_rs_sys::closure::lean_apply_m as *const (), "lean_apply_m"),
        // IO
        (
            lean_rs_sys::io::lean_io_mark_end_initialization as *const (),
            "lean_io_mark_end_initialization",
        ),
        // external
        (
            lean_rs_sys::external::lean_register_external_class as *const (),
            "lean_register_external_class",
        ),
    ];

    // Every address must be non-null (failing to link manifests as a build
    // error, but null after relocation is also a regression worth catching).
    for (addr, name) in addresses {
        assert!(!addr.is_null(), "{name} resolved to a null address");
    }

    // The hand-maintained list and the probe list above must stay in sync;
    // catching drift here is cheaper than chasing it through the doc tools.
    assert_eq!(
        addresses.len(),
        REQUIRED_SYMBOLS.len(),
        "tests/linkage.rs probes {} symbols but REQUIRED_SYMBOLS lists {}; \
         keep them in lockstep",
        addresses.len(),
        REQUIRED_SYMBOLS.len(),
    );
}