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 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




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