[isabelle-dev] Pink tactics
makarius at sketis.net
Wed Sep 6 21:32:30 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 , 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.
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 ...
More information about the isabelle-dev