#1050 (Nov 3, 2019, 1:41:16 AM)

1. proper theory for export_proofs; (detail / hgweb)
2. tuned signature; (detail / hgweb)
3. merged (detail / hgweb)
4. just tidied one proof (detail / hgweb)
5. proper graph traversal -- avoid exponential blowup (amending 71d1971d67ad); (detail / hgweb)
6. oops — fixed symbols!! (detail / hgweb)
7. reorganisation to eliminate Brouwer_Fixpoint from complex analysis (detail / hgweb)
8. merged (detail / hgweb)
9. Inverse function theorem + lemmas (detail / hgweb)
10. back to more elementary Buffer.T -- less intermediate garbage; (detail / hgweb)
11. unused; (detail / hgweb)
12. unused; (detail / hgweb)
13. more direct output of XML material -- bypass Buffer.T; (detail / hgweb)
14. clarified signature; (detail / hgweb)
15. tuned; (detail / hgweb)
16. more direct output of XML material -- bypass Buffer.T; (detail / hgweb)
17. more scalable protocol_message: use XML.body directly (Output.output hook is not required); (detail / hgweb)
18. clarified signature; (detail / hgweb)
19. tuned; (detail / hgweb)

Started by an SCM change

This run spent:

• 51 min waiting;
• 1 hr 20 min build duration;
• 2 hr 12 min total from scheduled to completion.