clarified notion of unknown files: ignore files outside of a Mercurial repository;

more balanced AFP partitioning;

more abbrevs -- this makes "(=" ambiguous and thus simplifies input of "(=)" (within the context of Main HOL);

tuned -- more uniform;

eliminated somewhat pointless parallelism (from 857da80611ab): usually hundreds of tasks with < 1ms each, also note that the enclosing join_theory happens within theory graph parallelism;

Drop rewrite rule arguments of sublocale and interpretation implementations.

more balanced AFP partitioning;

clarified signature;

build_history_base as remote build on lxbroy10: thus self_update has already happened once, and thus avoids conflicts with parallel builds on shared home directory;

more robust: normalize potentially symbolic rev;

proxy setup for lrzcloud1;

tuned signature;

support for permissive connections, for odd situations where host keys are not accepted;

proper target directory;

eliminated dead code from 2a1acc88a180 (presumably left over from ML type-inference experimentation);

document existing Apache2 configuration;

consolidated main cronjob server on virtual machine together with build_log database; eliminated special tricks for Gentoo; import plain_identify logs, export all logs for backup; run build_release, build_history_base in parallel to remote_build_history tasks;

identify closer to main cronjob -- avoid diverging changeset versions;

Drop rewrites after defines in interpretations.

proper remote_mac according to Admin/Release/CHECKLIST;

more Java heap, e.g. relevant for hg.graph on Isabelle repository;

more robust check -- do not rely on return code;

more compact ML_Statistics, to make build_status work with less than 2GB heap;

retain latest ml_stats (amending e76c6cb0d461);

accomodate smaller build machine;

clarified signature;

clarified self_update: imitate visible directory state on remote side;

more operations;

self_update implies push_isabelle_home (see also 4c253e84ae62);

uniform setup_repository (pull/clone without update); tuned signature;

clarified signature: facilitate interactive experimentation;

clarified tasks;