[isabelle-dev] Mira still alive?

Lars Hupel hupel at in.tum.de
Mon Apr 13 14:57:24 CEST 2015

> 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

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


* 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).

More information about the isabelle-dev mailing list