[isabelle-dev] \nexists

[Makarius]

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


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