[isabelle-dev] Remaining uses of Proof General?

[Makarius]

On Mon, 28 Apr 2014, Peter Lammich wrote:

> 1. I cannot really control what Isabelle/Jedit processes when, and it
>    invests computation power on the meaningless parts of the file
>    directly after the point where I am editing. I'm not even convinced
>    that it is the right approach to let Isabelle/jEdit's heuristics
>    decide when and what it processes, and make user intervention
>    impossible at first place

Isabelle/jEdit is indeed about giving up manual control: the system is 
moving so fast, that you cannot handle every part of it yourself. It is 
like a TGV: you buy a ticket and sit comfortably, while the machine is 
moving on its own.

There is nothing really revolutionary about that.  Any of the major IDEs 
work in a similar manner.  I don't claim any orginality on ideas here. 
Last year at ITP Rennes, it was very interesting for me to see that the 
MSR guys are imitating a similar IDE model in Dafny, although that is a 
quite different prover and a quite different platform.

Hopefully the ITP community will make further moves towards serious IDEs, 
not just boring copy paste from one buffer into another (where a 
sub-ordinate process consumes that).


> (Or even worse, force the user into
>  workarounds like inserting semicolons or "end"s behind the current
>  editing point, which seems to be common practice among Isabelle/jEdit
>  users)

I don't know much about common practice.  Maybe that is just what people 
at TUM do occasionally.  There is the general problem here that people are 
often too shy or just not capable to explain what they are doing.  It is 
also difficult to describe verbally how interaction is done, but videos 
sometimes help.


> 2. In PG, when the processed region reaches the end of a theory file, I
>    can be pretty sure that everything is fine with this theory. In
>    Isabelle/jEdit, I have to scan the theory status panel manually for
>    remaining red or pink bars, which is very inconvenient for large
>    projects with hundreds of files.

I can't follow this argument.  The Theories panel is one of the things 
that is lacking in Proof General.  I cannot imagine anymore how big 
libraries were managed in the old regime.

What is indeed missing is the infamous "wrap-up" of a session, that I have 
explained on the Isabelle mailing lists many times, like what isabelle 
build does in batch mode.  That is still not there, since the Theories 
panel already does a fairly good job, and doing it formally in the IDE 
document model is not completely trivial: such things need to be done in 
real time on the spot for large libraries.


> Moreover, I find it a bit scary that severe errors related to 
> Isabelle/jEdit's document processing model (cf. 
> https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-November/msg00170.html) 
> can go undiscovered for several month, although most Isabelle users are 
> on Isabelle/jEdit these days. I ask myself: Have they got so used to 
> strange behaviours of the IDE that they do not realize severe errors any 
> more?

That was a severe problem, and I can guess only half of the reasons how 
this came about.  I would not use that as an argument againts 
Isabelle/jEdit, though, since the problem was caused by some unclear bit 
of the implementation that had to care about standard mode (PIDE) and 
legacy mode (TTY / Proof General) at the same time. If the latter had been 
discontinued 2 years ago, we would all be in better shape today.


 	Makarius