Email Gateway (Nov 22 2024 at 18:45): Email Gateway (Nov 22 2024 at 18:45):From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
Hi all,
I've noticed recently that invoking "auto" with many (e.g. 50) premises (using "using") can sometimes lead to an "Interrupt_Breakdown" exception. I've enclosed an example below -- if you wait a few minutes with Isabelle2024, you might be able to reproduce the exception.
My trouble is that Sledgehammer invokes "auto" as part of its preplay. I'm tempted to simply catch the exception and consider this case a failure (analogous to timing out), but something tells me that catching "Interrupt_Breakdown" might be taboo. Any hints on what I should do?
The issue is getting more pressing because I'm experimenting with an alternative mode of Sledgehammer that doesn't invoke ATPs and directly relies on Isabelle proof methods as the engine for proof search (think: "try0" + relevance filtering). Then I run into the problem so often -- and sometimes after a few seconds only -- that the whole new mode becomes unusable.
Best,
Jasmin
theory Scratch
imports Main
begin
lemma "2 + 2 = 5"
(*
sledgehammer[auto, debug, slices = 1, max_facts = 100, timeout = 10, mepo]
*)
using semiring_norm(89) semiring_norm(88) semiring_norm(86) semiring_norm(84) semiring_norm(85) semiring_norm(83) numeral_plus_numeral add_numeral_left num.exhaust numeral_Bit0 verit_eq_simplify(9) Let_numeral numeral_eq_iff semiring_norm(87) verit_eq_simplify(8) semiring_norm(90) semiring_norm(6) semiring_norm(2) semiring_norm(7) semiring_norm(9) semiring_norm(3) semiring_norm(4) semiring_norm(5) semiring_norm(8) semiring_norm(10) add_One_commute is_num_normalize(1) semiring_norm(82) verit_eq_simplify(10) verit_eq_simplify(12) verit_eq_simplify(14) add_right_cancel add_left_cancel dbl_inc_simps(5) sqr.simps(3) sub_num_simps(5) dbl_simps(5) one_plus_numeral numeral_plus_one one_add_one Let_1 numeral_eq_one_iff one_eq_numeral_iff sub_num_simps(6) sub_num_simps(9) sub_num_simps(8) dbl_simps(3) dbl_inc_simps(3) one_reorient dbl_inc_def numerals(1) sqr.simps(2) sqr.simps(1) one_plus_numeral_commute dbl_def numeral_One nat_1_add_1 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 add.left_commute add_left_imp_eq add_right_imp_eq numeral_Bit1 sub_num_simps(7) sub_num_simps(4) dbl_simps(4) sub_num_simps(3) add_neg_numeral_special(4) neg_equal_iff_equal add.inverse_inverse verit_minus_simplify(4) minus_add_distrib minus_add_cancel add_minus_cancel Let_neg_numeral neg_numeral_eq_iff dbl_dec_simps(3) add_neg_numeral_simps(3) dbl_simps(1) dbl_inc_simps(4) dbl_dec_simps(5) numeral_eq_neg_one_iff neg_one_eq_numeral_iff semiring_norm(167) add_neg_numeral_simps(1) add_neg_numeral_simps(2) semiring_norm(165) semiring_norm(166) dbl_inc_simps(1) dbl_dec_simps(1) add_neg_numeral_special(9) add_neg_numeral_special(1) add_neg_numeral_special(2) add_neg_numeral_special(3) sub_num_simps(2)
apply auto
--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html
Last updated: Jan 04 2025 at 20:18 UTC