1 | // Lean compiler output |
2 | // Module: Lake.Version |
3 | // Imports: Init |
4 | #include <lean/lean.h> |
5 | #if defined(__clang__) |
6 | #pragma clang diagnostic ignored "-Wunused-parameter" |
7 | #pragma clang diagnostic ignored "-Wunused-label" |
8 | #elif defined(__GNUC__) && !defined(__CLANG__) |
9 | #pragma GCC diagnostic ignored "-Wunused-parameter" |
10 | #pragma GCC diagnostic ignored "-Wunused-label" |
11 | #pragma GCC diagnostic ignored "-Wunused-but-set-variable" |
12 | #endif |
13 | #ifdef __cplusplus |
14 | extern "C" { |
15 | #endif |
16 | static lean_object* l_Lake_uiVersionString___closed__4; |
17 | static lean_object* l_Lake_uiVersionString___closed__1; |
18 | LEAN_EXPORT lean_object* l_Lake_versionStringCore; |
19 | static lean_object* l_Lake_uiVersionString___closed__7; |
20 | static lean_object* l_Lake_versionString___closed__4; |
21 | static uint8_t l_Lake_version_isRelease___closed__1; |
22 | static lean_object* l_Lake_versionStringCore___closed__8; |
23 | static lean_object* l_Lake_uiVersionString___closed__3; |
24 | static lean_object* l_Lake_versionStringCore___closed__7; |
25 | LEAN_EXPORT lean_object* l_Lake_version_specialDesc; |
26 | LEAN_EXPORT lean_object* l_Lake_versionString; |
27 | uint8_t lean_string_dec_eq(lean_object*, lean_object*); |
28 | static lean_object* l_Lake_version_specialDesc___closed__3; |
29 | static lean_object* l_Lake_versionStringCore___closed__9; |
30 | static lean_object* l_Lake_versionStringCore___closed__5; |
31 | static lean_object* l_Lake_versionStringCore___closed__10; |
32 | static lean_object* l_Lake_versionStringCore___closed__1; |
33 | static lean_object* l_Lake_versionStringCore___closed__6; |
34 | static lean_object* l_Lake_uiVersionString___closed__5; |
35 | uint8_t l_instDecidableNot___rarg(uint8_t); |
36 | static uint8_t l_Lake_versionString___closed__1; |
37 | static lean_object* l_Lake_version_specialDesc___closed__1; |
38 | static lean_object* l_Lake_version_specialDesc___closed__2; |
39 | extern lean_object* l_Lean_versionString; |
40 | static lean_object* l_Lake_versionStringCore___closed__4; |
41 | static lean_object* l_Lake_versionStringCore___closed__3; |
42 | static lean_object* l_Lake_versionString___closed__6; |
43 | LEAN_EXPORT lean_object* l_Lake_version_patch; |
44 | static lean_object* l_Lake_versionString___closed__7; |
45 | static lean_object* l_Lake_versionString___closed__8; |
46 | LEAN_EXPORT lean_object* l_Lake_version_minor; |
47 | LEAN_EXPORT uint8_t l_Lake_version_isRelease; |
48 | static lean_object* l_Lake_versionStringCore___closed__2; |
49 | static lean_object* l_Lake_versionString___closed__3; |
50 | static lean_object* l_Lake_uiVersionString___closed__2; |
51 | LEAN_EXPORT uint8_t l_Lake_version_isPrerelease; |
52 | LEAN_EXPORT lean_object* l_Lake_version_major; |
53 | static uint8_t l_Lake_versionString___closed__2; |
54 | lean_object* lean_string_append(lean_object*, lean_object*); |
55 | static lean_object* l_Lake_versionString___closed__5; |
56 | lean_object* l_Nat_repr(lean_object*); |
57 | LEAN_EXPORT lean_object* l_Lake_uiVersionString; |
58 | static lean_object* l_Lake_uiVersionString___closed__6; |
59 | static lean_object* _init_l_Lake_version_major() { |
60 | _start: |
61 | { |
62 | lean_object* x_1; |
63 | x_1 = lean_unsigned_to_nat(4u); |
64 | return x_1; |
65 | } |
66 | } |
67 | static lean_object* _init_l_Lake_version_minor() { |
68 | _start: |
69 | { |
70 | lean_object* x_1; |
71 | x_1 = lean_unsigned_to_nat(1u); |
72 | return x_1; |
73 | } |
74 | } |
75 | static lean_object* _init_l_Lake_version_patch() { |
76 | _start: |
77 | { |
78 | lean_object* x_1; |
79 | x_1 = lean_unsigned_to_nat(0u); |
80 | return x_1; |
81 | } |
82 | } |
83 | static uint8_t _init_l_Lake_version_isPrerelease() { |
84 | _start: |
85 | { |
86 | uint8_t x_1; |
87 | x_1 = 1; |
88 | return x_1; |
89 | } |
90 | } |
91 | static uint8_t _init_l_Lake_version_isRelease___closed__1() { |
92 | _start: |
93 | { |
94 | uint8_t x_1; |
95 | x_1 = l_Lake_version_isPrerelease; |
96 | if (x_1 == 0) |
97 | { |
98 | uint8_t x_2; |
99 | x_2 = 1; |
100 | return x_2; |
101 | } |
102 | else |
103 | { |
104 | uint8_t x_3; |
105 | x_3 = 0; |
106 | return x_3; |
107 | } |
108 | } |
109 | } |
110 | static uint8_t _init_l_Lake_version_isRelease() { |
111 | _start: |
112 | { |
113 | uint8_t x_1; |
114 | x_1 = l_Lake_version_isRelease___closed__1; |
115 | return x_1; |
116 | } |
117 | } |
118 | static lean_object* _init_l_Lake_version_specialDesc___closed__1() { |
119 | _start: |
120 | { |
121 | lean_object* x_1; |
122 | x_1 = lean_mk_string_from_bytes("" , 0); |
123 | return x_1; |
124 | } |
125 | } |
126 | static lean_object* _init_l_Lake_version_specialDesc___closed__2() { |
127 | _start: |
128 | { |
129 | lean_object* x_1; |
130 | x_1 = lean_mk_string_from_bytes("pre" , 3); |
131 | return x_1; |
132 | } |
133 | } |
134 | static lean_object* _init_l_Lake_version_specialDesc___closed__3() { |
135 | _start: |
136 | { |
137 | uint8_t x_1; |
138 | x_1 = l_Lake_version_isPrerelease; |
139 | if (x_1 == 0) |
140 | { |
141 | lean_object* x_2; |
142 | x_2 = l_Lake_version_specialDesc___closed__1; |
143 | return x_2; |
144 | } |
145 | else |
146 | { |
147 | lean_object* x_3; |
148 | x_3 = l_Lake_version_specialDesc___closed__2; |
149 | return x_3; |
150 | } |
151 | } |
152 | } |
153 | static lean_object* _init_l_Lake_version_specialDesc() { |
154 | _start: |
155 | { |
156 | lean_object* x_1; |
157 | x_1 = l_Lake_version_specialDesc___closed__3; |
158 | return x_1; |
159 | } |
160 | } |
161 | static lean_object* _init_l_Lake_versionStringCore___closed__1() { |
162 | _start: |
163 | { |
164 | lean_object* x_1; lean_object* x_2; |
165 | x_1 = l_Lake_version_major; |
166 | x_2 = l_Nat_repr(x_1); |
167 | return x_2; |
168 | } |
169 | } |
170 | static lean_object* _init_l_Lake_versionStringCore___closed__2() { |
171 | _start: |
172 | { |
173 | lean_object* x_1; lean_object* x_2; lean_object* x_3; |
174 | x_1 = l_Lake_version_specialDesc___closed__1; |
175 | x_2 = l_Lake_versionStringCore___closed__1; |
176 | x_3 = lean_string_append(x_1, x_2); |
177 | return x_3; |
178 | } |
179 | } |
180 | static lean_object* _init_l_Lake_versionStringCore___closed__3() { |
181 | _start: |
182 | { |
183 | lean_object* x_1; |
184 | x_1 = lean_mk_string_from_bytes("." , 1); |
185 | return x_1; |
186 | } |
187 | } |
188 | static lean_object* _init_l_Lake_versionStringCore___closed__4() { |
189 | _start: |
190 | { |
191 | lean_object* x_1; lean_object* x_2; lean_object* x_3; |
192 | x_1 = l_Lake_versionStringCore___closed__2; |
193 | x_2 = l_Lake_versionStringCore___closed__3; |
194 | x_3 = lean_string_append(x_1, x_2); |
195 | return x_3; |
196 | } |
197 | } |
198 | static lean_object* _init_l_Lake_versionStringCore___closed__5() { |
199 | _start: |
200 | { |
201 | lean_object* x_1; lean_object* x_2; |
202 | x_1 = l_Lake_version_minor; |
203 | x_2 = l_Nat_repr(x_1); |
204 | return x_2; |
205 | } |
206 | } |
207 | static lean_object* _init_l_Lake_versionStringCore___closed__6() { |
208 | _start: |
209 | { |
210 | lean_object* x_1; lean_object* x_2; lean_object* x_3; |
211 | x_1 = l_Lake_versionStringCore___closed__4; |
212 | x_2 = l_Lake_versionStringCore___closed__5; |
213 | x_3 = lean_string_append(x_1, x_2); |
214 | return x_3; |
215 | } |
216 | } |
217 | static lean_object* _init_l_Lake_versionStringCore___closed__7() { |
218 | _start: |
219 | { |
220 | lean_object* x_1; lean_object* x_2; lean_object* x_3; |
221 | x_1 = l_Lake_versionStringCore___closed__6; |
222 | x_2 = l_Lake_versionStringCore___closed__3; |
223 | x_3 = lean_string_append(x_1, x_2); |
224 | return x_3; |
225 | } |
226 | } |
227 | static lean_object* _init_l_Lake_versionStringCore___closed__8() { |
228 | _start: |
229 | { |
230 | lean_object* x_1; lean_object* x_2; |
231 | x_1 = l_Lake_version_patch; |
232 | x_2 = l_Nat_repr(x_1); |
233 | return x_2; |
234 | } |
235 | } |
236 | static lean_object* _init_l_Lake_versionStringCore___closed__9() { |
237 | _start: |
238 | { |
239 | lean_object* x_1; lean_object* x_2; lean_object* x_3; |
240 | x_1 = l_Lake_versionStringCore___closed__7; |
241 | x_2 = l_Lake_versionStringCore___closed__8; |
242 | x_3 = lean_string_append(x_1, x_2); |
243 | return x_3; |
244 | } |
245 | } |
246 | static lean_object* _init_l_Lake_versionStringCore___closed__10() { |
247 | _start: |
248 | { |
249 | lean_object* x_1; lean_object* x_2; lean_object* x_3; |
250 | x_1 = l_Lake_versionStringCore___closed__9; |
251 | x_2 = l_Lake_version_specialDesc___closed__1; |
252 | x_3 = lean_string_append(x_1, x_2); |
253 | return x_3; |
254 | } |
255 | } |
256 | static lean_object* _init_l_Lake_versionStringCore() { |
257 | _start: |
258 | { |
259 | lean_object* x_1; |
260 | x_1 = l_Lake_versionStringCore___closed__10; |
261 | return x_1; |
262 | } |
263 | } |
264 | static uint8_t _init_l_Lake_versionString___closed__1() { |
265 | _start: |
266 | { |
267 | lean_object* x_1; lean_object* x_2; uint8_t x_3; |
268 | x_1 = l_Lake_version_specialDesc; |
269 | x_2 = l_Lake_version_specialDesc___closed__1; |
270 | x_3 = lean_string_dec_eq(x_1, x_2); |
271 | return x_3; |
272 | } |
273 | } |
274 | static uint8_t _init_l_Lake_versionString___closed__2() { |
275 | _start: |
276 | { |
277 | uint8_t x_1; uint8_t x_2; |
278 | x_1 = l_Lake_versionString___closed__1; |
279 | x_2 = l_instDecidableNot___rarg(x_1); |
280 | return x_2; |
281 | } |
282 | } |
283 | static lean_object* _init_l_Lake_versionString___closed__3() { |
284 | _start: |
285 | { |
286 | lean_object* x_1; lean_object* x_2; lean_object* x_3; |
287 | x_1 = l_Lake_version_specialDesc___closed__1; |
288 | x_2 = l_Lake_versionStringCore; |
289 | x_3 = lean_string_append(x_1, x_2); |
290 | return x_3; |
291 | } |
292 | } |
293 | static lean_object* _init_l_Lake_versionString___closed__4() { |
294 | _start: |
295 | { |
296 | lean_object* x_1; |
297 | x_1 = lean_mk_string_from_bytes("-" , 1); |
298 | return x_1; |
299 | } |
300 | } |
301 | static lean_object* _init_l_Lake_versionString___closed__5() { |
302 | _start: |
303 | { |
304 | lean_object* x_1; lean_object* x_2; lean_object* x_3; |
305 | x_1 = l_Lake_versionString___closed__3; |
306 | x_2 = l_Lake_versionString___closed__4; |
307 | x_3 = lean_string_append(x_1, x_2); |
308 | return x_3; |
309 | } |
310 | } |
311 | static lean_object* _init_l_Lake_versionString___closed__6() { |
312 | _start: |
313 | { |
314 | lean_object* x_1; lean_object* x_2; lean_object* x_3; |
315 | x_1 = l_Lake_versionString___closed__5; |
316 | x_2 = l_Lake_version_specialDesc; |
317 | x_3 = lean_string_append(x_1, x_2); |
318 | return x_3; |
319 | } |
320 | } |
321 | static lean_object* _init_l_Lake_versionString___closed__7() { |
322 | _start: |
323 | { |
324 | lean_object* x_1; lean_object* x_2; lean_object* x_3; |
325 | x_1 = l_Lake_versionString___closed__6; |
326 | x_2 = l_Lake_version_specialDesc___closed__1; |
327 | x_3 = lean_string_append(x_1, x_2); |
328 | return x_3; |
329 | } |
330 | } |
331 | static lean_object* _init_l_Lake_versionString___closed__8() { |
332 | _start: |
333 | { |
334 | uint8_t x_1; |
335 | x_1 = l_Lake_versionString___closed__2; |
336 | if (x_1 == 0) |
337 | { |
338 | lean_object* x_2; |
339 | x_2 = l_Lake_versionStringCore; |
340 | return x_2; |
341 | } |
342 | else |
343 | { |
344 | lean_object* x_3; |
345 | x_3 = l_Lake_versionString___closed__7; |
346 | return x_3; |
347 | } |
348 | } |
349 | } |
350 | static lean_object* _init_l_Lake_versionString() { |
351 | _start: |
352 | { |
353 | lean_object* x_1; |
354 | x_1 = l_Lake_versionString___closed__8; |
355 | return x_1; |
356 | } |
357 | } |
358 | static lean_object* _init_l_Lake_uiVersionString___closed__1() { |
359 | _start: |
360 | { |
361 | lean_object* x_1; |
362 | x_1 = lean_mk_string_from_bytes("Lake version " , 13); |
363 | return x_1; |
364 | } |
365 | } |
366 | static lean_object* _init_l_Lake_uiVersionString___closed__2() { |
367 | _start: |
368 | { |
369 | lean_object* x_1; lean_object* x_2; lean_object* x_3; |
370 | x_1 = l_Lake_uiVersionString___closed__1; |
371 | x_2 = l_Lake_versionString; |
372 | x_3 = lean_string_append(x_1, x_2); |
373 | return x_3; |
374 | } |
375 | } |
376 | static lean_object* _init_l_Lake_uiVersionString___closed__3() { |
377 | _start: |
378 | { |
379 | lean_object* x_1; |
380 | x_1 = lean_mk_string_from_bytes(" (Lean version " , 15); |
381 | return x_1; |
382 | } |
383 | } |
384 | static lean_object* _init_l_Lake_uiVersionString___closed__4() { |
385 | _start: |
386 | { |
387 | lean_object* x_1; lean_object* x_2; lean_object* x_3; |
388 | x_1 = l_Lake_uiVersionString___closed__2; |
389 | x_2 = l_Lake_uiVersionString___closed__3; |
390 | x_3 = lean_string_append(x_1, x_2); |
391 | return x_3; |
392 | } |
393 | } |
394 | static lean_object* _init_l_Lake_uiVersionString___closed__5() { |
395 | _start: |
396 | { |
397 | lean_object* x_1; lean_object* x_2; lean_object* x_3; |
398 | x_1 = l_Lake_uiVersionString___closed__4; |
399 | x_2 = l_Lean_versionString; |
400 | x_3 = lean_string_append(x_1, x_2); |
401 | return x_3; |
402 | } |
403 | } |
404 | static lean_object* _init_l_Lake_uiVersionString___closed__6() { |
405 | _start: |
406 | { |
407 | lean_object* x_1; |
408 | x_1 = lean_mk_string_from_bytes(")" , 1); |
409 | return x_1; |
410 | } |
411 | } |
412 | static lean_object* _init_l_Lake_uiVersionString___closed__7() { |
413 | _start: |
414 | { |
415 | lean_object* x_1; lean_object* x_2; lean_object* x_3; |
416 | x_1 = l_Lake_uiVersionString___closed__5; |
417 | x_2 = l_Lake_uiVersionString___closed__6; |
418 | x_3 = lean_string_append(x_1, x_2); |
419 | return x_3; |
420 | } |
421 | } |
422 | static lean_object* _init_l_Lake_uiVersionString() { |
423 | _start: |
424 | { |
425 | lean_object* x_1; |
426 | x_1 = l_Lake_uiVersionString___closed__7; |
427 | return x_1; |
428 | } |
429 | } |
430 | lean_object* initialize_Init(uint8_t builtin, lean_object*); |
431 | static bool _G_initialized = false; |
432 | LEAN_EXPORT lean_object* initialize_Lake_Version(uint8_t builtin, lean_object* w) { |
433 | lean_object * res; |
434 | if (_G_initialized) return lean_io_result_mk_ok(lean_box(0)); |
435 | _G_initialized = true; |
436 | res = initialize_Init(builtin, lean_io_mk_world()); |
437 | if (lean_io_result_is_error(res)) return res; |
438 | lean_dec_ref(res); |
439 | l_Lake_version_major = _init_l_Lake_version_major(); |
440 | lean_mark_persistent(l_Lake_version_major); |
441 | l_Lake_version_minor = _init_l_Lake_version_minor(); |
442 | lean_mark_persistent(l_Lake_version_minor); |
443 | l_Lake_version_patch = _init_l_Lake_version_patch(); |
444 | lean_mark_persistent(l_Lake_version_patch); |
445 | l_Lake_version_isPrerelease = _init_l_Lake_version_isPrerelease(); |
446 | l_Lake_version_isRelease___closed__1 = _init_l_Lake_version_isRelease___closed__1(); |
447 | l_Lake_version_isRelease = _init_l_Lake_version_isRelease(); |
448 | l_Lake_version_specialDesc___closed__1 = _init_l_Lake_version_specialDesc___closed__1(); |
449 | lean_mark_persistent(l_Lake_version_specialDesc___closed__1); |
450 | l_Lake_version_specialDesc___closed__2 = _init_l_Lake_version_specialDesc___closed__2(); |
451 | lean_mark_persistent(l_Lake_version_specialDesc___closed__2); |
452 | l_Lake_version_specialDesc___closed__3 = _init_l_Lake_version_specialDesc___closed__3(); |
453 | lean_mark_persistent(l_Lake_version_specialDesc___closed__3); |
454 | l_Lake_version_specialDesc = _init_l_Lake_version_specialDesc(); |
455 | lean_mark_persistent(l_Lake_version_specialDesc); |
456 | l_Lake_versionStringCore___closed__1 = _init_l_Lake_versionStringCore___closed__1(); |
457 | lean_mark_persistent(l_Lake_versionStringCore___closed__1); |
458 | l_Lake_versionStringCore___closed__2 = _init_l_Lake_versionStringCore___closed__2(); |
459 | lean_mark_persistent(l_Lake_versionStringCore___closed__2); |
460 | l_Lake_versionStringCore___closed__3 = _init_l_Lake_versionStringCore___closed__3(); |
461 | lean_mark_persistent(l_Lake_versionStringCore___closed__3); |
462 | l_Lake_versionStringCore___closed__4 = _init_l_Lake_versionStringCore___closed__4(); |
463 | lean_mark_persistent(l_Lake_versionStringCore___closed__4); |
464 | l_Lake_versionStringCore___closed__5 = _init_l_Lake_versionStringCore___closed__5(); |
465 | lean_mark_persistent(l_Lake_versionStringCore___closed__5); |
466 | l_Lake_versionStringCore___closed__6 = _init_l_Lake_versionStringCore___closed__6(); |
467 | lean_mark_persistent(l_Lake_versionStringCore___closed__6); |
468 | l_Lake_versionStringCore___closed__7 = _init_l_Lake_versionStringCore___closed__7(); |
469 | lean_mark_persistent(l_Lake_versionStringCore___closed__7); |
470 | l_Lake_versionStringCore___closed__8 = _init_l_Lake_versionStringCore___closed__8(); |
471 | lean_mark_persistent(l_Lake_versionStringCore___closed__8); |
472 | l_Lake_versionStringCore___closed__9 = _init_l_Lake_versionStringCore___closed__9(); |
473 | lean_mark_persistent(l_Lake_versionStringCore___closed__9); |
474 | l_Lake_versionStringCore___closed__10 = _init_l_Lake_versionStringCore___closed__10(); |
475 | lean_mark_persistent(l_Lake_versionStringCore___closed__10); |
476 | l_Lake_versionStringCore = _init_l_Lake_versionStringCore(); |
477 | lean_mark_persistent(l_Lake_versionStringCore); |
478 | l_Lake_versionString___closed__1 = _init_l_Lake_versionString___closed__1(); |
479 | l_Lake_versionString___closed__2 = _init_l_Lake_versionString___closed__2(); |
480 | l_Lake_versionString___closed__3 = _init_l_Lake_versionString___closed__3(); |
481 | lean_mark_persistent(l_Lake_versionString___closed__3); |
482 | l_Lake_versionString___closed__4 = _init_l_Lake_versionString___closed__4(); |
483 | lean_mark_persistent(l_Lake_versionString___closed__4); |
484 | l_Lake_versionString___closed__5 = _init_l_Lake_versionString___closed__5(); |
485 | lean_mark_persistent(l_Lake_versionString___closed__5); |
486 | l_Lake_versionString___closed__6 = _init_l_Lake_versionString___closed__6(); |
487 | lean_mark_persistent(l_Lake_versionString___closed__6); |
488 | l_Lake_versionString___closed__7 = _init_l_Lake_versionString___closed__7(); |
489 | lean_mark_persistent(l_Lake_versionString___closed__7); |
490 | l_Lake_versionString___closed__8 = _init_l_Lake_versionString___closed__8(); |
491 | lean_mark_persistent(l_Lake_versionString___closed__8); |
492 | l_Lake_versionString = _init_l_Lake_versionString(); |
493 | lean_mark_persistent(l_Lake_versionString); |
494 | l_Lake_uiVersionString___closed__1 = _init_l_Lake_uiVersionString___closed__1(); |
495 | lean_mark_persistent(l_Lake_uiVersionString___closed__1); |
496 | l_Lake_uiVersionString___closed__2 = _init_l_Lake_uiVersionString___closed__2(); |
497 | lean_mark_persistent(l_Lake_uiVersionString___closed__2); |
498 | l_Lake_uiVersionString___closed__3 = _init_l_Lake_uiVersionString___closed__3(); |
499 | lean_mark_persistent(l_Lake_uiVersionString___closed__3); |
500 | l_Lake_uiVersionString___closed__4 = _init_l_Lake_uiVersionString___closed__4(); |
501 | lean_mark_persistent(l_Lake_uiVersionString___closed__4); |
502 | l_Lake_uiVersionString___closed__5 = _init_l_Lake_uiVersionString___closed__5(); |
503 | lean_mark_persistent(l_Lake_uiVersionString___closed__5); |
504 | l_Lake_uiVersionString___closed__6 = _init_l_Lake_uiVersionString___closed__6(); |
505 | lean_mark_persistent(l_Lake_uiVersionString___closed__6); |
506 | l_Lake_uiVersionString___closed__7 = _init_l_Lake_uiVersionString___closed__7(); |
507 | lean_mark_persistent(l_Lake_uiVersionString___closed__7); |
508 | l_Lake_uiVersionString = _init_l_Lake_uiVersionString(); |
509 | lean_mark_persistent(l_Lake_uiVersionString); |
510 | return lean_io_result_mk_ok(lean_box(0)); |
511 | } |
512 | #ifdef __cplusplus |
513 | } |
514 | #endif |
515 | |