#1894 (Feb 20, 2023, 12:50:07 AM)

1. merged (detail / hgweb)
2. proper Nodes.init (amending 9b35c1171d9a); (detail / hgweb)
3. unused; (detail / hgweb)
4. tuned; (detail / hgweb)
5. clarified signature defaults; (detail / hgweb)
6. clarified types: support a variety of Build_Job instances; (detail / hgweb)
7. clarified signature: more explicit synchronized operations; (detail / hgweb)
8. clarified signature: more explicit synchronized operations; (detail / hgweb)
9. clarified modules (again);
   clarified signature: idempotent "finish" operation, analogous to "join"; (detail / hgweb)
10. clarified signature: more explicit synchronized operations; (detail / hgweb)
11. clarified signature: more explicit synchronized operations; (detail / hgweb)
12. more robust: first register job, then start job; (detail / hgweb)
13. clarified signature: proper scope of synchronized operation; (detail / hgweb)
14. proper synchronized access to mutable state, to support concurrency eventually; (detail / hgweb)
15. tuned signature: explicit marker for mutable global state; (detail / hgweb)
16. tuned; (detail / hgweb)
17. more robust; (detail / hgweb)
18. clarified signature; (detail / hgweb)
19. clarified modules; (detail / hgweb)
20. merged (detail / hgweb)
21. Tidied some really messy proofs (detail / hgweb)
22. added lemmas asymp_not_liftable_to_multpHO and asymp_multpHO (detail / hgweb)

Started by an SCM change

This run spent:

• 5.7 sec waiting;
• 1 hr 53 min build duration;
• 1 hr 53 min total from scheduled to completion.