[isabelle-dev] Mira still alive?

[Lars Hupel]

> This raises the questions whether somebody is still seriously relying on
> mira or whether it it time to admit that this approach has failed after
> some initial enthusiasm in 2010/2011.
> 
> I would still appreciate a less ambitious continuous integration testing
> environment for Isabelle etc. using existing platforms, e.g . Jenkins.

Some time ago I performed some trials with Jenkins to determine which
parts of the current workflow can still be supported:

* the nightly builds are trivial to model in Jenkins
* testboard might need some work, but it is feasible
* all my attempts at getting Jenkins to properly version (as in: store
changes in a Git or Mercurial repository) failed because the plugins
which promise to do this are either outdated, broken or both
* it natively supports LDAP-based authentication via web which makes it
easy to make changes in the build configuration
* building on multiple hosts in parallel is simple and requires very
little setup apart from a working SSH connection

The major pain point with Jenkins is ensuring security: If we run this
service ourselves* _and_ it should be accessible from the Internet (not
just from TUM's internal network), it needs continued attention, both
for the operating system and Jenkins. Jenkins releases happen very
frequently (~ once a week). This wasn't a problem with Mira previously,
because the attack surface is much smaller. (AFAIK the web interface is
read-only.)

The good news is that administrating a Jenkins server does not require
root access, which means we might be able let our local sysadmins manage
the server. I'll try to investigate whether they have the resources for
that.

Cheers
Lars


* The other option – a hosted Jenkins instance – likely won't work for
us, because the available machines are not beefy enough (e.g. CloudBees
offers VMs with a measly 8 GB RAM, as compared to our own lxbroy10 which
has 128 GB).