def ms2str(v):
    """
    Convert a time in milliseconds to a time string.

    Arguments:
        v: a time in milliseconds.

    Returns:
        A string in the format HH:MM:SS,mmm.
    """
    v, ms = divmod(v, 1000)
    v, s = divmod(v, 60)
    h, m = divmod(v, 60)
    return f"{h:02d}:{m:02d}:{s:02d},{ms:03d}"