Email Gateway (Aug 28 2023 at 15:31): Email Gateway (Aug 28 2023 at 15:31):From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
Dear colleagues,
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.
The issue is not restricted to "simp". "using ... by auto" can also lead to the same behavior.
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:
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)
end
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.
Best,
Jasmin
[1] https://arxiv.org/abs/2303.04488
Screenshot 2023-08-28 at 17.22.13.png
Screenshot 2023-08-28 at 17.21.56.png
Email Gateway (Aug 30 2023 at 11:22):From: Makarius <makarius@sketis.net>
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.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Sep 06 2023 at 19:33):From: Makarius <makarius@sketis.net>
I got distracted elsewhere, especially for the release.
Nonetheless, I have started to revisit and rethink the management of
Isabelle/ML threads. Traces of that process are already in
Isabelle/47d0c333d155 (and before).
In the next 1-2 days, I will be busy again elsewhere. Stay tuned ...
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Oct 12 2023 at 20:13):From: Makarius <makarius@sketis.net>
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
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Apr 28 2024 at 04:17 UTC