Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Coq and Unicode

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Coq and Unicode


Chronological Thread 
  • From: "Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Coq and Unicode
  • Date: Wed, 31 Jul 2019 15:01:28 -0400
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=bcpierce AT cis.upenn.edu; spf=Pass smtp.mailfrom=bcpierce AT cis.upenn.edu; spf=None smtp.helo=postmaster AT mx0b-000c2a01.pphosted.com
  • Ironport-phdr: 9a23:QOqBVBJcSh72L3US+NmcpTZWNBhigK39O0sv0rFitYgRLfvxwZ3uMQTl6Ol3ixeRBMOHsqgC2red6vqwEUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCejbb9oKBi7rQrdutQIjYZhN6081gbHrnxUdupM2GhmP0iTnxHy5sex+J5s7SFdsO8/+sBDTKv3Yb02QaRXAzo6PW814tbrtQTYQguU+nQcSGQWnQFWDAXD8Rr3Q43+sir+tup6xSmaIcj7Rq06VDi+86tmTgLjhSEaPDA77W7XkNR9gqJHrxyuqBNxzZPaboKLOvR5Za7dYcoaRW9dUsZRSyBMAIWxZJYPAeobOuZYqpHwq1UToBSgAwmsBvngyjpJhn/wwKY3zf4tGhzc0gwhAd0Oqmjbo8v7OKwPVu2617XHzS3Cb/xIwzfy9JbHfws9rvGNRrJ8a9fRyVExGAPDiFWcs5LqMC6I1ukUtWWQ8uluVfq3hmI6pAx8oSKjytoth4THnI4Z11DJ+CVjzIs7JNC0UFN3bN6nHZdKqi2XOZd6TtkiTmxmoio21LkLtJimdyYQ0psn3QTQa/mffoiI/B3jUOGRLC99hHNqZL6wnA++/VS8xuHgSsa4zkxFojZYntXWrnANzxzT6s+cSvth4EiuxCyD2BzU6uFBOUw0lKzbJIA9wrMoi5YevkfOEjXrlEj3gqKabFgo9+io5uj9bLjrp4eQN4puhQH/NqQulNa/AeM9MgUWRGeU5fy81Lz98k3jXLpFkOY7nbXYsJDBP8gbu7a5DBFT0oYl8RqwESqp0MkAkXkdMF1FYA6Hj5TuO1zWPP/4Cu6/j02wnzdv2vDJJabsAo7NL3jGiLfuZ6xx609ayAopzNBQ/YhYCr8bIKG7Zkikv9vBSxQ9LgacwuD9Cdw72JlNd3iIB/rTGq7Us1aN5+RnCK/EXI4Yoj3wYbBx7fX2jHIjklI1dqiym4YPZXa+WPlqPhPKMjLXnt4dHDJS7UIFR+vwhQjaCGMBVzOJR6s5owoDJsemAIPEHND/hazZ1mLjRsVdPGkeUxaUCXfvbJmJV7EHbyfAepYwwAxBbqCoTsoa7T/rsQb7z7R9Ke+Np38TtImlycB44euVmB0vp2UtU5atllqVRmQxpVsmAics1fki80d80RGeyaV+hbpVGcEBv/4=

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




Archive powered by MHonArc 2.6.18.

Top of Page