[isabelle-dev] Towards the Isabelle2014 release

[Gerwin Klein]

http://isabelle.in.tum.de/testboard/Isabelle/rev/d765be00b181

There is a separate changeset for the AFP.

If you’re happy with the one above, and maybe Tom sends me a rebased version, I can push them both.

Gerwin

On 30 Jun 2014, at 2:22 pm, Thomas Sewell <thomas.sewell at nicta.com.au> wrote:

> 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.