#2079 (Dec 20, 2023, 3:59:53 AM)

1. merged (detail / hgweb)
2. use strict Global_Theory.register_proofs as checkpoint for stored zproof, and thus reduce current zboxes; (detail / hgweb)
3. clarified signature; (detail / hgweb)
4. omit pointless future: proof terms are built sequentially; (detail / hgweb)
5. omit unclear / inaccurate renaming; (detail / hgweb)
6. more normalization: re-use Thm.solve_constraints as important checkpoint for results, notably Global_Theory.name_thm; (detail / hgweb)
7. more robust: avoid assumption about Context.certificate_theory; (detail / hgweb)
8. tuned; (detail / hgweb)
9. clarified pro-forma proof: no zboxes here (partially revert 686b7b14d041); (detail / hgweb)
10. tuned; (detail / hgweb)
11. tuned; (detail / hgweb)
12. more normalization; (detail / hgweb)
13. less ambitious normalization: term abstractions over terms and proofs, but not proofs over proofs (which may be large); (detail / hgweb)
14. tuned; (detail / hgweb)
15. more thorough beta contraction, following Envir.norm_term; (detail / hgweb)
16. tuned, following Envir.norm_term; (detail / hgweb)
17. more operations; (detail / hgweb)
18. merged (detail / hgweb)
19. unused lemma (detail / hgweb)
20. restore benchmark requirement heaps properly; (detail / hgweb)
21. continue build while waiting for updated schedule; (detail / hgweb)
22. clarified signature; (detail / hgweb)
23. added start-up sequence for benchmark with requirements; (detail / hgweb)
24. use single-threaded session build as benchmark (using ZF-Constructible); (detail / hgweb)
25. separate build processes for scheduler and scheduled; (detail / hgweb)
26. add delay and limit options for when schedule is considered outdated; (detail / hgweb)
27. proper closing order; (detail / hgweb)
28. read serial for schedules (amending 2039f360); (detail / hgweb)

Started by an SCM change

This run spent:

• 3 hr 9 min waiting;
• 2 hr 4 min build duration;
• 5 hr 14 min total from scheduled to completion.