pub unsafe extern "C" fn lean_initialize_runtime_module()