Am 29/07/2012 03:16, schrieb Gerwin Klein: > On 29/07/2012, at 5:06 AM, Makarius <makar...@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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
