[isabelle] Isabelle2016-1-RC0 available for testing

[Makarius]

Dear Isabelle users,

the year 2016 is an "Isabelle leap-year", with more than one release.
(The usual distance between regular releases is 8-10 months.)

Many changes and improvements have been accumulated in the past few
months. A preview of what is coming is available here:
http://isabelle.in.tum.de/website-Isabelle2016-1-RC0

This corresponds to Isabelle/666c7475f4f7 and AFP/1e958cc1942e. Note
that the website and documentation still need to be updated.


Despite the name "Isabelle2016-1", this is not a revised version of
Isabelle2016, but a completely new major release. See also
the NEWS file
http://isabelle.in.tum.de/website-Isabelle2016-1-RC0/dist/Isabelle2016-1-RC0/doc/NEWS.html

When discussing problems, observations, suggestions, etc. the mail
subject line should be changed to something meaningful (but the release
candidate number still given in the message body).


Makarius

[Andreas Lochbihler]

Dear Makarius,

I played a bit with RC0 and noticed that reactivity seems to be a bit lower than with
Isabelle2016. In particular, when I have a non-terminating proof command like

subgoal by transfer simp

and (due to some changes in the theory above) the proof loops, then I have found no way to
interrupt the proof. Even when I delete the whole line, PolyML and the JVM keep running at
100% for minutes and I don't get any updates in the output or state buffer any more. I
really have to shut down Isabelle/jEdit and restart to get back to work. This never
happened to me with Isabelle2016 in the past six months.

In the test, I ran Isabelle with the default settings on a quad core Intel from 4 years
ago with 16GB of RAM under Ubuntu 14.04.

Andreas

[Lars Hupel]

Dear Makarius,

the "proof outline" feature is very helpful. I have two suggestions for
improvements, and one item which could be worth thinking about:

1) Sometimes I define inductive predicates using "_" instead of
inventing a bogus variable name. When writing an inductive proof, I
usually do the same thing:

case (rec_comb Γ t css name Γ' cs u u' env _ rhs val)

The "proof outline" however will invent a funny name, like "uu". Is it
possible to also print "_" here? In my opinion it's much nicer to
explicitly state that a variable doesn't matter than to use a somehow
modified internal name.

2) Is it possible for the blue "i" icon in the gutter to disappear when
a proof body already exists? As it stands it is easily mistaken for a
hint given by "Auto Quickcheck" or "Auto Solve Direct".

3) I would assume that the mechanism is general enough to allow skeleton
generation for arbitrary initial methods. I'm mainly thinking about the
"standard" method here, but of course, this may also apply to others.

Cheers
Lars

[Lars Hupel]

Dear Makarius,

I noticed that auto-indentation is switched on by default. While this
improves the workflow when typing, it complicates it when committing: it
tends to introduce trailing spaces.

For example, when I finish a sub-proof like this:

have "..." ...<Enter>
<Enter>
...

Now, the middle line contains two trailing spaces. This is mildly
annoying, because I want to avoid checking in trailing spaces into
version control.

The workaround I'm employing currently is the "WhiteSpace" plugin
(<http://plugins.jedit.org/plugins/?WhiteSpace>) which allows to purge
trailing spaces on save. It can also be configured to just show them and
not purge them automatically.

Cheers
Lars

[Lars Hupel]

Dear Makarius,

it seems that in some situations, the "error" markup covers a too large
region. Here's a small example:

lemma True
proof -
have False
sorry

―‹abc›

The comment is also highlighted in red.

Cheers
Lars