[isabelle-dev] \nexists

[Tobias Nipkow]

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

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.

Tobias

>
> 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
> Admin/isatest/isatest-statistics.
>
> That also depends on good physical measurements: that was historically
> done without Latex getting in between.
>
>
> 	Makarius
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5135 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160716/1f090443/attachment.bin>