Email Gateway (Jan 28 2021 at 03:58): Email Gateway (Jan 28 2021 at 03:58):From: Pedro Sánchez Terraf <sterraf@famaf.unc.edu.ar>
Dear Makarius/All,
I've been using UTF8 chars in my last project on my old Linux laptop.
The session did build without errors under Isabelle2020 but it fails (at
the document preparation stage) in all release candidates (I'm sorry for
the late notice).
The command I'm using to build is
$ ~/bin/Isabelle2021-RC3/bin/isabelle build -v -c -d . UTF8_Test
I'm attaching a minimal session directory (to try) to reproduce the failure:
*** Latex error (line 4 of
"/mnt/93fd06e5-877d-4514-a81f-769dbfb90089/pedro/tmp/hola/UTF8_Test/UTF8_Test.thy"):
*** Package inputenc Error: Keyboard character used is undefine
*** d
*** (inputenc) in inputencoding `utf8'.
*** See the inputenc package documentation for explanation.
*** ...
*** Erdö
*** Failed to build document "document"
One further thing to notice is that after failure, a standard LaTeX
compilation (using pdflatex) of the files created at ./output/document
succeeds without complaining about the utf8 chars.
By checking the logs I realized the document preparation is through
LuaTeX. Might that be the reason?
Thanks for any help.
utf8_test.tar.gz
Email Gateway (Jan 28 2021 at 11:12):From: Makarius <makarius@sketis.net>
Yes, LuaTeX had a lot of recent refinements concerning UTF8. A current version
works smoothly most of the time, older versions don't.
Your example is OK on my standard Ubuntu 20.04 installation, also my standard
Windows + MikTeX installation.
You can either update Linux/LaTeX or make your latex sources less ambitious,
using old-fashioned escape sequences like Erd\"os for Erdös, or better
Erd\H{o}s for proper Hungarian Erdős.
Makarius
Last updated: Jul 15 2022 at 23:21 UTC