The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

Hi Benjamin and Michael,

I like the idea of moving to Unicode symbols, and I think it's quite 
feasible. There are a few issues, though; not so much with encoding, but with 
font support:

* There is currently no free monospace font with good Unicode coverage. If 
pixel-perfect indentation is a concern (and I see most people using Coq with 
a fixed-width font), then Unicode will cause some grief. I've done some work 
on this (https://github.com/cpitclaudel/monospacifier), but it isn't perfect.

* On Debian derivatives, the only commonly installed fonts that include a 
wide range of symbols are TeX fonts, and there's a bug in their metrics which 
causes Emacs and other metrics-respecting applications to display them with 
huge line gaps (see https://github.com/cpitclaudel/company-coq/issues/15, 
https://github.com/cpitclaudel/company-coq/issues/31, and 
https://emacs.stackexchange.com/questions/251/line-height-with-unicode-characters
 for more info). This was fixed in Emacs 25 
(https://lists.gnu.org/archive/html/bug-gnu-emacs/2015-05/msg00696.html), but 
it's not released yet.

* Many users don't have the right fonts installed, so some symbols will show 
up as � or as a white box.

This is nothing that can't be solved with a bit of setup time, though. And 
Unicode everywhere seems to work for Agda, so it could probably work for us 
too.

Cheers,
Clément.

On 02/26/2016 12:32 PM, Soegtrop, Michael wrote:
> Dear Benjamin,
> 
>> At some point, I’d really like to convert Software Foundations to Unicode, 
>> as this would avoid a lot of hassles with notation, awkward hacks in HTML 
>> generation, etc.
> 
>> But I’ve been nervous about making the switch so far for two reasons:
> 
> a few reasons for switching to Unicode:
> 
> 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
> 
> 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.
> 
>  
> 
> Best regards,
> 
>  
> 
> Michael
> 
>  
> 
> *From:*coq-club-request AT inria.fr
>  
> [mailto:coq-club-request AT inria.fr]
>  *On Behalf Of *Benjamin C. Pierce
> *Sent:* Friday, February 26, 2016 3:34 PM
> *To:* 
> coq-club AT inria.fr
> *Subject:* Re: [Coq-Club] Lean Theorem Prover
> 
>  
> 
> Since we’re talking about unicode, I’d like to get people’s advice…  
> 
>  
> 
> At some point, I’d really like to convert Software Foundations to unicode, 
> as this would avoid a lot of hassles with notation, awkward hacks in HTML 
> generation, etc.  But I’ve been nervous about making the switch so far for 
> two reasons:
> 
>  1. I wonder whether beginning users will find the available input methods 
> confusing or off-putting, and 
>  2. (more significantly) I wonder whether the world has stabilized to the 
> point where the major Coq IDEs will “just work” with unicode in their 
> default configurations on all platforms.
> 
> What do people think?  Should I just take the plunge?  Or is it not time 
> yet?
> 
>  
> 
>     - Benjamin
> 
>  
> 
>  
> 
>     On Feb 26, 2016, at 9:20 AM, Clément Pit--Claudel 
> <clement.pit AT gmail.com
>  
> <mailto:clement.pit AT gmail.com>>
>  wrote:
> 
>      
> 
>     On 02/26/2016 01:23 AM, Arnaud Spiwack wrote:
> 
>         I just mean I like the agda-style input which replaces \forall by 
> the unicode ∀ seamlessly. It's possible that this is supported in coq as 
> well I guess (I'm a little behind the times).
> 
> 
>     That's just built-in in emacs. There are even several ways to do that 
> (the old-school quail, and the newish company-math at least).
> 
> 
>     Indeed; with plain Emacs, just typing `M-x set-input-method RET TeX 
> RET` will give you the Agda-style input that you mentionned.
>     Alternatively (if you use it), company-coq loads company-math, so 
> typing \rightarr will offer \rightarrow, and RET will complete it to →.
> 
>     Should we make this the default input method in PG?
> 
>     Clément.
> 
>  
> 
> Intel Deutschland GmbH
> Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
> Tel: +49 89 99 8853-0, www.intel.de
> Managing Directors: Christin Eisenschmid, Christian Lamprechter
> Chairperson of the Supervisory Board: Nicole Lau
> Registered Office: Munich
> Commercial Register: Amtsgericht Muenchen HRB 186928
>

Attachment: signature.asc
Description: OpenPGP digital signature