Changes

Summary

1. merged
2. misc tuning and clarification: more standard Same.commit discipline;
3. tuned;
4. tuned names;
5. more operations; more accurate treatment of beta contraction in norm_term/norm_proof, following Envir.norm_term;
6. minor performance tuning: more careful treatment of empty environment;
7. clarified signature;
8. more zproofs;
9. clarified signature: support shared cache;
10. tuned;
11. tuned: avoid shadowing;
12. more zproofs;
13. tuned;
14. more operations; clarified cache;
15. tuned signature;
16. tuned names;
17. tuned -- eliminate clones;
18. tuned;
19. more operations;
20. more operations;
21. tuned;
22. clarified signature;
23. tuned;
24. tuned;
25. consider schedule calculation time in estimation;
26. compare previous build schedule with new one, to prevent regressions;
27. clarified: build schedules may be outdated when empty, after some time, or due to build progress;
28. store previous build jobs in graph so schedules can be used later in the build process;
29. add serial for build schedule to avoid unnecessary db read/writes;
30. tuned;
31. clarified;
32. tuned;
33. use build database to synchronize build schedule computed on master node (e.g., such that view on cluster is consistent);
34. add build uuid to schedule;
35. tuned;
36. use schedule directly instead of extra cache;
37. added build schedule command-line wrapper;
38. added graphical representation of build schedules;
39. clarified build heuristics parameters;
40. proper parallel paths: factor in elapsed time;
41. performance tuning: cache estimates;