Email Gateway (Aug 22 2022 at 12:07): Email Gateway (Aug 22 2022 at 12:07):From: "C. Diekmann" <diekmann@in.tum.de>
Hi,
My projects have external dependencies, which makes testing a new
Isabelle RC a bit hard.
Is there a working version of the afp available?
Is there a working version of the famous seL4/l4v WordLemmaBucket available?
Best,
Cornelius
Email Gateway (Aug 22 2022 at 12:08):From: Makarius <makarius@sketis.net>
On Sat, 2 Jan 2016, C. Diekmann wrote:
To get started with systematic testing there is now the relatively
early http://isabelle.in.tum.de/website-Isabelle2016-RC0 (corresponding
to Isabelle/e18444532fce and AFP/c62777f3e932).My projects have external dependencies, which makes testing a new
Isabelle RC a bit hard.Is there a working version of the afp available?
AFP is cited above as c62777f3e932, it can be cloned from
https://bitbucket.org/isa-afp/afp-devel/
Is there a working version of the famous seL4/l4v WordLemmaBucket
available?
I don't know.
The standard way to keep generally interesting libraries in an
automagically maintained way is to put them into AFP. Gerwin Klein should
be able to say how feasible it is for this word bucket.
Makarius
Email Gateway (Aug 22 2022 at 12:08):From: Makarius <makarius@sketis.net>
Is that the "where" attribute of Eisbach or Pure?
The Eisbach version was fluctuating a bit in the past few months. In
Isabelle2016-RC1 it is again closer to the Pure version.
The full re-unification of both variants has to wait for another release.
Makarius
Email Gateway (Aug 22 2022 at 12:08):From: Daniel Matichuk <Daniel.Matichuk@nicta.com.au>
On 17 Jan 2016, at 12:19 AM, Makarius <makarius@sketis.net> wrote:
On Mon, 11 Jan 2016, Gerwin Klein wrote:
There are some theories it depends on that don’t work yet, but WordLemmaBucket should be usable without those (they are mostly some Eisbach tweaks that still need updating and are possibly obsolete for Isabelle2016).
During the update I found we had a few instance of this pattern:
lemmas x = y [where a = b, simplified]
This fails with an error message in Isabelle2016-RC0. I used this idiom instead:
lemmas x' = y [where a = b]
lemmas x = x' [simplified]Is this what I should be doing, or is there a nicer way without introducing an x'?
Is that the "where" attribute of Eisbach or Pure?
This is indeed the Eisbach “where", which WordLemmaBucket happened to use due to it depending on Eisbach in our theory layout. The theory now checks in Isabelle2016-RC1 without rewriting any attribute expressions.
The Eisbach version was fluctuating a bit in the past few months. In Isabelle2016-RC1 it is again closer to the Pure version.
The full re-unification of both variants has to wait for another 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.
Email Gateway (Aug 22 2022 at 12:21):From: Makarius <makarius@sketis.net>
Great.
Just note that between informal Isabelle2016-RC0 and formal
Isabelle2016-RC1, a few incompatibilities may creep in, but it should be
handable. I guess that Isabelle2016-RC1 will be published in 2 weeks.
Makarius
Email Gateway (Aug 22 2022 at 12:25):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Thanks for the heads-up. Let’s see how it goes, usually the last tweaks are easy to adapt to.
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.
Email Gateway (Aug 22 2022 at 12:29):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
An Isabelle2016-RC0 Version of WordLemmaBucket is now available from:
https://github.com/seL4/l4v/blob/2016/lib/WordLemmaBucket.thy
There are some theories it depends on that don’t work yet, but WordLemmaBucket should be usable without those (they are mostly some Eisbach tweaks that still need updating and are possibly obsolete for Isabelle2016).
During the update I found we had a few instance of this pattern:
lemmas x = y [where a = b, simplified]
This fails with an error message in Isabelle2016-RC0. I used this idiom instead:
lemmas x' = y [where a = b]
lemmas x = x' [simplified]
Is this what I should be doing, or is there a nicer way without introducing an x'?
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.
Last updated: Apr 20 2024 at 08:16 UTC