The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

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> 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