[isabelle] RC2: Sledgehammer blocks other functionality

[Peter Lammich]

Hi,

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.

The find theorems-panel will not come back with output until
sledgehammer has finished. The same for the find constants and print
context panels.

In my opinion, (usually long-running) background sledgehammer tasks
should have less priority than (usually short running) query-tasks, in
particular, as the normal usage pattern is most likely to start
sledgehammer in the background, and, in parallel, exploring ways to
solve the goal manually, e.g., using find-theorems to search for
suitable theorems.

--
Peter

[Makarius]

Post by Peter Lammich
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
months ago:

changeset: 60610:f52b4b0c10c4
user: wenzelm
date: Mon Jun 29 20:55:46 2015 +0200
description:
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
https://bitbucket.org/isabelle_project/isabelle-release/commits/81cbea2babd9
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.


Makarius