Function lean_io_mark_end_initialization 

pub unsafe extern "C" fn lean_io_mark_end_initialization()

Signal that runtime initialization is complete; subsequent allocations should not flag objects as persistent (lean.h:2907).