[isabelle-dev] Towards the Isabelle2014 release

[Thomas Sewell]

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.sewell at 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-dev at in.tum.de
>>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>>>>
>>> _______________________________________________
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>>>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: AFP-hypsubst.diff
Type: text/x-patch
Size: 64398 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140611/daa1acc7/attachment-0004.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: hypsubst.diff
Type: text/x-patch
Size: 55473 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140611/daa1acc7/attachment-0005.bin>