#1640 (Feb 3, 2022, 12:50:07 AM)

1. more precise slicing computation and output when not enough lemmas are available (e.g. with the 'only' syntax 'sledgehammer (lem1 lem2 lem3)') (detail / hgweb)
2. enable induction in one of Zipperposition's slices (detail / hgweb)
3. made sorting of Vampire facts more robust in the face of names that deviate from the standard scheme (detail / hgweb)
4. robustly handle empty proof blocks in Isar proof output (detail / hgweb)
5. propagate right result when enough proofs have been found (detail / hgweb)
6. correctly parse E proofs that assume '=' and '!=' bind more tightly than connectives (detail / hgweb)
7. don't lose error messages (detail / hgweb)
8. don't pass --auto-schedule to E indiscriminately -- use it instead of 'auto' in one slice (detail / hgweb)
9. careful with partial applications (detail / hgweb)
10. don't perform preplaying steps if preplaying is disabled (detail / hgweb)
11. adjust TPTP THF parser to give priority to @ over other operators, to parse Ehoh proofs (detail / hgweb)
12. tuned punctuation (detail / hgweb)
13. handle TPTP '!=' more gracefully in Isar proof reconstruction (detail / hgweb)
14. guard against duplicate lines in Zipperposition proofs (detail / hgweb)

Started by an SCM change

This run spent:

• 6 sec waiting;
• 1 hr 37 min build duration;
• 1 hr 37 min total from scheduled to completion.