Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] NEWS: Document preparation engine updates


view this post on Zulip Email Gateway (Sep 27 2020 at 19:26):

From: Makarius <makarius@sketis.net>
* Document preparation *

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

view this post on Zulip Email Gateway (Sep 28 2020 at 11:01):

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: Mar 04 2024 at 10:08 UTC