#462 (Nov 1, 2017, 12:50:11 AM)

1. removed unused option, which is potentially expensive; (detail / hgweb)
2. allow to augment session context via explicit session infos;
   more compact required_session interface; (detail / hgweb)
3. synthesize session with all required theories from other session imports; (detail / hgweb)
4. clarified signature; (detail / hgweb)
5. clarified signature; (detail / hgweb)
6. clarified signature; (detail / hgweb)
7. clarified signature; (detail / hgweb)
8. clarified signature: global_theories is always required; (detail / hgweb)
9. tuned; (detail / hgweb)
10. tuned signature; (detail / hgweb)
11. clarified modules; (detail / hgweb)
12. minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC; (detail / hgweb)
13. more permissive: db could be empty after hard crash; (detail / hgweb)
14. no censorship (in contrast to 2c828c830ad7); (detail / hgweb)
15. A few more topological results. And made some slow proofs faster (detail / hgweb)
16. removed ancient nat-int transfer (detail / hgweb)
17. added lemma (detail / hgweb)

Started by an SCM change

This run spent:

• 9.8 sec waiting;
• 1 hr 15 min build duration;
• 1 hr 15 min total from scheduled to completion.