Email Gateway (Aug 19 2022 at 15:05): Email Gateway (Aug 19 2022 at 15:05):From: Makarius <makarius@sketis.net>
Dear Isabelle users,
in anticipation of the Isabelle2014 release in August, the first official
release candidate Isabelle2014-RC1 is now available for testing:
http://isabelle.in.tum.de/website-Isabelle2014-RC1
Some enthusiasm for testing is important to keep up with the high levels
of system sophistication and user expectation that we have seen in recent
years. Observations and problems of release candidates may be discussed
here on isabelle-users, or via private mail with the person who is
responsible (when that is obvious).
We have about 3 weeks time for that, with 2-3 release candidates as usual.
The time to report problems is before the final release, not after it!
Makarius
Email Gateway (Aug 19 2022 at 15:05):From: Peter Lammich <lammich@in.tum.de>
How to transfer my configuration settings, shortcuts, abbreviations,
etc. from the repository version to 2014-RC1 and later to 2014?
Email Gateway (Aug 19 2022 at 15:05):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear all,
I observed a problem with datatype_new which was not present in Isabelle2014-RC0
theory Test
imports
Main
begin
typedef ('a,'b)com = "(UNIV :: ('a * 'b)set)" by auto
datatype_new ('q,'f) foo = Bar 'f "'q list" "('q,unit)com"
*** [| a = local.foo.Bar x1 x2 x3; b = local.foo.Bar y1 y2 y3; R x1 y1;
*** x2 = y2; x3 = y3 |]
*** ==> thesis |]
*** ==> thesis
*** Proof failed.
*** 1. !!x1 x2 x3 x1a x2a x3a.
*** [| R x1 x1a; list_all2 op = x2 x2a; x3 = x3a;
*** !!x1b x2b x3b y1 y2 y3.
*** [| x1 = x1b; x2 = x2b; x3 = x3b; x1a = y1; x2a = y2; x3a = y3;
*** R x1b y1; x2b = y2; x3b = y3 |]
*** ==> thesis;
*** b = local.foo.Bar x1a x2a x3a; a = local.foo.Bar x1 x2 x3 |]
*** ==> thesis
*** The error(s) above occurred for the goal statement (line 8 of "~/Test.thy"):
*** [| local.foo.rel_foo R a b;
*** !!x1 x2 x3 y1 y2 y3.
*** [| a = local.foo.Bar x1 x2 x3; b = local.foo.Bar y1 y2 y3; R x1 y1;
*** x2 = y2; x3 = y3 |]
*** ==> thesis |]
*** ==> thesis
end
A hg bisect delivers f9dd8a33f820 as first problematic revision.
Kind regards,
René
signature.asc
Email Gateway (Aug 19 2022 at 15:05):From: Makarius <makarius@sketis.net>
The persistent state is usually confined to $ISABELLE_HOME_USER -- you can
access that symbolically in the Prover IDE, e.g. the file-browser in
Faviourites, to see where it is actually pointing in the file-system.
For versions that are almost identical, such as presumably
Isabelle2014-RC1 ... Isabelle2014 final, it should be possible to move
over the whole directory content (while the system is not running).
For distinctive release it requires more care, though: there is no
official support for this non-trivial problem. I normally look at
individual files like $ISABELLE_HOME_USER/jedit/properties (after sorting)
and transfer changes bit-by-bit.
Makarius
Email Gateway (Aug 19 2022 at 15:06):From: Dmitriy Traytel <traytel@in.tum.de>
Hi René,
Last updated: Apr 26 2024 at 01:06 UTC