[isabelle-dev] Bad theory import "Main"

[Makarius]

On 23/04/17 15:54, Tobias Nipkow wrote:
> The Isabelle regression test system shows up a mistake in a commit of
> yours and you ask what its purpose is? And tell us your rarely look there?

That was a trivial mistake: easy to spot and easy to repair. We don't
need a huge monster like Jenkins for that, with all its waste of resources.


The key problem of the Jenkins project is that the test coverage that is
required to hold up stable Isabelle releases on many platforms dropped
significantly (one 1 ago). I have recovered from that partially, by
working around Jenkins.

In the past 1.5 years, I've spent a lot of time trying to explain how
the Isabelle administration works. If we don't manage to overcome the
"blame game", things will decline further.


	Makarius