#1617 (Dec 20, 2021, 12:50:09 AM)

1. NEWS (detail / hgweb)
2. merged (detail / hgweb)
3. used TH1 for Leo-III in sledgehammer (detail / hgweb)
4. tuned run_sledgehammer and called it directly from Mirabelle (detail / hgweb)
5. exported Sledgehammer.launch_prover and use it in Mirabelle (detail / hgweb)
6. proper filtering inf induction rules in Mirabelle (detail / hgweb)
7. added nearly_all_facts_of_context and uniformized its usage in Sledgehammer and Mirabelle (detail / hgweb)
8. tuned ATP to use is_widely_irrelevant_const (detail / hgweb)
9. added support for initialization messages to Mirabelle (detail / hgweb)

Started by an SCM change

This run spent:

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