#2852 (May 15, 2021, 11:11:07 PM)

Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

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:

• 2 min 4 sec waiting;
• 2 hr 45 min build duration;
• 2 hr 47 min total from scheduled to completion.

• Isabelle_C