#1465 (May 16, 2021, 1:56:36 AM)

1. merged (detail / hgweb)
2. proper build of required session images vs. build with Mirabelle presentation; (detail / hgweb)
3. reactive "sledgehammer"; (detail / hgweb)
4. reactive "sledgehammer_filter": statically correct, but untested (no proof_file); (detail / hgweb)
5. clarified command-line; (detail / hgweb)
6. clarified signature;
   supporess empty results; (detail / hgweb)
7. clarified signature; (detail / hgweb)
8. clarified log content; (detail / hgweb)
9. reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; (detail / hgweb)
10. tuned; (detail / hgweb)
11. unused; (detail / hgweb)
12. unused (see 8ffc607c345d); (detail / hgweb)
13. clarified signature: provide access to previous state; (detail / hgweb)
14. clarified signature (see Scala version); (detail / hgweb)
15. tuned signature; (detail / hgweb)
16. avoid duplicate loading of ML file; (detail / hgweb)

Started by an SCM change

This run spent:

• 1 hr 6 min waiting;
• 1 hr 27 min build duration;
• 2 hr 33 min total from scheduled to completion.