[isabelle-dev] Pink tactics
Makarius
makarius at sketis.net
Thu Oct 12 22:13:21 CEST 2023
On 30/08/2023 13:21, Makarius wrote:
> On 28/08/2023 17:31, Jasmin Blanchette wrote:
>>
>> 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.
>>
>> 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.
>
> This Interrupt is probably a resource problem of the ML runtime system,
> presumably stack overflow.
>
> Unlike the Java/VM we don't see the difference of an external event and such
> an internal event of the Poly/ML RTS.
>
> I will make some further experiments to see if we can somewhat enhance the
> concept of Isabelle/ML thread, without having to ask David Matthews for
> changes in Poly/ML.
It has required a few weeks longer than expected, but now we have quite
different interrupt handling in Isabelle/ML.
Your isolated example works now like this in Isabelle/280a228dc2f1:
theory Scratch
imports Main
begin
lemma "1 + 2 = 4"
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)
(*exception Interrupt_Breakdown raised*)
oops
end
Note that the proper way to distinguish interrupts is Exn.is_interrupt,
Exn.is_interrupt_proper, Exn.is_interrupt_breakdown.
Some fine points might still be open, and to be reconsidered.
Makarius
More information about the isabelle-dev
mailing list