[isabelle-dev] New testing infrastructure

[Lars Hupel]

Dear Isabelle developers,

as promised last week, I've been working on a new testing infrastructure
for Isabelle. Here's what works now:

* There is a live Jenkins instance at <https://ci.isabelle.systems/>
[1]. It is publicly available and runs on a virtual machine provided by
the department's sysops. Builds are triggered automatically. The builds
themselves run on the lxbroy* machines provided by the chair's sysops
(as before).

* For security reasons, the Jenkins instance can't be configured via the
web interface. All configuration must go through Ansible [0] and is
versioned. Ansible reads the configuration and applies it to the host
automatically when invoked. This requires root access on the virtual
machine (currently, Johannes and I have root access). I will put the
Mercurial config repository under nfs:/home/isabelle at some point so
that it is accessible for everyone with an account here. (The
configuration contains critical information, e.g. passwords and private
keys, which is why it can't be public.)

* The "single source of truth" continues to be the main Isabelle
repository (hosted at <https://isabelle.in.tum.de/repos/isabelle>).
Jenkins polls it every couple of minutes and spawns a build on every
change. Here's an example:
<https://ci.isabelle.systems/jenkins/job/isabelle-repo-hol/2/>.

* Not yet ported are, in decreasing order of priority: testboard,
reports, isatest, afptest. I will contact the responsible persons soon
to work out a migration plan.

Cheers
Lars



[0] <https://docs.ansible.com/ansible/index.html>
[1] <http://isabelle.systems> forwards to <https://isabelle.in.tum.de/>