#1974 (Jun 24, 2023, 12:50:10 AM)

1. clarified signature: prefer explicit combinator; (detail / hgweb)
2. unused; (detail / hgweb)
3. restore heaps from database, which takes precedence over file-system; (detail / hgweb)
4. tuned; (detail / hgweb)
5. more operations; (detail / hgweb)
6. tuned; (detail / hgweb)
7. more robust try-finally; (detail / hgweb)
8. tuned signature; (detail / hgweb)
9. proper clean_entry; (detail / hgweb)
10. afford larger build_database_slice for better compression (HOL: 1 slice, HOL-Proofs: multiple slices for testing); (detail / hgweb)
11. prefer system option; (detail / hgweb)
12. clarified signature: more explicit class SQL.Data; (detail / hgweb)
13. proper ML_Heap.clean_entry; (detail / hgweb)
14. tuned signature; (detail / hgweb)
15. tuned; (detail / hgweb)
16. store heaps within database server; (detail / hgweb)
17. tuned signature; (detail / hgweb)
18. clarified modules; (detail / hgweb)
19. tuned signature; (detail / hgweb)
20. clarified modules; (detail / hgweb)
21. clarified modules; (detail / hgweb)

Started by an SCM change

This run spent:

• 9.8 sec waiting;
• 2 hr 3 min build duration;
• 2 hr 3 min total from scheduled to completion.