Re: [isabelle] Problems with LIPIcs and Isabelle document preparation
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 ...
On Mo, 2019-07-01 at 20:21 +0200, Makarius wrote:
> 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:
> Such dropouts have occasionally happened in the past 20 years of
> Isabelle document preparation, and there has always been a proper way
> 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
> 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
> 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.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and