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.
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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and