On 03/05/14 00:05, Makarius wrote:
On Tue, 29 Apr 2014, Thomas Sewell wrote:
I tried an adjustment a while ago in which I had the goal state print
incrementally. Even if some of the subgoals took a while to print,
you'd see the line with "goal (12 subgoals)" immediately, and then
the subgoals as they were formatted. The short summary is that this
helped a little sometimes, but I often still saw an empty Output
panel for seconds after moving the cursor to a line that the
continuous checker had already processed.
I strongly suspect that the print request was waiting in a queue
somewhere. The system would become responsive again once it finished
doing something else.
That is the normal future task farm, with its restricted worker thread
pool. All PIDE execution works via some Future.fork, with different
priorities in the queue. Proof tasks have low priority, print tasks
have high priority. Once a task is running on some thread, it
continues and cannot be preempted by newer tasks with higher priority.
The basic assumption is that each proof task does not run too long,
and if it does it is something to be improved in the application to
make it more smooth. In contrast, Proof General makes it more easy to
produce huge and heavy proof scripts that can be hardly handled by
anyone else later.
Right. That seems to be the assumption that's being violated in the few
cases where people are still keen on ProofGeneral, for instance, in
Andreas' big complicated tactic applications.
The case where I get into trouble is in implementing a package-lite. I
put together a collection of tactics or computations in ML blocks and
execute them at some point in a theory via setup or ML. It's a bit like
setting up a proper package and invoking it, but without the implied
robustness or generality. Some of these can run for a minute or longer.
They're the kind of computations that users might want to control.
With regard to the future task farm: This is pretty much what I'd
expected. So we see a delay if all the available threads are executing
tasks that take a while and are not the current print task. Adding more
threads reduces the chance of this happening, but not much. The higher
priority for print tasks means the delay will end as soon as any thread
becomes available, so the more threads the faster on average that will
happen, but without guarantees.
Let me make a proposal. I think that various users would appreciate it
if one of the worker threads was reserved for print jobs caused by
moving the cursor (highest priority tasks) and their dependencies
(assuming more than one worker thread). That would hopefully make it
easier to control the delay. If the user is cautious with moving the
cursor and if enough proof dependencies have been processed, the system
*should* be as responsive as PG. The delay would also be mostly
unaffected by the proof task runtime, only the print task runtimes,
which might be easier for an advanced user to manage.
Users running on batteries might also want a mode that restricts all
threads to the behaviour above.
As always, I have no idea how difficult that would be.
On incremental printing: it's easy to implement by generalising a
couple of the relevant Pretty operations to produce a Seq.seq
internally rather than a list.
That would probably violate some implicit assumptions about print
modes, which are a slightly odd intrusion into the purity of Pretty.T.
What was the reason for incremental printing anyway? Just performance
for huge goal states? There are other bottle-necks concerning that,
and if goals really do get that big one should think about other ways
to expose them, not by "printing" in the old-fashioned way.
Incrementality might have other reasons and actual benefits. In the
early years of PIDE I had more ambitions for that, but it caused so
many additional problems in the document model and the GUI that I
removed most of it for the sake of delivering something that is
sufficiently stable to be usable in practice.
The reason for the experiment was that I was fixing some proofs
somewhere, I forget where, which had relatively fast tactics executing
on large, slow-to-print goals. I was probably in a context where Simpl
was loaded, where printing is slower than usual (probably the
print/parse translations, I've had a look and got nowhere.)
It occurred to me that I could debug some of my mistakes faster if I
just knew whether or not the tactic I'd typed had solved a goal, and
many more if I just saw the first goal. But the time saved is probably
lost again adjusting the goals limit, and it's annoying to do by hand.
Incremental output seemed like a good idea.
It looked promising initially, but then became really annoying,
because Isabelle/jEdit or PIDE resets the Output buffer each time it
gets more to display. So if you scroll down to look for something,
you get scrolled back up for each time a subgoal prints, which can
give the sensation that the editor is fighting you.
There is a deeper conceptual problem here. Several independent
entities want to update content of some GUI component: output window,
tree view etc. This requires a "merge" of these change of the GUI
state, but that is usually only done by a hard reset on one side,
ignoring the other side. You can see that in jEdit's SideKick tree
view, Isabelle/jEdit's Output dockable with scrollbar and folds, or
even just in a plain Terminal with the scrollbar.
Sure. I was surprised that I got the incremental output working at all
without any Scala changes.
I wasn't for a moment implying there wasn't a good reason for this
behaviour or that doing this properly wouldn't be real work.
In a no-particular-urgency sense, better support for incremental output
might be a good idea. As I said above, the delay length seen by the user
is affected by the longest task times, including printing. If
Isabelle/jEdit requested printed goals one at a time, that would
probably decrease the longest task time quite a bit, especially the
longest high-priority task time. I guess I had envisaged the sort of
thing that facebook and slashdot do, where there's a "(10 more stories)"
marker at the bottom of the news feed which prompts the fetching of more
content as soon as it appears visually. I have no idea if that's
workable in jEdit or not.
The other argument for better support for incremental output is in
implementing the kind of package-lite I mentioned before. Like Andreas,
I tend to debug these by tracing a lot of data, and searching in the
output for suspect events. It's a little annoying that Isabelle/jEdit
doesn't like having its output panel searched, and keeps resetting the
cursor if there's a constant stream of data being printed.
I guess I could work around all of this myself, by inventing a language
of commands that create a Future-forked stream of trace output, and some
search functions for it. Maybe I should just do that.
Cheers,
Thomas.
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
