#611 (Apr 25, 2018, 1:26:40 AM)

1. merged (detail / hgweb)
2. fixing more messy proofs (detail / hgweb)
3. more ambitious parallelism (in contrast to a8ee8e4884ec): pri = 1 ensures that internal proof tasks are executed before the already forked theory outline with pri = 0; (detail / hgweb)
4. eliminated pointless special case (see also a8ee8e4884ec, c4c4c2f01723); (detail / hgweb)
5. proper datatype for 8-bit characters (detail / hgweb)
6. corrected nonsense (detail / hgweb)
7. less ambitious parallelism: avoid problems with HOL-Proofs and threads=2 (congestion with many thousands futures and rather dense heap); (detail / hgweb)
8. clarified modules; (detail / hgweb)

Started by an SCM change

This run spent:

• 36 min waiting;
• 1 hr 18 min build duration;
• 1 hr 55 min total from scheduled to completion.