Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle document generation and ACM and LIPIc...

view this post on Zulip Email Gateway (Jan 20 2021 at 07:37):

From: Tobias Nipkow <nipkow@in.tum.de>
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. My crude solution is to disable the
    offending macros:

\usepackage{isabelle,isabellesym}
\def\isadelimtheory{}\def\endisadelimtheory{}
\def\isatagtheory{}\def\endisatagtheory{}
\def\isadelimML{}\def\endisadelimML{}
\def\isatagML{}\def\endisatagML{}
\def\isafoldML{}
\def\isadelimproof{}\def\endisadelimproof{}
\def\isatagproof{}\def\endisatagproof{}
\def\isafoldproof{}
\isabellestyle{it}

I am sure there is a better solution.

  1. Luatex does not work for LIPIcs:

Latex error (line 7 of
"/usr/local/texlive/2020/texmf-dist/tex/generic/pdftex/glyphtounicode.tex"):
Unde
fined control sequence.
\pdfglyphtounicode

The combination of luatex and \pdfglyphtounicode is discussed a little here:
https://tex.stackexchange.com/questions/404566/is-glyphtounicode-useful-with-lualatex-or-not-useful

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.

Tobias
smime.p7s

view this post on Zulip Email Gateway (Jan 23 2021 at 14:26):

From: Makarius <makarius@sketis.net>
On 20/01/2021 08:36, Tobias Nipkow wrote:

  1. Luatex does not work for LIPIcs:

Latex error (line 7 of
"/usr/local/texlive/2020/texmf-dist/tex/generic/pdftex/glyphtounicode.tex"):
  Unde
  fined control sequence.
  \pdfglyphtounicode

The combination of luatex and \pdfglyphtounicode is discussed a little here:
https://tex.stackexchange.com/questions/404566/is-glyphtounicode-useful-with-lualatex-or-not-useful

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.

I have experimented a bit with my demo setup for LIPIcs:
https://makarius.sketis.net/repos/LIPIcs

The relevant changes are:

changeset: 3:68ac580ac444
user: wenzelm

view this post on Zulip Email Gateway (Jun 05 2021 at 11:26):

From: Makarius <makarius@sketis.net>
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.

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

Makarius

view this post on Zulip Email Gateway (Nov 22 2021 at 19:21):

From: Tobias Nipkow <nipkow@in.tum.de>
What is the situatiuon here? I still run into the old (comment) problems (it
seems). Do I need to do something special?

Thanks
Tobias
smime.p7s

view this post on Zulip Email Gateway (Nov 22 2021 at 20:19):

From: Makarius <makarius@sketis.net>
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
https://makarius.sketis.net/repos/LIPIcs together with last-minute fine points
for the Isabelle2021-1 release, such as
https://isabelle.sketis.net/repos/isabelle-release/rev/6424f74fd9d4

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

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

Makarius

view this post on Zulip Email Gateway (Nov 25 2021 at 11:22):

From: Makarius <makarius@sketis.net>
There is now improved support for Dagstuhl LIPIcs here, without the awkward
build script:

https://isabelle.sketis.net/repos/isabelle-release/rev/4faf0ec33cbf

https://makarius.sketis.net/repos/LIPIcs/rev/bae7fa0f17a6

This will be in the next release candidate for Isabelle2021-1 (within the next
few days). Afterwards I will merge it back to the isabelle-rev and switch
mentally to the post-release mode.

Makarius

Last updated: Jan 04 2025 at 20:18 UTC