Re: [isabelle] RC2: Sledgehammer blocks other functionality
On Mon, 1 Feb 2016, Peter Lammich wrote:
a running sledgehammer instance does no longer block the output window
(including goal state) [as it did in Isabelle2015], however, it still
blocks the query-panels.
There should be no difference in this respect. All short-running
query-like operations are treated uniformly, see also this change from 7
date: Mon Jun 29 20:55:46 2015 +0200
improved scheduling for urgent tasks, using farm of replacement threads
(may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
There is also this NEWS entry from that time:
* Improved scheduling for urgent print tasks (e.g. command state output,
interactive queries) wrt. long-running background tasks.
Here is a proof that long-running tasks may even block the update of the
State panel (which is just another query in the background):
(*block worker threads with very long-running tasks*)
ML_val "(1 upto 20) |> Par_List.map (fn _ => OS.Process.sleep (seconds 1000.0))"
After this command is forked, just move around already processed theories
and try to get a State panel update -- nothing happens.
I have now amended this in
by changing the NEWS:
* Slightly improved scheduling for urgent print tasks (e.g. command
state output, interactive queries) wrt. long-running background tasks.
The change log entry explains the more fundamental problem behind it. This
means the attempt to improve the situation last summer did not work out:
more substantial changes in PIDE document execution are required.
With proper testing and tangible feedback on time, it could have been part
of Isabelle2016. Now it is (again) postponed to a later release.
This archive was generated by a fusion of
Pipermail (Mailman edition) and