coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Coq and Unicode, Benjamin C. Pierce, 07/31/2019
- Re: [Coq-Club] Coq and Unicode, Théo Zimmermann, 07/31/2019
Archive powered by MHonArc 2.6.18.