[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.

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