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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev