[isabelle-dev] NEWS: Document preparation engine updates

Makarius makarius at sketis.net
Sun Sep 27 21:26:26 CEST 2020


*** 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


More information about the isabelle-dev mailing list