lean_rs_sys/
init.rs

1//! Runtime initialization and thread attachment.
2//!
3//! These symbols are exported by `libleanshared` but **not declared in
4//! `lean.h`** (they are part of Lean's runtime entry-point surface, not the
5//! object-ABI header). The `LEAN_HEADER_DIGEST` build check therefore does
6//! not gate them; instead they are protected by `REQUIRED_SYMBOLS` plus
7//! `tests/linkage.rs`, which fails to link if any are missing.
8
9use core::ffi::c_char;
10
11unsafe extern "C" {
12    /// Initialize the Lean runtime. Must be called exactly once per process
13    /// before any other Lean-runtime entry point. The C signature in the
14    /// runtime accepts no arguments.
15    pub fn lean_initialize();
16
17    /// Initialize the runtime module (compact regions, persistent objects).
18    /// Must be called after [`lean_initialize`] and before invoking any
19    /// compiled Lean module's `init` entry point.
20    pub fn lean_initialize_runtime_module();
21
22    /// Attach the current OS thread to the Lean runtime so it may invoke
23    /// compiled Lean code. Each thread that calls into Lean must pair this
24    /// with [`lean_finalize_thread`] before exiting.
25    pub fn lean_initialize_thread();
26
27    /// Detach the current OS thread from the Lean runtime.
28    pub fn lean_finalize_thread();
29
30    /// Install the process command-line arguments for `System.Args`. `argv`
31    /// must outlive any Lean code that reads the arguments.
32    pub fn lean_setup_args(argc: i32, argv: *mut *mut c_char);
33
34    /// Start the Lean task manager with a runtime-chosen number of worker
35    /// threads (`lean.h:1272`).
36    pub fn lean_init_task_manager();
37
38    /// Start the Lean task manager with the requested number of worker
39    /// threads (`lean.h:1273`).
40    pub fn lean_init_task_manager_using(num_workers: u32);
41
42    /// Stop the Lean task manager and join all workers (`lean.h:1274`).
43    pub fn lean_finalize_task_manager();
44}
lean_rs_sys/init.rs

lean_rs_sys/
init.rs
