Module init 

Runtime initialization and thread attachment.

These symbols are exported by libleanshared but not declared in lean.h (they are part of Lean’s runtime entry-point surface, not the object-ABI header). The LEAN_HEADER_DIGEST build check therefore does not gate them; instead they are protected by REQUIRED_SYMBOLS plus tests/linkage.rs, which fails to link if any are missing.

Functions

lean_finalize_task_manager^⚠

Stop the Lean task manager and join all workers (lean.h:1274).

lean_finalize_thread^⚠

Detach the current OS thread from the Lean runtime.

lean_init_task_manager^⚠

Start the Lean task manager with a runtime-chosen number of worker threads (lean.h:1272).

lean_init_task_manager_using^⚠

Start the Lean task manager with the requested number of worker threads (lean.h:1273).

lean_initialize^⚠

Initialize the Lean runtime. Must be called exactly once per process before any other Lean-runtime entry point. The C signature in the runtime accepts no arguments.

lean_initialize_runtime_module^⚠

Initialize the runtime module (compact regions, persistent objects). Must be called after lean_initialize and before invoking any compiled Lean module’s init entry point.

lean_initialize_thread^⚠

Attach the current OS thread to the Lean runtime so it may invoke compiled Lean code. Each thread that calls into Lean must pair this with lean_finalize_thread before exiting.

lean_setup_args^⚠

Install the process command-line arguments for System.Args. argv must outlive any Lean code that reads the arguments.