[isabelle-dev] Remaining uses of Proof General?

[Thomas Sewell]

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.