[isabelle-dev] Remaining uses of Proof General?

[Peter Lammich]

I'm still a regular user of PG. From time to time, I test
Isabelle/jEdit, and my reasons for switching back to PG are somewhat
similar to what Andreas reported. My main problems with Isabelle/JEdit
are:

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 (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)

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.

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?


--
  Peter





On Mo, 2014-04-28 at 09:14 +0200, Andreas Lochbihler wrote:
> Hi Makarius,
> 
> Over the past weeks, I've been using Isabelle/jEdit about half of my Isabelle time (and 
> ProofGeneral 3.7.1.1 with XEmacs the other half). Isabelle/jEdit is great when it comes to 
> working on small projects or refactoring existing sources. I really like the negative line 
> spacing setting and completion of fact names! Thanks!
> 
> My main usage of PG is when I want to construct a complicated proof method call like
> 
> (fastforce intro: ... dest: ... elim: ... simp add: ... cong: ... del: ... simp del: ...)+
> 
> that collapses an apply script of a hundred lines. I haven't yet found a convenient way to 
> write the apply script in Isabelle/jEdit, because of reactivity issues (see item 2 below) 
> and the continuous updates of the output window (when I scroll to some other part of the 
> apply script using the cursor keys). Are there key bindings for scrolling that do not move 
> the cursor?
> 
> 
> Here are some things that could be improved in Isabelle/jEdit (I am currently on 
> Isabelle/4e2a0d4e7a82):
> 
> 1. Symbol completion in PG was absolutely deterministic. The immediate symbol completion 
> in jEdit works great, too, I merely had to learn new sequences of key strokes. Symbol 
> completion of non-unique results is not satisfactory.
> 
> a) Given some text like
> 
> definition foo where "foo = ..."
> 
> when I add an attribute like [simp]: after the where, I get a symbol completion popup to 
> replace the : with the element sign. Usually, my next thing is to move the cursor with the 
> cursor keys. But the popup gobbles all the key strokes until I explicitly close it with 
> ESC. As colons are used everywhere in Isabelle's outer syntax, it would really be great if 
> the popup only appears when I am in inner syntax.
> 
> b) Sometimes, when I write a HOL term, I used to not get the completion popup when I enter 
> something like \un if there were sufficiently many parse errors in that partial term. Even 
> Ctrl-b did not help. However, I cannot reproduce it in a small example at the moment.
> 
> 
> 2. Reactivity when processing large files
> 
> With PG, I knew how to control the Isabelle prover. When I edit a large file in a larger 
> project like JinjaThreads, every now and then, Isabelle changes the background colour from 
> red to gray and then, apparently nothing happens for minutes before Isabelle turns it red 
> again and starts reprocessing. Is there some way to explicitly tell Isabelle that it 
> should now start to check again. Toggling "continuous checking" does not help. Sometimes, 
> I even have to close the theory file and reopen it again.
> 
> 
> 3. Navigation between theories files
> 
> In PG, I usually have only a small subset of the loaded theories and ML files open as 
> buffers, and I conveniently switch between them with Ctrl-x b. In jEdit, I use Ctrl-` to 
> go to the previous file, but going to a different one is a pain, because I have to search 
> it in the complete list of open files.
> 
> It would be great if there was a list of just those files that I had on my screen 
> previously, not all loaded files.
> 
> Moreover, when I close a file and then press Ctrl-` in the file that shows up, I do not 
> get to the file I have visited before the two, but to some arbitrary other. Can jEdit 
> remember the order in which files have been visited? XEmacs at least does this.
> 
> 
> Maybe there are already solutions to the above annoyances, I just don't know them. There's 
> another thing I would like to see in jEdit: The window layout has three columns (one dock 
> on the left and one on the right) and the middle column (with the editor area) can be 
> divided in three rows (dock - text - dock). Is there some way that I can split the right 
> column into two rows to show two information areas at the same time (e.g. Output at the 
> top and Find below)?
> 
> 
> Andreas
> 
> 
> On 27/04/14 20:14, Makarius wrote:
> > Are there any remaining uses of Proof General, e.g. in the situation of current
> > Isabelle/5b6f4655e2f2 ?
> >
> > This is neither a joke nor a running gag -- I just can't think of anything myself after
> > the introduction of the spell checker.
> >
> >
> >      Makarius
> > _______________________________________________
> > isabelle-dev mailing list
> > isabelle-dev at in.tum.de
> > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev