#970 (Jul 27, 2019, 12:50:09 AM)

1. finalize proofs earlier to reduce memory requirement; (detail / hgweb)
2. proper proof_serial; (detail / hgweb)
3. more explicit type proof_serial; (detail / hgweb)
4. defer rew_proof on unnamed PThm node as open_proof operation: significant performance improvement;
   misc tuning and clarification; (detail / hgweb)
5. more accurate proof definitions (PThm nodes); (detail / hgweb)
6. avoid duplicate Thm.name_derivation on unnamed PThm nodes ("simps" vs. "case_eqns" and "recursor_eqns"); (detail / hgweb)
7. prefer local counter; (detail / hgweb)
8. more accurate proof export; (detail / hgweb)
9. clarified syntax; (detail / hgweb)
10. tuned; (detail / hgweb)
11. more thorough clean_proof; (detail / hgweb)
12. clarified modules; (detail / hgweb)

Started by an SCM change

This run spent:

• 7.8 sec waiting;
• 1 hr 18 min build duration;
• 1 hr 18 min total from scheduled to completion.