Stream: General

Topic: Consumer thread failure: "Isabelle.command_input"

view this post on Zulip Chengsong Tan (Jul 02 2024 at 17:48):

Hi,

It seems that a certain sledgehammer call can crash the Isabelle on my computer.
The error message goes like this:

6:36:41 PM [Isabelle.command_input] [error] command_input: *** Consumer thread failure: "Isabelle.command_input"
6:36:41 PM [Isabelle.command_input] [error] command_input: *** I/O error: Socket closed

This error causes the prover process to terminate, and seems to be reproducible on my machine with the sledgehammer call on line 930 of the file "NewModifiedDirtyEvict.thy" from below (I included necessary imports):
NewModifiedDirtyEvict.thy
BasicInvariants.thy
CoherenceProperties.thy
BuggyRules.thy
Join video call.
Transposed.thy

My laptop is an Intel machine with Windows 11.
Can anyone else reproduce this error?

Last updated: Dec 21 2024 at 12:33 UTC