Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problems with LIPIcs and Isabelle document pre...


view this post on Zulip 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

view this post on Zulip 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 ...

view this post on Zulip 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: Mar 28 2024 at 20:16 UTC