#2499 (Mar 21, 2024, 1:33:11 AM)

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

1. build component for cvc5-latest (ef2bc3f735df); (detail)
2. merged (detail)
3. try proof method "order" in Sledgehammer's proof reconstruction (detail)
4. added Mirabelle action "order" (detail)
5. renamed lemma antisymp_on_reflcp to antisymp_on_reflclp (detail)
6. tuned proof (detail)
7. added lemma order_reflclp_if_transp_and_asymp (detail)
8. added lemmas antisym_on_reflcl_if_asym_on and antisymp_on_reflclp_if_asymp_on (detail)
9. HOL-Library: added modulo/congruence for real numbers (detail)
10. only print schedule if relevant; (detail)
11. remove laziness: no need, and errors during initialization loop with close(); (detail)
12. more general definition of meromorphicity; Weierstraß factorisation theorem (detail)
13. always provide build_database_server option in benchmark command; (detail)
14. always check if node is defined, e.g. for exists_next operation wit empty schedule; (detail)

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

1. Multirelations_Heterogeneous: further results for convex-closure (detail)

Started by an SCM change

This run spent:

• 7.9 sec waiting;
• 11 hr build duration;
• 11 hr total from scheduled to completion.