[isabelle-dev] Towards the Isabelle2014 release

[Thomas Sewell]

The changeset has landed in the sense that I sent Gerwin a bundle containing:

changeset:   6bf63b1f41f0
tag:         tip
user:        Thomas Sewell <thomas.sewell at nicta.com.au>
date:        Wed Jun 11 14:24:23 2014 +1000
summary:     Hypsubst preserves equality hypotheses

He probably pushed it to the testboard with that changeset ID, but he might have rebased, in which case it will have that summary but a different ID. I don't know what the testboard report was, and in the meanwhile Gerwin has been travelling, so no further progress has been made.

I'd like to get this process moving again. If noone has any objections, I'd like to move the change into mainline ASAP so it can be included in the upcoming release. I can help fix any resulting failures which I've somehow overlooked. I'm not sure who I should ask to push the change in though.

Thomas.

________________________________________
From: Makarius [makarius at sketis.net]
Sent: Monday, June 30, 2014 9:56 PM
To: Gerwin Klein; Thomas Sewell
Cc: isabelle-dev at mailbroy.informatik.tu-muenchen.de
Subject: Re: [isabelle-dev] Towards the Isabelle2014 release

On Wed, 11 Jun 2014, Gerwin Klein wrote:

> On 11.06.2014, at 2:56 pm, Thomas Sewell <thomas.sewell at nicta.com.au> wrote:
>
>> Gerwin will push the isabelle hypsubst change to the testboard now (assuming he can remember how).
>
> He could and did.

Has that change been landed?  Which changeset IDs are relevant?

I don't have any special expertise in this area, but merely want to make
sure that we can move on towards the release.


        Makarius

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.