isabelle

Meaning of isabelle clarsimp/fastforce's background turning light red


Image to fastforce with light red background

Image of clarsimp with light red background

This keeps happening in my proofs. As you can see, the proof goal window is blank. What does the light red background on fastforce mean? The same happends with clarsimp.

It seems to hang forever once that happens.


Solution

  • Is there any additional output when you position the caret on the fastforce call? If yes, that will probably tell you what the problem is.

    But my guess is that there is none, and in that case the problem is usually that the fastforce call diverges and eventually runs out of memory and crashes. That is usually the cause of lines in Isabelle being printed in red like this. This can have a number of reasons: excessive backtracking, a simplifier loop, etc.