1// Lean compiler output
2// Module: Lake.Main
3// Imports: Init Lake Lake.CLI
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
14extern "C" {
15#endif
16LEAN_EXPORT lean_object* _lean_main(lean_object*, lean_object*);
17lean_object* l_Lake_CliM_run___rarg(lean_object*, lean_object*, lean_object*);
18static lean_object* l_main___closed__1;
19lean_object* l_Lake_lake(lean_object*, lean_object*, lean_object*);
20static lean_object* _init_l_main___closed__1() {
21_start:
22{
23lean_object* x_1;
24x_1 = lean_alloc_closure((void*)(l_Lake_lake), 3, 0);
25return x_1;
26}
27}
28LEAN_EXPORT lean_object* _lean_main(lean_object* x_1, lean_object* x_2) {
29_start:
30{
31lean_object* x_3; lean_object* x_4; uint8_t x_5;
32x_3 = l_main___closed__1;
33x_4 = l_Lake_CliM_run___rarg(x_3, x_1, x_2);
34x_5 = !lean_is_exclusive(x_4);
35if (x_5 == 0)
36{
37return x_4;
38}
39else
40{
41lean_object* x_6; lean_object* x_7; lean_object* x_8;
42x_6 = lean_ctor_get(x_4, 0);
43x_7 = lean_ctor_get(x_4, 1);
44lean_inc(x_7);
45lean_inc(x_6);
46lean_dec(x_4);
47x_8 = lean_alloc_ctor(0, 2, 0);
48lean_ctor_set(x_8, 0, x_6);
49lean_ctor_set(x_8, 1, x_7);
50return x_8;
51}
52}
53}
54lean_object* initialize_Init(uint8_t builtin, lean_object*);
55lean_object* initialize_Lake(uint8_t builtin, lean_object*);
56lean_object* initialize_Lake_CLI(uint8_t builtin, lean_object*);
57static bool _G_initialized = false;
58LEAN_EXPORT lean_object* initialize_Lake_Main(uint8_t builtin, lean_object* w) {
59lean_object * res;
60if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
61_G_initialized = true;
62res = initialize_Init(builtin, lean_io_mk_world());
63if (lean_io_result_is_error(res)) return res;
64lean_dec_ref(res);
65res = initialize_Lake(builtin, lean_io_mk_world());
66if (lean_io_result_is_error(res)) return res;
67lean_dec_ref(res);
68res = initialize_Lake_CLI(builtin, lean_io_mk_world());
69if (lean_io_result_is_error(res)) return res;
70lean_dec_ref(res);
71l_main___closed__1 = _init_l_main___closed__1();
72lean_mark_persistent(l_main___closed__1);
73return lean_io_result_mk_ok(lean_box(0));
74}
75void lean_initialize();
76
77 #if defined(WIN32) || defined(_WIN32)
78 #include <windows.h>
79 #endif
80
81 int main(int argc, char ** argv) {
82 #if defined(WIN32) || defined(_WIN32)
83 SetErrorMode(SEM_FAILCRITICALERRORS);
84 #endif
85 lean_object* in; lean_object* res;
86lean_initialize();
87lean_set_panic_messages(false);
88res = initialize_Lake_Main(1 /* builtin */, lean_io_mk_world());
89lean_set_panic_messages(true);
90lean_io_mark_end_initialization();
91if (lean_io_result_is_ok(res)) {
92lean_dec_ref(res);
93lean_init_task_manager();
94in = lean_box(0);
95int i = argc;
96while (i > 1) {
97 lean_object* n;
98 i--;
99 n = lean_alloc_ctor(1,2,0); lean_ctor_set(n, 0, lean_mk_string(argv[i])); lean_ctor_set(n, 1, in);
100 in = n;
101}
102res = _lean_main(in, lean_io_mk_world());
103}
104lean_finalize_task_manager();
105if (lean_io_result_is_ok(res)) {
106 int ret = lean_unbox_uint32(lean_io_result_get_value(res));
107 lean_dec_ref(res);
108 return ret;
109} else {
110 lean_io_result_show_error(res);
111 lean_dec_ref(res);
112 return 1;
113}
114}
115#ifdef __cplusplus
116}
117#endif
118