Email Gateway (Aug 22 2022 at 12:45): Email Gateway (Aug 22 2022 at 12:45):From: Peter Lammich <lammich@in.tum.de>
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.
Email Gateway (Aug 22 2022 at 12:46):From: Makarius <makarius@sketis.net>
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:
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:
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
Last updated: Apr 24 2024 at 08:20 UTC