#2159 (Mar 21, 2024, 1:39:20 AM)

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

Started by an SCM change

This run spent:

• 49 min waiting;
• 2 hr 4 min build duration;
• 2 hr 53 min total from scheduled to completion.