[isabelle-dev] Remaining uses of Proof General?

[Makarius]

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.


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


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


 	Makarius