[isabelle-dev] Jenkins maintenance

[Lars Hupel]

Thank you for bringing the discussion back on track. Let me try to
address the remaining points.

> 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. This avoids the
> current duplication of tests where one first pushes to the testboard,
> waits for everything to run through, and then pushes to the repository
> where everything is tested again.

This is definitely achievable; however, it needs broad developer
consensus first, because it's a change in the usual workflow. Consider
this a call for opinions.

Granted, the duplication of tests is an issue, but unfortunately, hard
to avoid under the current circumstances. By changing the workflow to
make breaking changes (except possibly AFP) "syntactically impossible",
many things can be simplified. Bitbucket, for example, has facilities to
enable such a workflow.

However, before we do that, we need to think carefully about formalising
the connection between Isabelle and the AFP. I'll let others take the
lead on this – Florian, maybe?

Also note that the status page now includes a load diagram. While the
interpolation is somewhat strange, it shows a clear trend: the
infrastructure is operating below 50% capacity.

> According to the official README_REPOSITORY
> (http://isabelle.in.tum.de/repos/isabelle/file/ec0fb01c6d50/README_REPOSITORY#l282)
> there is
> 
>   * no need to test pdf documents

This is arguable. In fact, it is very convenient to have documents in a
continually working state, because Jenkins also serves a "continuous
delivery" purpose: The AFP statistics page, and also everything else on
<https://devel.isa-afp.org/> (including documents) is being produced by
Jenkins. Failure to produce a document in that sense is also a failure
to present an entry.

In the long term, it could also make sense to present the official
Isabelle documentation (i.e. everything in "~~/src/Doc") in a similar
fashion. Currently users have to build documents themselves.

> The 1 thread test is the base of all other tests. Without that it
> becomes very difficult to see anything concerning performance changes.

This is not a problem; I have it on my list anyway.

Makarius, last time we spoke I didn't get the impression that this is
crucial for performance analysis, which is why I didn't prioritize it.
As always, I first need to figure out how long this takes on our
hardware and if necessary, provision an appropriate machine. It would
also be great if, as we discussed, there was a possibility to control
"ML_OPTIONS" via options instead of environment variables.

> I am still hoping for October (which is actually now). I have explained
> many times privately, what the purpose of "platform tests" is: a
> portfolio of officially supported platforms -- some of them unusual for
> most isabelle-dev users -- need to be continuously tested (meaning once
> per day, or even once per week).

Together with Thomas Fritz I have already provisioned a native (i.e.
non-virtualized) El Capitan worker a week ago [0]. It runs a nightly
"build -a" job [1], 32 bit, 2 threads. It requires approx. 5 h for that.
It also doesn't send messages on failure (currently).

Makarius, if you'd like to be subscribed to build mails, please tell me.
Otherwise it'll stay silent.

> Mira was actually quite good in adjoining information to the repository
> history views of the two repositories. Over a few years, that was the
> main tool for me to figure out what works and what not, and to see when
> it stopped working etc. Right now, it requires much more clicking, and I
> am still unsure where the information is actually hidden.

The reason why it was "quite good" is that it was tightly coupled to the
Mercurial API; this is also the reason for its eventual demise.

There are two possible proper solutions for this, "push" and "pull".

Pull: Implement a loosely-coupled extension for hgweb to fetch
information from Jenkins. All changesets and their statuses are recorded
in there and can be retrieved from the API, not unlike the statistics
page. This can be done with Javascript and implemented without changing
anything in Jenkins.

Push: Embrace Bitbucket and use their "Build Status" API [2]. This
information is displayed in the "Builds" column in the "Commits" view.
Of course, this only works for repositories hosted on Bitbucket. This
likely requires some Scala code to work (i.e. performing an
authenticated HTTP request).

I'd be happy if someone other than me could take the lead on this.

> Also note that the Mira architects were actually looking at Jenkins at
> that time, and pointed out that it was a bit old-fashioned in focusing
> on "latest" versions by default and lacking proper changeset identification.

I don't understand what that means. "Changeset identification" works
perfectly fine. In fact, many of the jobs in our current setup are
triggered with explicit changeset ids.

> This means, any Isabelle tools built on top of Jenkins need to try hard
> to do it the proper way, e.g. working over timeless / stateless
> Mercurial history in a monotonic fashion. Views should make it easy to
> see "into the history", without requiring a lot of clicking.

The Jenkins build history is also monotonic. Some additional glue code
is required to connect that history to the Mercurial history. But as
sketched above, that requires much less than Mira, which used an
additional database to store this information.

> 2) Further, »keep it simple, stupid« came to its limits with all the
> involved technicalities: issues jobs on remote machines, exception
> handling, proper daemonizing – it is surely easy to extend that list.
> The Jenkins universe, as fas as I can tell, embodies significant
> expertise in that area which you don't want to reimplement.

In software engineering, this is known as "Not Invented Here" syndrome :-)

>   * How much efforts are required to make proper use of it? I.e. what is
> the "payload" of it as a "carrier system" for an actual application.

The advantages, as outlined by Florian, by far outweigh the efforts.

>   * Which policies and attitudes of the platform are forced on the
> application? How easy (or difficult) is it to reshape it for our the
> requirements.

This – of course – greatly depends on the requirements. Jenkins itself
is infinitely malleable through plugins and configuration. But one needs
to carefully evaluate which requirements are inherent and which are
incidental based on the past.

Outside of Isabelle, I've already gathered a lot of experience with
setting up and maintaining build systems (not just Jenkins) and the
usual insight is that if it's complicated to implement in the build
system, it's worth looking closely how to simplify the underlying
structure. Of course, that's nothing new for Isabelle users: the simpler
the definition, the easier the proof.

> And where are the public sources of Isabelle/Jenkins?

I have thought about this again and decided that it's not worth
separating the private from the public parts. There are three reasons:

1) It needlessly complicates the setup. This is not an insurmountable
obstacle, but it requires some additional effort from my end.

2) Changes in the infrastructure can only be done by someone who is
familiar with how the whole setup works and has root access to the
underlying machines and configuration interfaces. Even if the sources
were public and could be changed, there'd still be the manual step of
deploying them.

3) When we're talking about what actually gets executed by Jenkins, it's
rather boring: it runs a single script which resides in "~~/Admin". The
rest of the sources is responsible for painstakingly creating a uniform
environment (from scratch or incrementally) on all three kinds of
machines we have currently; i.e. not interesting outside TUM.

Despite that, I don't want to leave the impression of a lack of
transparency, which is why I will take two measures in the near future:

1) Publish the private documentation of how the system works, which I
have made available so far to anyone who asked. If anyone else is
interested in reading the other parts of the sources, please ask.

2) Open a public tracker for issues and proposals about the
infrastructure. This will also make it easier to track changes.

Cheers
Lars


[0] <https://ci.isabelle.systems/jenkins/computer/workermac1/>
[1] <https://ci.isabelle.systems/jenkins/job/isabelle-nightly-mac/>
[2]
<https://developer.atlassian.com/bitbucket/api/2/reference/resource/repositories/%7Busername%7D/%7Brepo_slug%7D/commit/%7Bnode%7D/statuses/build>