[isabelle-dev] Grouping ISABELLE_FULL_TEST?

Lars Hupel hupel at in.tum.de
Mon Feb 1 09:07:08 CET 2016

> Clustering weak nodes always requires more administrative efforts than
> just one or two fat nodes without special tricks.

This is technically correct, but not to the extent you're implying.
Managing one more node with the current setup is literally just another
line in the Ansible configuration.

In fact, I have two configurations, one for testing and one for
production. The testing setup consists of 2 nodes, the production setup
of 5+ nodes. The administrative efforts for both are exactly the same.
All nodes can be bootstrapped from a vanilla Debian/Ubuntu installation.

The reason I'm jumping through these extra hoops with Ansible is that
this finally gives us a reproducible setup.

(NB: Obtaining new hardware hasn't been ruled out yet. These weak nodes
exist to have at least *something* reliable.)


More information about the isabelle-dev mailing list