Re: [isabelle] Isabelle document generation and ACM and LIPIcs LaTeX styles
- To: Tobias Nipkow <nipkow at in.tum.de>, Isabelle Users <isabelle-users at cl.cam.ac.uk>
- Subject: Re: [isabelle] Isabelle document generation and ACM and LIPIcs LaTeX styles
- From: Makarius <makarius at sketis.net>
- Date: Sat, 5 Jun 2021 13:25:53 +0200
- Authentication-results: cam.ac.uk; iprev=pass (mta1.cl.cam.ac.uk) smtp.remote-ip=126.96.36.199; spf=softfail smtp.mailfrom=sketis.net; dkim=pass header.d=sketis.net header.s=key2 header.a=rsa-sha256; arc=none
- Authentication-results: cam.ac.uk; iprev=pass (relay.yourmailgateway.de) smtp.remote-ip=188.8.131.52; spf=pass smtp.mailfrom=sketis.net; dkim=pass header.d=sketis.net header.s=key2 header.a=rsa-sha256; arc=none
- Authentication-results: mx2f26; spf=pass (sender IP is 184.108.40.206) smtp.mailfrom=makarius at sketis.net smtp.helo=[192.168.179.20]
- In-reply-to: <email@example.com>
- References: <firstname.lastname@example.org>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.8.1
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