#2096 (Jan 11, 2024, 2:32:04 AM)

1. merged (detail / hgweb)
2. clarified signature; (detail / hgweb)
3. clarified signature; (detail / hgweb)
4. tuned signature; (detail / hgweb)
5. tuned; (detail / hgweb)
6. clarified test: no exception yet; (detail / hgweb)
7. tuned; (detail / hgweb)
8. tuned; (detail / hgweb)
9. tuned signature: more direct operations; (detail / hgweb)
10. clarified signature; (detail / hgweb)
11. clarified signature: more direct operations; (detail / hgweb)
12. tuned signature; (detail / hgweb)
13. tuned; (detail / hgweb)
14. minor performance tuning, for important special case where consts are already expanded (e.g. re-certification within proof procedure); (detail / hgweb)
15. tuned whitespace; (detail / hgweb)
16. more robust: certify types uniformly (see also 62b75508eb66); (detail / hgweb)
17. tuned; (detail / hgweb)
18. clarified signature; (detail / hgweb)
19. clarified signature: avoid redundant Term.maxidx_of_term; (detail / hgweb)
20. proper check of result from Soft_Type_System.global_purge (amending b2bedb022a75); (detail / hgweb)
21. misc tuning and clarification: prefer Same.operation; (detail / hgweb)
22. clarified signature; (detail / hgweb)
23. tuned names; (detail / hgweb)
24. clarified signature; (detail / hgweb)
25. tuned whitespace; (detail / hgweb)
26. clarified modules;
    minor performance tuning; (detail / hgweb)
27. clarified signature; (detail / hgweb)
28. added and removed lemmas (detail / hgweb)
29. proper SMTP session: set envelope sender address correctly; (detail / hgweb)

Started by an SCM change

This run spent:

• 1 hr 42 min waiting;
• 2 hr 1 min build duration;
• 3 hr 43 min total from scheduled to completion.