The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

On Wed, Mar 8, 2017 at 10:23 AM, Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com> wrote:

I guess that it is not the responsibility of the "grep" and friends to enable you to type unicode characters.
(it is the job of programs providing "input method", I guess, such as "xim", "uim" and many others).

Of course. As somebody who worked on Unicode support for one of Java compilers, I have also seen some other issues. For example, what is the default file encoding of .v files? Is it ASCII of Unicode? If Unicode what is the encoding (UTF-8/UTF-16/etc.). Could BOM be present? Is it mandatory? Is compiler output properly preserves Unicode in error messages? If in XML protocol used by IDE character offsets to source files are used, it should be understood that even in UCS-2 some characters can take more than 2 bytes (see "surrogates"), etc.

--

CMU ECE PhD candidate

Mobile: +1(510)220-1060