[isabelle-dev] Pink tactics

[Makarius]

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.


	Makarius