#5311 (Jun 9, 2024, 10:57:30 PM)

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

1. merged (detail / hgweb)
2. clarified data representation: prefer explicit type Thm_Name; (detail / hgweb)
3. more operations, following Isabelle/ML; (detail / hgweb)
4. clarified signature: more explicit operations; (detail / hgweb)
5. clarified treatment of Thm_Name.T (again, see also 8a9588ffc133); (detail / hgweb)
6. clarified operations, including exceptions; (detail / hgweb)
7. tuned: more direct Isabelle/ML; (detail / hgweb)
8. clarified modules; (detail / hgweb)
9. more accurate thm "name_hint", using Thm_Name.T; (detail / hgweb)
10. more operationsd; (detail / hgweb)
11. tuned; (detail / hgweb)
12. more robust: prefer synchronous compression (usually <= 1ms, sometimes 1..5ms); (detail / hgweb)
13. clarified signature; (detail / hgweb)
14. clarified output, following Consumer_Thread.failure; (detail / hgweb)
15. more informative exception output, with optional trace; (detail / hgweb)
16. more accurate output of Thm_Name.T wrt. facts name space; (detail / hgweb)
17. clarified signature: more operations; (detail / hgweb)
18. tuned structure; (detail / hgweb)
19. tuned; (detail / hgweb)
20. more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name; (detail / hgweb)
21. clarified signature: prefer explicit operation; (detail / hgweb)
22. clarified signature; (detail / hgweb)
23. tuned: prefer Thm_Name operations; (detail / hgweb)
24. tuned; (detail / hgweb)
25. prefer dynamic position from command transaction; (detail / hgweb)
26. tuned signature; (detail / hgweb)
27. clarified signature: more explicit preprocessing; (detail / hgweb)
28. clarified signature: separate formal context from exported theory_name; (detail / hgweb)
29. tuned signature: just one ZThm is sufficient; (detail / hgweb)

Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

1. merged (detail)
2. tuned, following Isabelle/9aa11b457c36; (detail)
3. adapted to Isabelle/718daea1cf99; (detail)
4. more accurate thm name_hint, using Thm_Name.T (see Isabelle/c2537860ccf8); (detail)
5. revert 1f139e059475 and dfa7db541b8e: no name clash of internal derivations thanks to Isabelle/8a9588ffc133; (detail)
6. adapted to Isabelle/8a9588ffc133; (detail)

Started by an SCM change

This run spent:

• 3 min 23 sec waiting;
• 5 hr 4 min build duration;
• 5 hr 8 min total from scheduled to completion.