The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

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
>