Re: [isabelle] 2014-RC1 issues

On Wed, 30 Jul 2014, Peter Lammich wrote:

* If a lemma is not properly closed, ie. the done or qed is missing, the
  next command only issues a warning and recovers the state. As warnings
  are omnipresent in Isabelle, it is very hard to spot such places when
  developing a theory. This leads to garbage accumulating in theory
  files and probably only being discovered upon batch-build.

That is actually a contribution in Isabelle2014 to make error recovery a bit more useful, without doing the real job of (sub)structural checking yet.

What do you mean by "warnings are omnipresent in Isabelle"? The prover IDE shows them more prominently than in the TTY past, but that could be taken as motivation to remove the reasons for warnings. Not all such spots are bad, but an avarage theory normally has only few warnings.

* In the output buffer, the standard Ctrl-Ins for "copy" does not work,
while it works in the main text area. Can these shortcuts be configured
separately? Or do I have to live with Ctrl-C?

I did not know about Ctrl-Ins yet. What you observe here is merely the known and documented difference of the main jEdit text area with its actions and shortscuts vs. regular Java Swing GUI components. The latter only have basic Ctrl-C, and it actually works routinely, which is a big step forwards to the historic perspective.

If Ctrl-C does *not* work somewhere, it is actually an issue that needs to be addressed.

* Odd behaviour when focus lays in output buffer or any other panel:
  Cursor movement and entering newlines still goes to the text area, but
  other keyboard input goes to the panel (and may or may not be
  interpreted there). The only indication for this is a slightly changed
  color of the cursor in the main window.

This belongs to normal jEdit policies. In Isabelle/jEdit for the coming release I added the faint cursor to emphasize that -- normally it would be just absent.

* No indentation feature. It is hard to keep track of big proofs and
  indent them correctly, in particular as code-folding does not work

In PG, there was a nice auto-indentation feature that worked reliable for (almost) all cases.

That is indeed a notable omission. In 1998, I added indentation to PG 2.x quite early, and earned the name "The indentation Man" in the inner circle of PG developers. In Isabelle/jEdit the lack of it has become a running gag over the years: it needs to come one day, but so far I just wanted to evade the wrath of users when the Prover IDE suddenly makes *standard* indentation of Isar text by default.

* When developing proofs:
 The output window displays the current position
 by default ... if you are typing a new command, it usually displays
 "Syntax error".
 However, while typing your next method/isar step, you usually want to
 see the current goal state, not a the completely useless information
 "syntax error".

 In PG, the output was not updated before you explicitely processed
 the command. Maybe, this can be simulated by turning auto-update off
 and bind update to a convenient shortcut.

Nothing new about this observation. It belongs to general mismatch of TTY/PG mechanics wrt. the document-oriented model. Note that you can also use the Query panel to print proof states on demand and only on demand.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.