[isabelle-dev] Isabelle/Admin area

Makarius makarius at sketis.net
Fri Oct 21 17:24:01 CEST 2016


We are heading towards a release, which is the time to consolidate and
improve the overall setup (currently at Isabelle/692a1b317316).

The Isabelle/Admin directory is the authoritative place where Isabelle
self-administration happens. E.g. Isabelle/Admin/Release has a few notes
and scripts for the final launch.


The actual work of administrative tools is increasingly done in
Isabelle/Scala, which is the main system programming language of
Isabelle. The directory src/Pure/Admin contains the Scala sources of
interesting tools like build_release.scala or build_history.scala -- the
outer wrappers are Admin/build_release and Admin/build_history.

The build_history tool is particularly relevant to produce systematic
performance data from Isabelle build processes: it operates on old
versions back to the tag "build_history_base" (08-Jan-2013). Thus it
allows to redo tests that were somehow omitted or garbled in the nightly
builds.


The Isabelle/Scala module Build_Log provides operations to access old
and new log files, e.g. from isatest back to 2002. This information
should at some point be stored in a proper database, e.g. a plain file
managed by SQLite (see the Isabelle/Scala module of the same name) or a
proper datebase server. That will eventually allow to work
systematically with "telemetry data" over the repository, to figure out
where resource and performance problems first occur in the history.


There is also a small cronjob for administrative purposes
(Admin/cronjob/main and src/Pure/Admin/isabelle_cronjob.scala). It is
inspired by old isatest, but omits its old weaknesses -- such as direct
NFS access to shared log areas. Instead it all works via the SSH and
Mecurial modules of Isabelle/Scala. The requirements for a remote
machine to participate in testing are rather minimal: SSH access to some
Unixoid environment, which may be also Cygwin.

Administrative cronjobs come and go according to particular needs; the
Isabelle history documents that by normal commits. For example, David
Matthews is presently working on the next big update of Poly/ML, and
when a build of Isabelle mostly works there will be a nightly test to
keep watch on it over some weeks or months.


During spring and summer this year, I have spent a lot of energy to
explain the needs for "tooling" to support Isabelle administration
properly. Now I've spent only 2-3 weeks to implement most of that on the
spot.

A few things are still missing, e.g. a little bit of HTML presentation.
On the other hand, the Isabelle environment is PIDE-centric, so
Isabelle/jEdit might eventually acquire some administrative GUI tools,

But that is a different story for a different release ...


	Makarius


More information about the isabelle-dev mailing list