nipkow at in.tum.de
Sat Jul 16 14:26:51 CEST 2016
On 15/07/2016 20:33, Makarius wrote:
> On 15/07/16 17:08, Tobias Nipkow wrote:
>> For me a default is something that a) is beneficial for the majority of
>> users and b) can be overwritten if you don't like it. Isn't that
>> possible here?
> That is the existing default of not insisting in Latex documents in
> every single point of history. When there is something wrong with Latex,
> it is usually easy to repair afterwards.
> Asking everybody to test Latex every time imposes a burden with little
> In contrast, a full "build -a" for the formal content is vital. The
> shorter that takes, the more it becomes second nature to do it
> frequently -- I often do it for every single changeset (before the local
Your notion of what is good for developers differs from their own notion, at
least for the ones I talked to. But it turns out you are right: combining -a and
-o document=pdf is not a good idea, it breaks Logics_ZF.
> The current Isabelle Jenkins setup has changed focus slightly. There are
> more continuously built "artifacts", like documents, but important
> "telemetry" data visualization is missing. So we are flying blind
> concerning performance figures, not just for AFP (as we do for many
> years), but also for the main repository.
> What is really needed now, is a replacement for
> That also depends on good physical measurements: that was historically
> done without Latex getting in between.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5135 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev