#2126 (Feb 15, 2024, 2:28:54 AM)

1. merged (detail / hgweb)
2. prefer physical processors (see also 4b014e6c1dfe and 26a43785590b); (detail / hgweb)
3. more robust: avoid occasional problems reading this special file (e.g. SSH.Local or "lxcisa0"); (detail / hgweb)
4. more robust default; (detail / hgweb)
5. more accurate, notably on lxbroy10 and vmnipkow9; (detail / hgweb)
6. clarified num_processors: follow Poly/ML (with its inaccuracies); (detail / hgweb)
7. clarified modules, following Isabelle/ML; (detail / hgweb)
8. clarified signature; (detail / hgweb)
9. tuned comments; (detail / hgweb)
10. merged (detail / hgweb)
11. the syntax of Lebesgue integrals (LINT, LBINT, ∫, etc.) now requires parentheses (detail / hgweb)
12. merged (detail / hgweb)
13. A few lemmas brought in from AFP entries (detail / hgweb)
14. merged (detail / hgweb)
15. made destructor-view tactic more robust (by Jan van Brügge) (detail / hgweb)

Started by an SCM change

This run spent:

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