coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Lean Theorem Prover

From: Daniel Schepler <dschepler AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Lean Theorem Prover
Date: Fri, 26 Feb 2016 14:58:08 -0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=dschepler AT gmail.com; spf=Pass smtp.mailfrom=dschepler AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f54.google.com
Ironport-phdr: 9a23:MrbzyRLex+PCwjpPnNmcpTZWNBhigK39O0sv0rFitYgULf3xwZ3uMQTl6Ol3ixeRBMOAu60C1bad6/CocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWC0ILpi6vqq9X6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD89pozcNLUL37cqIkVvQYSW1+ayFmrPHs4DLEVEOk4mYWGjEdlQMNCAzY5jn7WI3wu230rLwu9jOdOJjaRLY1VDDq1KxrRQfshT1PYzIi+2Haksh9lopUpRugo1p0xIuCM9LdD+Z3Yq6IJYBSfmFGRMsEEnUZWo4=

On Fri, Feb 26, 2016 at 6:34 AM, Benjamin C. Pierce
<bcpierce AT cis.upenn.edu>
wrote:
> (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.

As just one data point - on Debian GNU/Linux, the GTK-based CoqIDE
just works with unicode. As for inputting unicode characters, it took
a bit more effort - but the instructions at
https://coq.inria.fr/cocorico/TeXInputMethodForUnicodeNotations under
"In CoqIDE (using UIM on POSIX systems)" were all I needed to get that
working.
--
Daniel

RE: [Coq-Club] Lean Theorem Prover, (continued)