[isabelle-dev] Further updates on isabelle-dev infrastructure

[Makarius]

The traditional spot for isabelle-dev resources (repository snapshots,
build log status etc.) is http://isabelle.in.tum.de/devel

I have done quite a lot of renovation of the infrastructure behind that
in the past 2 years, and now again some more. Here is a summary of
notable points (referring to current  Isabelle/7e223a05e6d8).

  * The main cronjob and the build_log database server (PostgreSQL) are
now running on just one virtual Ubuntu server. This simplifies the
administration, e.g. there is no longer the Gentoo installation of
lxbroy10 to worry about. It also removes past uncertainties about the
ultimate responsibility of system administration on various hosts: I am
just doing it myself for a single node, which is very easy thanks to
https://help.ubuntu.com/lts/serverguide (before I did it already for the
PostgreSQL node).

  * The web hosting of http://isabelle.in.tum.de/devel is also on that
server: there are HTML forwards from the toplevel index.html files, but
not for other files (e.g. generated PNGs). The target address is
https://isabelle.sketis.net/devel -- I have switched almost everything
to HTTPS recently.

  * The build status page https://isabelle.sketis.net/devel/build_status
will continuously provide more relevant information. A minor addition is
the "data: CSV" entry. This helps to figure out Mercurial changeset ids
for significant changes in the timing seen in the charts. On my Linux
box, opening CSV triggers the Spreadcheet application of LibreOffice,
which is adequate for further inspection. I could provide further data
formats if this is required (e.g. SQLite db).

  * The main build_history jobs for testing and timing repository
versions are run via plain ssh, with minimal assumptions about the
target system. This can sometimes be tricky, e.g. to connect to LRZ
cloud nodes that have no public IP address, by tunneling Isabelle/Scala
ssh connections as well as Mercurial ssh connections (thery use
different SSH libraries). Today it appears to work properly for the
first time and we should see "AFP slow" charts in the evening.

This flexible ssh setup also means that build hosts may be almost
everywhere and everything (Linux, macOS, Windows + Cygwin sshd). People
who have (potentially old) server-class machines running somewhere and
want to donate nightly-build resources are welcome to contact me personally.

Note that cloud nodes that are too much virtualized don't help for
precise performance measurement. E.g. a cheap service like
https://www.netcup.de/vserver/vps.php#features is not sufficient for
proper timing -- I am presently using the VPS 500 G8 offering for the
cronjob + db server.


	Makarius