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
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
