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

On 22/11/2021 20:21, Tobias Nipkow wrote:
> What is the situatiuon here? I still run into the old (comment) problems (it
> seems). Do I need to do something special?

I am presently reworking my LIPIcs example together with last-minute fine points
for the Isabelle2021-1 release, such as

I will do something about isabelletags.sty and comment.sty within the next few

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

That is just "options [document_build = pdflatex]" in ROOT, but there can be
adverse effects concerning unusual isabellesym.sty entries (which I am not
going to change again for the release).


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