Re: [isabelle] RC5: Running sledgehammer still blocks output

On Tue, 19 May 2015, Peter Lammich wrote:

When sledgehammer runs in the background (invoked via the panel),
the output of commands that I enter is not displayed in the output
panel, until sledgehammer terminates.

A very annoying behaviour, if you want to continue exploring your proof
while sledgehammer tries to find a "shortcut" for you.

-- Peter

p.s. I also reported this problem for Isabelle2014.

Can you be more specific about the situation, especially the number of cores and ML threads, and sledgehammer provers?

For Isabelle2015 the scheduling has changed, to address that particular shortcoming of earlier versions. It now works quite differently from Isabelle2014.

In the tests I've made myself, it did work as intended. It was also occasionally discussed on various Isabelle2015-RC threads on the mailing list, where I called explicitly to test it thoroughly and produce tangible problem reports.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.