Build #90 (Feb 6, 2022, 12:14:00 AM)

1. tuned output syntax: Hoare triples are now blocks (detail)
2. tuned output syntax: INV and VAR are now blocks (detail)
3. more precise slicing computation and output when not enough lemmas are available (e.g. with the 'only' syntax 'sledgehammer (lem1 lem2 lem3)') (detail)
4. enable induction in one of Zipperposition's slices (detail)
5. made sorting of Vampire facts more robust in the face of names that deviate from the standard scheme (detail)
6. robustly handle empty proof blocks in Isar proof output (detail)
7. propagate right result when enough proofs have been found (detail)
8. correctly parse E proofs that assume '=' and '!=' bind more tightly than connectives (detail)
9. don't lose error messages (detail)
10. don't pass --auto-schedule to E indiscriminately -- use it instead of 'auto' in one slice (detail)
11. careful with partial applications (detail)
12. don't perform preplaying steps if preplaying is disabled (detail)
13. adjust TPTP THF parser to give priority to @ over other operators, to parse Ehoh proofs (detail)
14. tuned punctuation (detail)
15. handle TPTP '!=' more gracefully in Isar proof reconstruction (detail)
16. guard against duplicate lines in Zipperposition proofs (detail)
17. tuning (detail)
18. tuned NEWS (detail)
19. compile HOL-TPTP (detail)
20. compile Metis_Examples (detail)
21. more NEWS (detail)
22. compile mirabelle (detail)
23. tweaked Auto Sledgehammer's behavior and output (detail)
24. updated NEWS (detail)
25. removed experimental prover z3_tptp (detail)
26. print more verbose information (detail)
27. run all installed provers by default (detail)
28. update slice options centrally (detail)
29. further work on new Sledgehammer slicing (detail)
30. tweaked verbose output (detail)
31. tweak padding of prover slice schedule to include all provers (detail)
32. implemented 'max_proofs' mechanism (detail)
33. document new option 'max_proofs' (detail)
34. crude implementation of centralized slicing (detail)
35. removed obscure E option (detail)
36. take 'induction_rules' into consideration, as well as 'max_facts' even when 'only' is set (detail)
37. rationalize slicing format (detail)
38. thread slices through (detail)
39. simplified 'best_slice' data structure and made minor changes to slices (detail)
40. changed logic of 'slice' option to 'slices' (detail)
41. updated documentation of 'slice' (now 'slices') option (detail)
42. revised Sledgehammer documentation (detail)
43. rationalized output for forthcoming slicing model (detail)
44. use same default for FO and HO provers w.r.t. induction principles, based on evaluation -- this also simplifies the code (detail)
45. disable slicing within ATP module (in preparation for refactoring) (detail)
46. disable slicing within SMT (in preparation for factoring it out) (detail)
47. generalized the 'slice' option towards more flexible slicing (detail)
48. tuned -- fewer warnings; (detail)

1. Strong soundness. (detail)
2. Strong soundness. (detail)
3. Fix LaTeX issue. (detail)
4. Qualification required(?) (detail)
5. merged (detail)
6. more variants of the algorithm (detail)
7. Added funding acknowledgments.
   Fixed broken BibTeX citation. (detail)
8. Strong completeness for PAL systems. (detail)

Started by timer

This run spent:

• 15 ms waiting;
• 19 hr build duration;
• 19 hr total from scheduled to completion.