> 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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev