Constant REPL_RANDOM_INFOLEVEL 

pub const REPL_RANDOM_INFOLEVEL: u32 = 1003u32;