Re: [isabelle] Isabelle document generation and ACM and LIPIcs LaTeX styles

On 20/01/2021 08:36, Tobias Nipkow wrote:
> This is an experience report that highlights problems when preparing an
> Isabelle-based document with LaTeX style files provided by the ACM and by LIPIcs.
> 1. Isabelle style files use the plain tex comment package (for speed). This
> apperas to clash with ACM and LIPIcs.

I will do something about this for the next release: Isabelle2021-1 (December
2021). Presently I am collecting more problems and drafting some ideas how to
do better --- after more than 20 years of naive LaTeX generation from Isabelle/ML.

> 2. Luatex does not work for LIPIcs:
> It works without problem with pdflatex. In fact, it would be nice if one could
> tell Isabelle easily to use a specific latex instead of having to write a
> build file.

This will also work better in Isabelle2021-1: we still need old pdflatex for
various publishing channels.

I am also interested in the most nasty and annoying hacks in document/build
scripts, in order to eliminate the need for them and let the default
Isabelle/Scala setup do it directly.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.