#1610 (Dec 11, 2021, 12:50:07 AM)

1. merged (detail / hgweb)
2. more Mailman archives; (detail / hgweb)
3. more Mailman content; (detail / hgweb)
4. clarified signature; (detail / hgweb)
5. tuned metis to use map_index (detail / hgweb)
6. merged (detail / hgweb)
7. fixed HOL-TPTP (detail / hgweb)
8. tuned vars_of_iterm (detail / hgweb)
9. fixed TPTP generation of multi-arity expressions (detail / hgweb)
10. proper handling of Hilbert choice in TFX logics (detail / hgweb)
11. proper tptp_builtins (detail / hgweb)
12. reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle (detail / hgweb)
13. proper proxy for Hilbert choice in TPTP output (detail / hgweb)
14. proper polymorphism for TH1 format in Sledgehammer (detail / hgweb)
15. refactored $ite and $let configuration and added dummy_thf_reduced prover (detail / hgweb)
16. tuned TPTP file names generated by Sledgehammer (detail / hgweb)
17. tuned SMT-Lib file names generated by Mirabelle (detail / hgweb)
18. added support for higher-order SMT proof search in Sledgehammer (detail / hgweb)
19. separated FOOL from $ite/$let in TPTP output (detail / hgweb)

Started by an SCM change

This run spent:

• 5.6 sec waiting;
• 1 hr 39 min build duration;
• 1 hr 39 min total from scheduled to completion.