[isabelle-dev] Notes on isabelle build -a

[Makarius]

The art of manual isabelle build -a seems to have been forgotten, so
here are some basic notes in accordance to README_REPOSITORY (e.g.
Isabelle/4effb93c2a09).

In contrast to the batch-queue model of testboard, manual builds are
incremental to some extent: the full build happens in the context of a
few local changes, re-using already available heaps and logs (which
contain command timing information that improves multicore performance).
There is no need to reset to a completely clean situation, as usually
done by automatic batch tests.

Of course, a local change to Pure or HOL requires almost everything to
be rebuilt, but it can be interleaved with editing to some extent. In
lucky situations, only small parts require a rebuild; this happens in
approx. 50% of merge situations.


A typical workflow proceeds as follows:

  * "hg fetch" to resynchronize with the world out there

  * "isabelle build -j4 -a" to keep the hardware busy, before doing
anything else

  * spend time inspecting all incoming changes, they might be relevant
for planned edits

  * spend time thinking about edits, eventually work on them

  * when the initial build -a has terminated, local changes can be saved
and tested locally

  * iterate the last two items 1-30 times

  * get ready to push: hg fetch + isabelle build -a as before

  * finally push a fully tested version

In most situations, the elapsed time for the two extra build -a
processes (due to newly pulled material) is shorter than two fully clean
builds.

Of course, the whole affair needs decent hardware and ssh access to it.
(It sometimes helps to use rsync over ssh, to avoid auxiliary commits
pushed between private test repositories.)


	Makarius