> 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.) Cheers Lars _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
