[isabelle-dev] Pink tactics

[Makarius]

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