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.


isabelle-dev mailing list

Reply via email to