Re: [isabelle] 2014-RC1 issues



On Thu, 31 Jul 2014, Peter Lammich wrote:

Thus, in my case, it is difficult to write theories without warnings, or to manually check every single warning whether it is bad (garbage in the theory) or not (just some spurious simplifier warning).

The surprise will probably come in batch-build mode, as this will be the time when the garbage will make problems.

I'm already looking forward to the tutorials of the semantics-lecture,
where students will definitely hand in lots of unfinished lemmas, many
of them convinced they actually have proven it ...
In PG, or even in older isabelle/jedits, I could just give them the rule
of thumb: Your theory must not contain errors, sorrys, or oops.

Also, I will have hard times checking the submissions, as I have to manually check every warning to see wether the proof is actually closed ...

First note that I have changed the regular warning to an error_message in https://bitbucket.org/isabelle_project/isabelle-release/commits/ae3eac418c5f so it will be in the text release candidate. Hopefully people will actually test all that has accumulated.


In general, we have always had the following situation:

  * Authentic checking of theories requires a batch build.  It was never
    easier than today to do that (see the "system" manual).

    People sometimes "forget" to make a proper ROOT for their stuff, or
    don't know how it is done or that it is important.  Whenever someone
    shows me some theories that are not just small snippets, my first
    reflex is to do the missing "isabelle mkroot" and then the batch
    build to see if they are correct.

  * Proof General in the past and Prover IDE front-ends in the present are
    only an approximation, with a lot of conveniences, but without the
    full detail of checking.

    Proof General even had quick_and_dirty on by default over most of its
    life time, until that broke by accident in the 3.x to 4.x transition.


In situations where proper builds are too much for small experiments, it is possible to use the new "isabelle console" together with plain use_thy in raw ML (which is not Isabelle/ML); see also the "system" manual. Note that the old "isabelle tty" is already removed, although there is still "Isar.main()" to invoke the old toplevel.


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

Looks like I have to lower my expectations to modern user interfaces. One of these expectations is full configurability, not forcing the user to some fixed shortcuts that, depending on typing habits, may or may not be convenient.

There is nothing modern about Java/AWT/Swing -- it is in fact legacy for many years -- like most other GUI frameworks. Swing does have a lot of configurability, but a bit too much for my taste, and I don't really understand most of it. jEdit has its own Swing add-ons and bypasses to provide a quite sane environment.

For Isabelle/jEdit, I've spent extra care from the start to make copy-paste work almost universally. I remember Proof General / Emacs as something were this rarely worked on all platforms and all versions; I am surprised that it is now perceived differently.

When Isabelle/jEdit was young and fresh in 2008/2009, there was a local presentation of it at TUM. Someone asked: "What will be its main features?" My spontaneous response: "reliable copy-paste".


It was a very useful feature, and I'm really missing it. As code-folding also does not work, there is currently no feature that assists in keeping track of the structure of big developments.

jEdit also has explicit folds with funny {{{ }}} notation.


	Makarius




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