The Coq mailing list

[Makarius <makarius AT sketis.net>]

On Fri, 26 Feb 2016, Soegtrop, Michael wrote:

> 1.) Using Unicode notations in the HTML version but ASCII in the IDE is
>     as confusing as finding the shortcuts for the right symbols
>
> 2.) Most people read more than they write, so it makes sense to optimize
>     for readability – and the Unicode symbols are more readable
>
> 3.) The shortcuts for the Unicode symbols can be mentioned in IDE menus
>     at a prominent place

I fully agree that high-end proof assistants should support proper 
mathematical symbols without the user having to think about it. I disagree 
that such a blissful situation can be equated with "Unicode". Unicode is a 
rather big standard with many sub-standards, and it requires years and 
decades to make it really work for a particular task.

About 8 years ago, I set out to make mathematical symbols "just work" for 
the forthcoming Prover IDE of Isabelle -- uniformly on all platforms. It 
required several years to get there, and every year I learned new aspects 
of Unicode that I could not imagine before. In the current release of 
Isabelle2016 (February 2016) this is mostly routine, and we have again 
eliminated a lot of old ASCII replacement syntax. Interestingly, that 
release also parts with official Unicode in various ways, e.g. see "more 
arrow symbols" announced here
http://isabelle.in.tum.de/dist/Isabelle2016/doc/NEWS.html

Hopefully you see there arrows of length 3 and 4, taken from a server-side 
font that is also used in the IDE. Length 1 and 2 are defined by the 
Unicode standard and are in their usual place. Note that in standard 
Unicode fonts, length 2 arrows can already be a problem, and lead to 
disappointing white or black boxes.


> Regarding your portability concerns:
>
> · On Windows non-Unicode is dead. The last non Unicode Version was 
> Windows ME (Millennium Edition) which I don’t think is used any more. 
> Even its successor Windows XP is out of maintenance since a while and XP 
> does support Unicode (always – there are no XP systems which don’t 
> support it). Here is a link to OS usage statistics: 
> https://en.wikipedia.org/wiki/Usage_share_of_operating_systems.
>
> · I did a quick search on google for Unicode issues with 
> Linux/Debian/Ubuntu/Fedora/Mint. The first 20 articles I found where all 
> 2009 or older. So I think issues are solved since then, since google 
> doesn’t tend to prefer old articles.
>
> · I would think Mac with its DTP background was pretty much always 
> Unicode.

All these platforms pretend to support Unicode for some decades, but it is 
still possible to get into problems. It is not something that just works 
by default and can be counted on.

With some care, it is possible to turn Unicode into some use. I recommend 
to read the relevant documentation:
http://isabelle.in.tum.de/dist/Isabelle2016/doc/jedit.pdf
http://isabelle.in.tum.de/dist/Isabelle2016/doc/system.pdf
http://isabelle.in.tum.de/dist/Isabelle2016/doc/isar-ref.pdf
and search for "Isabelle symbols". The phrase "Unicode" is hardly ever 
used, because it is of little relevance.


I have pointed this out to various Coq people more than once, and this is 
just an opportunity to make a broadcast.


        Makarius