<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"></head><body style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div dir="auto" style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div dir="auto" style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;">Dear colleagues,<div><br></div><div>Sledgehammer invokes "simp" as part of proof reconstruction. I'm currently adding a mode, inspired by Magnushammer [1], where the simplifier is applied directly, without relying on an automatic theorem prover. However, for this to work, I need to call "by (simp add: ...)" with a timeout, where "..." is a potentially long list of lemmas that might lead to nontermination.</div><div><br></div><div>What happens quite often is that the "simp" call (actually, a call to "Goal.prove" in ML) throws "Interrupt". This is propagated through Sledgehammer and leads to the "sledgehammer" command to stop working and turn pink.</div><div><br></div><div>The issue is not restricted to "simp". "using ... by auto" can also lead to the same behavior.</div><div><br></div><div>I can sometimes reproduce the issue without Sledgehammer, using repository version Isabelle/10d85056cf3b. I write "sometimes" because it's clearly nondeterministic. Here's a .thy file:</div><div><br></div><div><div>theory Scratch</div><div> imports Main</div><div>begin</div><div><br></div><div><div>lemma "1 + 2 = 4"</div><div> apply (simp add: one_add_one numeral_plus_one one_plus_numeral numeral_eq_one_iff one_eq_numeral_iff semiring_norm(85) semiring_norm(83) numeral_plus_numeral add_numeral_left numeral_One numeral_Bit0 one_plus_numeral_commute Let_numeral numeral_eq_iff semiring_norm(87) semiring_norm(6) semiring_norm(2) numerals(1) nat_1_add_1 add_One_commute is_num_normalize(1) semiring_norm(82) dbl_simps(3) verit_eq_simplify(8) Let_1 add_right_cancel add_left_cancel verit_eq_simplify(10) add_neg_numeral_special(9) dbl_simps(5) neg_equal_iff_equal add.inverse_inverse verit_minus_simplify(4) neg_numeral_eq_iff Let_neg_numeral minus_add_distrib minus_add_cancel add_minus_cancel add_neg_numeral_simps(3) dbl_simps(1) neg_one_eq_numeral_iff numeral_eq_neg_one_iff semiring_norm(167) dbl_simps(4) add.inverse_distrib_swap group_cancel.neg1 minus_equation_iff equation_minus_iff verit_negate_coefficient(3) neg_numeral_neq_numeral numeral_neq_neg_numeral is_num_normalize(8) one_neq_neg_one numeral_neq_neg_one one_neq_neg_numeral dbl_def uminus_numeral_One ab_semigroup_add_class.add_ac(1) add_mono_thms_linordered_semiring(4) group_cancel.add1 group_cancel.add2 add.assoc add.left_cancel add.right_cancel add.commute)</div></div></div><div><br></div><div>end</div><div><br></div><div>The enclosed screenshots show what happens. If there's a way to call a tactic with a timeout as a blackbox, without risk of triggering fatal errors that lead Sledgehammer to entirely fail (i.e., become pink), I would be a taker.</div><div><div><br></div><div>Best,</div><div>Jasmin</div><div><br></div><div>[1] https://arxiv.org/abs/2303.04488</div><div><br></div><div><div>
<meta charset="UTF-8"><div dir="auto" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div>--<br>Prof. Dr. Jasmin Blanchette<br>Chair of Theoretical Computer Science and Theorem Proving<br>Ludwig-Maximilians-Universität München<br>Oettingenstr. 67, 80538 München, Germany<br>Tel.: +49 (0)89 2180 9337<br>Email: jasmin.blanchette@ifi.lmu.de<br>Web: <a href="https://www.tcs.ifi.lmu.de/">https://www.tcs.ifi.lmu.de/</a></div><div><br></div><div><img src="cid:7021019D-8F6A-45FF-AE05-BA94C82C0951" alt="Screenshot 2023-08-28 at 17.22.13.png"></div></div></div></div></div><br></div><div dir="auto" style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><img src="cid:16330005-DC80-496B-8AB5-05E13730A7F6" alt="Screenshot 2023-08-28 at 17.21.56.png"></div></div></body></html>