[isabelle-dev] \nexists

Makarius makarius at sketis.net
Fri Jul 15 20:33:51 CEST 2016

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

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.


More information about the isabelle-dev mailing list