[isabelle-dev] Bad theory import "Main"

[Lars Hupel]

> 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.

You yourself proposed investigating Jenkins (then Hudson) some while
ago, pointing out that e.g. the Scala team is using it. Then, later,
when I got started in the Munich group, we talked with e.g. Alex and
other stakeholders about Jenkins. Then, later, you came in person and
discussed various things. Up until that point in time, I didn't get the
impression that you were categorically opposed to the idea of Jenkins.
If so, you didn't say it. Then, out of the blue, you stopped caring,
unsubscribed for strange reasons from the CI list and started calling
Jenkins a "monster" and a "waste of resources".

It is because of that that I'm having a hard time believing that you're
willing to engage in constructive dialog about regression testing anymore.

You claim that you "did not get any answers". In reality, you got all
the answers and ignored them.

It is apt that you describe your private testing setup as a "workaround"
for the loss of platform support, because that is exactly what it is.
Multiple times I attempted to get Windows and OS X support working, by
talking to various people who need or have access to our compute
resources. You ignored that and worked around it.