[isabelle-dev] NEWS: Isabelle sessions and build management

[Tobias Nipkow]

Am 29/07/2012 03:16, schrieb Gerwin Klein:
> On 29/07/2012, at 5:06 AM, Makarius <makarius at sketis.net> wrote:
>> For AFP, I would like to see a scheme without hardwired "document" option within the ROOTs. Instead it can be provided for particular invocations of "isabelle build -o document=pdf" etc.  This and build -j MAX should give a great speedup of everyday testing of AFP, with latex out of the way and many cores busy.
> 
> This will need some care. The documents and outline are one major outcome (some might say the whole point) of the AFP sessions. So we still need to test them in the nightly run

This would give us one more dimension of incompleteness of AFP tests. Mira
already omits some of the sessions. Now we would omit latex. But we would need
to run latex overnight. And when an entry is checked it. And possibly also when
an entry is updated. This leads to a proliferation of special cases and creates
more opportunities for introducing errors that are overlooked/ignored.

Tobias