From: Makarius <makarius@sketis.net>
* Document preparation *
The standard LaTeX engine is now lualatex, according to settings
variable ISABELLE_PDFLATEX. This is mostly upwards compatible with old
pdflatex, but text encoding needs to conform strictly to utf8. Rare
INCOMPATIBILITY.
Discontinued obsolete DVI format and ISABELLE_LATEX settings variable:
document output is always PDF.
This refers to Isabelle/684f14b1e7fc (and AFP/35158287da0b).
At the Isabelle Workshop 2020, Clemens Ballarin proposed to switch to LuaLaTeX
by default: it allows advanced packages programmed in the Lua scripting language.
It has only required 2.5 days to clear out AFP documents in that respect.
If all turns out fine, I will later make use of the updated engine, e.g. to
have \usepackage[T1]{fontenc} and \usepackage{textcomp} by default: it allows
proper french single-quotes (for cartouches) without odd font problems.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
From: Makarius <makarius@sketis.net>
One more thing: using visual diffpdf on Ubuntu 18.04, I have compared various
important "doc" entries, e.g. prog-prove, jedit, implementation, isar-ref.
After Isabelle/8162ca81ea8a the results are mostly identical, with a few minor
deviations in font-metrics and hyphenation: both work generally better in
LuaLaTeX.
There might be more fine points to watch out for.
As a general principle, documents that use Isabelle mechanisms like the
@{verbatim} or @{text} antiquotations work better than low-level
"LaTeX-drawings" done manually (e.g. \verbatim and $...$).
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Oct 12 2024 at 20:18 UTC