#1938 (Apr 19, 2023, 3:49:16 AM)

1. tuned; (detail / hgweb)
2. more operations: avoid intermediate list; (detail / hgweb)
3. discontinued somewhat pointless operation: Conjunction.intr_balanced / Conjunction.elim_balanced with single hyp performs better (e.g. see AFP/351b7b576892); (detail / hgweb)
4. update NEWS: Sortset and Termset turned out to be counter productive, Ord_List.union is much lighter; (detail / hgweb)
5. drop unused Set().ord, which is potentially inefficient due to dict_ord/dest; (detail / hgweb)
6. tuned; (detail / hgweb)
7. backout b6aa5eac0a1a; (detail / hgweb)
8. tuned; (detail / hgweb)
9. Thm.shared context: speed-up low-level inferences; (detail / hgweb)
10. tuned whitespace; (detail / hgweb)
11. backout 4a174bea55e2; (detail / hgweb)
12. Backed out changeset f34d11942ac1 (detail / hgweb)
13. backout e3fe192fa4a8; (detail / hgweb)
14. backout 61f652dd955a; (detail / hgweb)
15. Backed out changeset e3db27e3b0c6 (detail / hgweb)
16. Backed out changeset cd5d56abda10 (detail / hgweb)
17. revert b43ee37926a9 due to problems with AFP/PAPP_Impossibility; (detail / hgweb)

Started by an SCM change

This run spent:

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