[isabelle-dev] \nexists

[Makarius]

On 16/07/16 14:26, Tobias Nipkow wrote:
>>
>> 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.

I am open to hear arguments why latex documents need to be continuously
available. So far there were none.

Instead we have in Isabelle/76492eaf3dc1 + AFP/89fba56726d8 a typical
situation where formal checking no longer works, due to changes in main
Isabelle that are not immediately clear.


In the last 10 years, continuous testing of Isabelle + AFP had the
following main purposes:

  * Make sure that formal checking of Isabelle always works 100% (main
repository).

  * Help to figure out quickly why a broken AFP stopped working. When
did it work last time with Isabelle?

  * Provide continuous performance measurements to keep everything going
in the longer run: i.e. to avoid the "invisible concrete wall" that is
always ahead of us, and moved occasionally further ahead.


Only little of that has been provided by the testing infrastructure in
recent years. The new Jenkins setup and the new hardware has improved
the sitation a bit, but we are still below the situation from some years
ago.

This is why I am doing more testing manually on my own machine than was
necessary in the past.


	Makarius