[isabelle-dev] Jenkins maintenance

Lars Hupel hupel at in.tum.de
Thu Oct 6 15:07:44 CEST 2016


> I had many private discussions with Lars in the past few months. I even
> pointed out important requirements before the start of the Jenkins project.

I am aware of that (I keep notes), and also of the relevant email
threads dating back to 2014.

> The present situation is that we have no proper test environment after
> isatest was shutdown prematurely. This is what I have called "flying
> blind", because vital performance measurements are missing.

This was already your criticism in 2014, because the performance
measurements weren't even that good when I took over. At some point, you
showed me the "/devel" graphs and explained to me that we need something
better for serious measurements. I fail to see how the situation is now
somehow worse than what we had with isatest.

In fact, the situation was even worse back then: Various Isabelle
developers have told me that they're using "macbroy2" which would
otherwise be used for isatest/afptest for private experiments. Since a
full test run would sometimes take some 10 hours, collisions were pretty
much guaranteed.

There cannot be useful performance measurements unless the environment
is controlled, i.e. free of other accesses.

> I need to improvise something for the coming release -- which is the
> reason why I have been off-line for some days, and also postponed the
> start of the hot phase for Isabelle2016-1.

What exactly do you have to improvise?

Cheers
Lars



More information about the isabelle-dev mailing list