[isabelle] Problems with LIPIcs and Isabelle document preparation

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

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


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