#517 (Jan 3, 2018, 12:50:12 AM)

1. repaired whitespace accident from 2505cabfc515 (detail / hgweb)
2. proper namespace for evaluators (detail / hgweb)
3. tuned (detail / hgweb)
4. more correct name resolving (detail / hgweb)
5. skip abstract constructors silently in datatype clauses of computations (detail / hgweb)
6. removed para about 'old_datatype' in docs (detail / hgweb)
7. old_datatype no longer exists (cf. 706b1cf7b76d); (detail / hgweb)
8. merged (detail / hgweb)
9. PIDE markup for Markdown items (which may consist of multiple paragraphs or lists); (detail / hgweb)
10. clarified terminology of "markdown_bullet"; (detail / hgweb)
11. compile (detail / hgweb)
12. updated dependencies + compile (detail / hgweb)
13. moved 'realizers' into their own theory, now that they are decupled from the old datatype construction (detail / hgweb)
14. removed 'old_datatype' command (detail / hgweb)
15. don't test 'old_datatype', which is on its way out (detail / hgweb)
16. ported inductive realizer to new datatype package (detail / hgweb)
17. removed needless theorems (detail / hgweb)
18. store high-level 'size' equations (detail / hgweb)
19. avoid call to function that may throw an exception in error message (detail / hgweb)

Started by an SCM change

This run spent:

• 9.6 sec waiting;
• 1 hr 30 min build duration;
• 1 hr 30 min total from scheduled to completion.