clarified signature; minor performance tuning;

tuned signature;

avoid accidental capture of theory value, and thus reduce heap size again (amending 5109e4b2a292);

tuned;

more robust: proper Proofterm.get_proofs_level with bound check;

tuned;

clarified signature: fewer tuples;

clarified signature: fewer tuples;

clarified signature: more explicit get_proofs_level with bounds check;

merged

misc tuning and clarification: more standard Same.commit discipline;

tuned;

tuned names;

more operations; more accurate treatment of beta contraction in norm_term/norm_proof, following Envir.norm_term;

minor performance tuning: more careful treatment of empty environment;

clarified signature;

more zproofs;

clarified signature: support shared cache;

tuned;

tuned: avoid shadowing;

more zproofs;

tuned;

more operations; clarified cache;

tuned signature;

tuned names;

tuned -- eliminate clones;

tuned;

more operations;

more operations;

tuned;

clarified signature;

tuned;

tuned;

consider schedule calculation time in estimation;

compare previous build schedule with new one, to prevent regressions;

clarified: build schedules may be outdated when empty, after some time, or due to build progress;

store previous build jobs in graph so schedules can be used later in the build process;

add serial for build schedule to avoid unnecessary db read/writes;

tuned;

clarified;

tuned;

use build database to synchronize build schedule computed on master node (e.g., such that view on cluster is consistent);

add build uuid to schedule;

tuned;

use schedule directly instead of extra cache;

added build schedule command-line wrapper;

added graphical representation of build schedules;

clarified build heuristics parameters;