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
