[isabelle-dev] Remaining uses of Proof General?

[Peter Lammich]

Hi all.

I have given Isabelle/jEdit another try and worked with it for almost
two weeks, on different tasks:
  * Porting the CAVA afp entries (depending on >300 theory files) from
2013-2 to devel.

  * Formalizations and proof development (The standard usage)

  * Writing tools in ML (ML-blocks in thy-file)

I have compiled a list of problems that I encountered during my work.
I have added descriptions to how PG solved these problems.

The problem report here refers to Isabelle version 2ccd6820f74e.

My overall impression is that Isabelle/jEdit is usable but much less
mature than PG:
It does not scale well to large projects, and tends to be unstable.
It has many cool advanced features, but lacks important basic ones. 

However, in my opinion, Isabelle/jEdit is approaching a level of
maturity required for production use, once the user knows about its
deficits and how to avoid them. I will continue using Isabelle/jEdit for
a few more weeks, hoping that a few more basic features will be
added/fixed before the next release ...


SCALABILITY & STABILITY:

* Isabelle/jEdit gets really slow and unresponsive when many files are
loaded (you have to wait seconds for a keystroke to show its effect). As
all prerequisite theories (not in an image) are automatically loaded,
this is unavoidable. In PG, it's no problem to load a theory with many
prerequisites, nor to have many buffers open simultaneously. 

NOTE: This problem could be solved in my case by 1) giving jEdit a
ridiculously large amount of heap space (4Gb) and, 2) using images for
prerequisite theories.

* Isabelle/jEdit does not scale to large files. Error markers on the
right side are only displayed for a context around the current cursor
position. There seems to be no way to jump to the error position. If the
error happens to be displayed as a red bar on the right side of the
editor area, pixel-accurate mousing is required to jump to the error,
and not to a position dozens of lines away.   

In PG, you could always jump to the position where processing failed by
Ctrl-. . Moreover, you got error messages with file names and line
numbers, that you could use to navigate to the error position easily.

* Isabelle/jEdit seems to be quite unstable. Within one week, it
happened several (3 or 4) times that the whole thing just became
unresponsive, and had to be restarted to continue work. In PG, those
things happen perhaps once in a month.

IMPORTANT FEATURES THAT ARE MISSING & OVERLY TEDIOUS WORKFLOWS

* Isabelle/jEdit does not support highlighting of paranthesis in the
output window (it does work in PG!). This is an essential feature to
read bigger goal states. 

Moreover, the output buffer does not support middle-mouse-button
copy-and-paste on my ubuntu-box, while it perfectly works in the editor
window.

* Long list of warnings, e.g. "duplicate simp rule", or tracing messages
produced by a method appear before the subgoals in the 
  output, and thus makes them inaccessible without lots of scrolling.
This feature is a real flow-stopper when exploring proofs. 

In PG, it is possible to have separate buffers for the goal-state, the
tracing, and the warning messages, thus you always see the current
subgoal you are working on without scrolling down some buffer every
time.

* If sledgehammer (both over panel and as command) is running, further
processing of the file is blocked/very slow. Thus, it is not possible
to run sledgehammer and, in parallel, continue exploration to find your
own proof. In PG, parallel sledgehammering works, and I used it
extensively. In Isabelle/jEdit I now think twice before I invoke
sledgehammer, because it just interrupts my workflow and I have to wait
for it to finish staring at the sledgehammer-window and doing nothing. 


* Isabelle/jEdit cannot open a theory-file without processing it. This
is in particular a problem when porting stuff and opening the original
version of the same file to look something up. Even worse: Once opened,
you cannot close the file again, and it will remain in the theory panel
(with an error marker) until you quit jEdit.

In PG, it is no problem to open a file without processing it.

* The standard search (Ctrl-F) function does not allow to enter
non-ASCII characters at all. This is a real show-stopper if you search
for a text containing such characters. In PG, you could at least use
\<...> - tokens to enter non-ASCII characters.

Moreover, I would like an incremental search, but there is probably a
jEdit pluging somewhere? (Probably with the same problems of entering
non-ASCII characters)


* When theories have inconsistent file/theory name, you will only find
the error by stepwise going back the chain of "bad theory" -  errors,
file by file. This is simply tedious. In PG, you got a backtrace in the
output, and could immediately identify the broken file.


* Auto-Completion does not really work. You have to decide for a
"completion delay". If you choose it too short, some completions will
not appear at all. If you choose it too long, it interrupts your typing
flow when entering special characters.

In PG, there is no context-sensitive completion at all ... the one in
jedit is actually not usable without
  tolerating .5sec completion delay on every special character you want
to type)

Moreover, the completion mechanism for entering special characters seems
not to be as mature as the one in PG was: When entering sequences that
should be completed, e.g., \lambda, this only works if there are no
characters behind. All in all, I am typing significantly more to enter
special characters than I did in PG.


* "Disappearing Proofs" in PG is a really nice feature to keep overview,
in particular in larger files. In PG, I used it heavily. There is
nothing similar in Isabelle/jEdit. Code-folding can be used to a certain
extent, but it cannot handle apply-style proofs, and is not applied
automatically as in PG. 

Moreover, code-folding still seems not to work properly: Sometimes,
fold-markers simply do not appear, sometimes they appear at completely
wrong places. I'm not sure whether this is a non-deterministic effect,
or depends on some garbage text at the end of the theory file. 


--
  Peter