Email Gateway (Aug 22 2022 at 20:13): Email Gateway (Aug 22 2022 at 20:13):From: Makarius <makarius@sketis.net>
Dear users of the Isabelle document preparation system,
people with formal documents on ITP 2019 may have noticed some
inconveniences with the LIPIcs LaTeX style:
https://www.dagstuhl.de/en/publications/lipics/instructions-for-authors
Such dropouts have occasionally happened in the past 20 years of
Isabelle document preparation, and there has always been a proper way to
settle the conflicts without downgrading into informality.
The repository https://bitbucket.org/makarius/lipics (presently at
version 8f3aff05b449) contains the basic setup for this relatively
ambitious LaTeX style.
The main idea is to do some postprocessing with perl in document/build:
https://bitbucket.org/makarius/lipics/src/8f3aff05b449/document/build
Presently it ...
* suppresses the use of the "comment" style in PlainTeX mode
* replaces generated comment environments to use LaTeX notation
It looks good so far, but further fine points may be missing. This
mailing list thread is meant to collect further improvements, such that
all Isabelle papers show up on ITP without funny adhoc hacking.
(I am co-author of an ITP paper myself, but it is talking informally
about Isabelle and HOL4, without proper document setup.)
Makarius
Email Gateway (Aug 22 2022 at 20:14):From: Peter Lammich <lammich@in.tum.de>
I get
Bad file 'root.bbl'
when using your script. It comes from the command
isabelle latex root.bbl
even if a root.bbl is in place ...
Email Gateway (Aug 22 2022 at 20:16):From: Peter Lammich <lammich@in.tum.de>
I did not have bibtex in my test setup. How about this?
isabelle latex -o bbl root
Thanks, that worked. (I had already tried "-o bbl root.bib"
and "-o bbl root.bbl", but both did not work)
The usage message of the isabelle latex tool says:
Usage: isabelle latex [OPTIONS] [FILE]
So I assumed I have to put a full file name there.
Last updated: Nov 21 2024 at 12:39 UTC