The Coq mailing list

["Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>]

Thanks, Théo!  It sounds like SF should wait for Coq 8.10 and then try a 
serious experiment with unicode…

    - Benjamin

> On Jul 31, 2019, at 5:04 PM, Théo Zimmermann 
> <theo.zimmi AT gmail.com>
>  wrote:
> 
> Hi Benjamin,
> 
> The situation has become better in CoqIDE "out of the box" in version
> 8.10 thanks to the effort by Arthur Charguéraud. See the documentation
> here: 
> https://coq.github.io/doc/V8.10+beta2/refman/practical-tools/coqide.html#coqide-unicode
> 
> As for Emacs, Company Coq has supported Unicode input for a long time
> now: 
> https://github.com/cpitclaudel/company-coq/blob/master/img/math-completion.png
> 
> I am not a vim user myself, but I want to highlight that vim has a
> very actively developed / maintained support package called "Coqtail".
> It deserves some praise. And I have no idea if it includes any Unicode
> input support (or if vim includes some by default).
> 
> Finally, Maxime is working on reviving the vscode support that had
> been started by CJ Bell: https://github.com/coq-community/vscoq. The
> new version is compatible with Coq 8.9+ but has not yet been published
> on the vscode store, if I'm not mistaken. When it is ready, it should
> be (again) a major player in the Coq editor support landscape, given
> the popularity of vscode, especially among younger students. I also
> don't know if it has a Unicode input method. I wouldn't be surprised,
> though, to hear that there is another extension with such support.
> 
> And by the way, we should not forget about new ways of interacting
> with Coq in the browser: jscoq (https://x80.org/rhino-coq/), and the
> Jupyter kernel (https://github.com/EugeneLoy/coq_jupyter).
> 
> Cheers,
> Théo
> 
> Le mer. 31 juil. 2019 à 21:01, Benjamin C. Pierce
> <bcpierce AT cis.upenn.edu>
>  a écrit :
>> 
>> At the moment, the books in the Software Foundations series deal with 
>> mathematical notations using a somewhat clunky collection of ascii symbols 
>> and latex-like ascii notations (for the .v files we distribute) and 
>> typesetting hacks (for the generated html files).
>> 
>> Every couple of years, I start wondering whether there is a better way — 
>> e.g., whether we could just convert everything to Unicode.  But we always 
>> end up not doing it because Unicode doesn’t seem to work reliably "out of 
>> the box" on some platform that people care about (CoqIDE on unix, CoqIDE 
>> on Windows, emacs with or without PG / Company Coq, …).
>> 
>> Has the situation gotten any better recently, or is that still where we 
>> are?
>> 
>> Thanks for any insights!
>> 
>>    - B
>> 
>