This is a tremendous achievement, thanks! Some of those proofs are unbearably messy… I’m impressed that you were able to do this in such a short time!
Larry On 11 Jun 2014, at 05:56, Thomas Sewell <thomas.sew...@nicta.com.au> wrote: > OK, I've finished the needed adjustments the AFP proofs which were affected > by the hypsubst change. > > The result is fairly encouraging: the AFP is *huge* and the diffstat of the > required changes is: > 63 files changed, 134 insertions(+), 81 deletions(-) > > Not an especially high percentage of changes in the end. > > To clarify, I had the AFP fully working at the last release. The condensed > patch I'm showing you now transplants that change onto the current state and > fixes as much as possible. CAVA seems to be broken anyway. > > Gerwin will push the isabelle hypsubst change to the testboard now (assuming > he can remember how), and, if noone objects in the next day or two, I'm going > to recommend the change be pulled into Isabelle mainline. > > I don't think there's a testboard equivalent for a simultaneous Isabelle/AFP > change, so we'll just hold that change here and push it into the AFP if the > Isabelle change is accepted. > > I attach the final patches for isabelle and the AFP, in case anyone is super > interested. > > Thanks all, > Thomas. > > > On 05/06/14 13:44, Thomas Sewell wrote: >> 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 > > <AFP-hypsubst.diff><hypsubst.diff>_______________________________________________ > 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
