Glad you brought up this topic (although it isn't "spam" for any meaningful definition of "spam"). I wanted to do it anyway, because somebody asked me about it privately.
> Jenkins sends lots of mails, and I find it hard to pay attention to them > at all. Even when I do look, the long message body makes it hard to find > the key points: What failed? Why did it fail? The message body consists of the entirety of something similar to "isabelle build -v". As such, it is not excessively long. As usual, a summary is printed at the very end, consisting of the sections "timing" and "failed sessions". > * Tests are run less often, e.g. 2-3h after a push and including all > later pushes in that time interval. This reduces test runs and increases > chances that Isabelle + AFP correspond correctly when Jenkins makes a > snapshot. That would hardly be "continuous integration", more like "delayed integration". As a first measure I have increased the grace period for the "isabelle-repo" job from 5 seconds to 5 minutes. This should give ample time to push already existing changesets to both repositories. Increasing the grace period even more does not make sense, for two reasons: 1) The vast majority of build failures were because of large-scale refactorings which cannot be done in 2 hours. 2) It contradicts your previous mail where you wanted to know exactly what push broke the build. The missing tooling here is for continuously testing accumulated changes to both the repository and the AFP in these situations, without affecting the global build. Git people use branches for that. In Mercurial, the replacement is unclear. > * Mails are sent only once per day, as a summary of broken sessions at > the end of the day, not every intermediate state. This is too stateful. A compromise I can offer is to send a mail whenever the build breaks, but not when it remains broken. For the records, attached is a list of triggers supported by the mail plugin. > If Jenkins were more like a queue management system, it could probably > also provide immediate feedback to the person who pushed something > broken to it. Jenkins can already do that. It doesn't work for our repositories though because there are usually no mail addresses associated with changesets. Cheers Lars
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev