Re: [isabelle] Problems with LIPIcs and Isabelle document preparation



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


--
  Peter


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:
> https://www.dagstuhl.de/en/publications/lipics/instructions-for-autho
> rs
> 
> 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
> 




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