# [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"
numeral_eq_one_iff one_eq_numeral_iff semiring_norm(85) semiring_norm(83)
one_plus_numeral_commute Let_numeral numeral_eq_iff semiring_norm(87)
is_num_normalize(1) semiring_norm(82) dbl_simps(3) verit_eq_simplify(8) Let_1
dbl_simps(1) neg_one_eq_numeral_iff numeral_eq_neg_one_iff semiring_norm(167)
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
(*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

```