[isabelle-dev] Jenkins maintenance

[Makarius]

On 03/10/16 17:12, Manuel Eberl wrote:
> 
> I for one think that a big improvement would be a system where no one
> pushes to the repository directly: every push goes to a testing server,
> and if the test is successful, the changes can then automatically be
> merged into the repository without an additional test.

When we introduced Mercurial in 2008, this was one idea to aim at
eventually. Today, I would refrain from any automatic daemon producing
changesets.

Instead, it should be easy and painless for human users to do that
themselves. At some point, builds could be integrated nicely into the
Prover IDE, together with regular Mercurial repository operations.


> It would also be an effective safeguard against breaking the repository (and possibly even the AFP),
> which /does/ happen quite frequently. (cf. the current situation where
> things have been broken for days)

I also prefer to have AFP working all the time, but that would require
much more resources, both hardware and humans.

A broken Isabelle repository is different: it means all wheels stand
still. That can be easily avoided by spending about 20min with manual
tests before pushing -- on decent hardware.

When the Isabelle repository is broken, which happens about 2 times per
year, there are friendly mails on isabelle-dev about it, mostly
reminders of README_REPOSITORY. Can you point out a mail thread, where
anybody was seriously blamed for it?


> Another improvement I can think of is
> that it would be good to have a little more control over testing:
> aborting tests when they are not necessary anymore, testing only the
> repository (and not the AFP) etc. All of this we can talk about and find
> a solution in time.

Yes. I read it as: ssh access to a proper test machine. That is the
traditional Isabelle development model.

When the Prover IDE learns to use remote machines eventually, that will
also use ssh for direct interaction with jobs.


> The reality of it all is that our testing infrastructure was in shambles for
> quite some time. Then Lars came along and put in a lot of effort to get
> things up and running again. The main response on this mailing list were
> vague insinuations that he does not understand how to do tests, or does
> not care about doing it properly, which could hardly be farther removed
> from the truth.

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.

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.

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.


	Makarius