[Python-Dev] optimization required: .format() is much slower than %