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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
