Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2015-RC3 and AFP


view this post on Zulip Email Gateway (Aug 22 2022 at 09:43):

From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
The branch happened a while ago (see my email from 20 April, looks like I sent this only to isabelle-devel, though) and lives in hg.code.sf.net/p/afp/afp-2015

Only editors are supposed to push to this branch and it should by now be basically frozen (I do still pull in new submissions from 2014 manually if they come in).

afp-2015 and RC3 currently pass the test, afp-2015 contains a compatibility patch for Lifting_Definition_Option for the corresponding RC3 changes, so that part is all fine.

Cheers,
Gerwin


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.

view this post on Zulip Email Gateway (Aug 22 2022 at 09:43):

From: Christian Sternagel <c.sternagel@gmail.com>
Thanks. Previously, I somehow missed the location of afp-2015. Now,
everything works for me ;)

cheers chris

view this post on Zulip Email Gateway (Aug 22 2022 at 10:10):

From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,

it seems the branch of the AFP into afp2015 and afp-devel did not yet
take place, did it?

Moreover some changes that are part of RC3 (concerning the lifting
package) are incompatible with the current afp-devel (the entry
Lifting_Definition_Option seems to be "broken").

In order to test RC3 it would be nice to have a corresponding AFP version.

cheers

chris

view this post on Zulip Email Gateway (Aug 22 2022 at 10:10):

From: Makarius <makarius@sketis.net>
There was some earlier confusion, but with Isabelle2015-RC3 the situation
was back to normal, althouth I did not announce this with that snapshot.

I am working routinely with hg.code.sf.net/p/afp/afp-2015 (currently at
4a7a946fa6c5).

Makarius


Last updated: Apr 19 2024 at 12:27 UTC