#1952 (May 10, 2023, 2:57:34 AM)

1. backed out changeset 6c2494750a4e: it hardly makes a difference for heap size, but crashes arm64_32-darwin for unknown reasons; (detail / hgweb)
2. enforce rebuild of Isabelle/ML + Isabelle/Scala; (detail / hgweb)
3. updated to jdk-17.0.7; (detail / hgweb)
4. minor performance tuning (see also f906f7f83dae and b23c42b9f78a); (detail / hgweb)
5. performance tuning: cached non-persistent Parser.gram reduces heap size by approx. 1-4%; (detail / hgweb)
6. more operations; (detail / hgweb)
7. tuned: more readable ML; (detail / hgweb)
8. tuned; (detail / hgweb)
9. backed out changeset 4660181c83c9: remove rather pointless timing (1..50ms); (detail / hgweb)
10. maintain dynamic position where values are created (again, amending afa6117bace4); (detail / hgweb)
11. more robust: publish token only after assignment of result; (detail / hgweb)
12. tuned comments; (detail / hgweb)
13. clarified signature; (detail / hgweb)
14. merged (detail / hgweb)
15. tuned signature; (detail / hgweb)
16. support for cached evaluation via weak_ref; (detail / hgweb)
17. optional timing; (detail / hgweb)
18. more informative trace of context allocations; (detail / hgweb)
19. tuned; (detail / hgweb)
20. tuned internal structure; (detail / hgweb)
21. tuned; (detail / hgweb)
22. tuned whitespace; (detail / hgweb)

Started by an SCM change

This run spent:

• 2 hr 7 min waiting;
• 2 hr 1 min build duration;
• 4 hr 8 min total from scheduled to completion.