Email Gateway (Aug 18 2022 at 18:26): Email Gateway (Aug 18 2022 at 18:26):From: Makarius <makarius@sketis.net>
The next official Isabelle release is scheduled for October 2011. In the
2-3 weeks before shipment there are traditional test releases, but this
time they are called "release candidates" and announced to a wider
audience.
So Isabelle2011-1-RC1 is now available here:
http://isabelle.in.tum.de/website-Isabelle2011-1-RC1/
This enables users to try on their own machines, and see how their
applications work with the coming release. Incompatibilites between the
RCs and the final version should be neglibile.
This gives an opportunity for last-minute fixes, but no feature additions
(the de-facto feature freeze is usually 6 weeks before a release, so it is
long over).
Feedback on problems can be posted on the list, or sent privately.
Makarius
Email Gateway (Aug 18 2022 at 18:28):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
I have found the following inconveniences in the release candidate, but I
consider none of them as release critical.
notepad begin
fix xs ys :: "'a list"
have "xs = ys"
proof(induction xs=="xs" rule: list.induct)
print_cases
oops
end
Undoing a proof over an oops in a notepad context (as above) does not work
(at least with PG 3.7.1.1. and XEmacs; I haven't tested the other interfaces).
partial_function sometimes does not check that the head of the equation is
the same as the name of the constant to be defined, as in the attached example.
Andreas
Email Gateway (Aug 18 2022 at 18:28):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
... now with the attachment.
Andreas
Scratch.thy
Email Gateway (Aug 18 2022 at 18:28):From: Makarius <makarius@sketis.net>
There is a misunderstanding here, and I was first confused myself due to
the unusual indentation style of the above. When you 'oops' out of a
proof body, including notepad, the extra 'end' is already outside of it.
So it will normally close the current theory or locale target or similar.
Here is a working example:
notepad
begin
fix x y z
have xxx
oops
lemma "x = x" ..
I did not try it with ancient PG 3.7.1.1, though, only with current PG
4.1 and Isabelle/jEdit.
Makarius
Email Gateway (Aug 18 2022 at 18:29):From: Tobias Nipkow <nipkow@in.tum.de>
Am 28/09/2011 17:55, schrieb Andreas Lochbihler:
I have found the following inconveniences in the release candidate, but
I consider none of them as release critical.
- The new induction method does not give the induction hypothesis the
name IH (as advertised in the NEWS) when explicit parameter
instantiations are given. Here's a silly example
Parameter instantiations can result in structural changes in the
hypotheses due to rewriting. It becomes pretty much impossible to figure
out at the end what is an induction hypothesis and what comes from the
side conditions. In such cases induction defaults to the old naming
schema. We would love to improve this in the future.
Tobias
notepad begin
fix xs ys :: "'a list"
have "xs = ys"
proof(induction xs=="xs" rule: list.induct)
print_cases
oops
end
Undoing a proof over an oops in a notepad context (as above) does not
work (at least with PG 3.7.1.1. and XEmacs; I haven't tested the other
interfaces).partial_function sometimes does not check that the head of the
equation is the same as the name of the constant to be defined, as in
the attached example.Andreas
Am 27.09.2011 00:20, schrieb Makarius:
The next official Isabelle release is scheduled for October 2011. In
the 2-3
weeks before shipment there are traditional test releases, but this
time they
are called "release candidates" and announced to a wider audience.So Isabelle2011-1-RC1 is now available here:
http://isabelle.in.tum.de/website-Isabelle2011-1-RC1/
This enables users to try on their own machines, and see how their
applications
work with the coming release. Incompatibilites between the RCs and the
final
version should be neglibile.This gives an opportunity for last-minute fixes, but no feature
additions (the
de-facto feature freeze is usually 6 weeks before a release, so it is
long over).Feedback on problems can be posted on the list, or sent privately.
Makarius
Email Gateway (Aug 18 2022 at 18:29):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Just for the record: In ancient PG 3.7.1.1, I cannot undo oops in a notepad
proof context even if there is no end.
Andreas
Email Gateway (Aug 18 2022 at 18:36):From: Makarius <makarius@sketis.net>
On Tue, 27 Sep 2011, Makarius wrote:
The next official Isabelle release is scheduled for October 2011.
Here is another release candidate:
http://isabelle.in.tum.de/website-Isabelle2011-1-RC2/
The changes can be followed here:
http://isabelle.in.tum.de/repos/isabelle-release
There were also some refinements in the packaging, e.g. upgrade or
downgrade of contributing components like Emacs and Proof General.
Feedback on problems can be posted on the list, or sent privately.
So far there were only very few problem report, which means either there
are no problems or nobody has really tried it.
Makarius
Last updated: Apr 26 2024 at 04:17 UTC