Indeed, there is a backward compatibility mode declaration. In fixing
things, I've been trying to use it as little as possible and as locally
as possible. Perhaps I should be bolder.
I'm aesthetically against using the compatibility mode all over the
place, since I feel that it's just mysterious. Of course, a lot of
Isabelle proof scripts are a bit mysterious already.
In particular, I want to avoid ever changing the setting globally. I've
had some bad experiences in the past with theories with differing global
configurations, which means that the location of a tactic and the
include graphs of theories start having subtle effects on the way the
tactics run. It's a mess.
I've started running through the AFP, and it doesn't look too bad. I'll
report on this again in the next few days.
Cheers all,
Thomas.
On 04/06/14 23:23, Lawrence Paulson wrote:
Didn’t we agree that a “backward compatibility mode” declaration (restoring the
former behaviour) would have to be available? That should make repairing legacy
proofs trivial. Naturally we would like to gradually port some of these
developments to do things the new way, but only some of them, and not
immediately.
Backward compatibility will be necessary for users, even if not for us.
Larry
On 4 Jun 2014, at 06:27, Thomas Sewell <thomas.sew...@nicta.com.au> wrote:
I had hoped to have the change I was making to hypothesis-substitution ready
for the coming release.
I've got it working for all of HOL and the library, and begun looking at the
AFP and at the l4.verified proofs. The HOL+library changes were easy enough,
but the l4.verified changes are somewhat daunting and I haven't gotten anywhere
with the AFP yet.
I'll have another look at it, because I'd like this to go somewhere at some
point. It might have to wait for a subsequent release though.
Cheers,
Thomas.
On 30/05/14 21:30, Makarius wrote:
The summer is getting close, and we need to start thinking about the coming
release.
I am myself on vacation during most of June. On return I would like to wrap up
rather quickly, so that we can publish Isabelle2014-RC0 in the second week of
July, for the Isabelle tutorial at VSL2014 Vienna. That will be still within
the main Isabelle repository.
The usual fork to the release repository and the regular sequence of
Isabelle2014-RC1, RC2, RC3, ... will happen in the week after ITP 2014.
I am myself attending the mega event at Vienna 13..19-Jul-2014. This will be
also an opportunity to show me personally remaining snags, and to continue the
elimination of remaining uses of Proof General. (It is getting harder and
harder to construct counter-examples to the claim that this set is already
empty.)
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
