[isabelle-dev] Remaining uses of Proof General?
makarius at sketis.net
Fri May 2 16:05:49 CEST 2014
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
More information about the isabelle-dev