lean4/src/runtime/init_module.cpp at 28a6d080ed33636257051f7a03b0c10ae7a1b62f · leanprover/lean4 · GitHub

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
/*
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author: Leonardo de Moura
*/
#include "runtime/alloc.h"
#include "runtime/debug.h"
#include "runtime/thread.h"
#include "runtime/object.h"
#include "runtime/io.h"
#include "runtime/stack_overflow.h"
#include "runtime/process.h"
#include "runtime/mutex.h"
#include "runtime/init_module.h"
#include "runtime/libuv.h"
#include "runtime/openssl.h"
#include "runtime/openssl/context.h"
#include "runtime/openssl/session.h"

namespace lean {
// idempotent as it may be called both by the generated `main` and, via `lean_initialize`,
// by generated module initializers
static bool g_initialized = false;
extern "C" LEAN_EXPORT void lean_initialize_runtime_module() {
    if (g_initialized)
        return;
    g_initialized = true;
    initialize_alloc();
    initialize_debug();
    initialize_object();
    initialize_io();
    initialize_thread();
    initialize_mutex();
    initialize_process();
    initialize_stack_overflow();
    initialize_openssl();
    initialize_openssl_context();
    initialize_openssl_session();
    initialize_libuv();
}
void initialize_runtime_module() {
    lean_initialize_runtime_module();
}
void finalize_runtime_module() {
    finalize_stack_overflow();
    finalize_openssl();
    finalize_process();
    finalize_mutex();
    finalize_thread();
    finalize_io();
    finalize_object();
    finalize_debug();
    finalize_alloc();
}
}