Re: [isabelle] Isabelle2016-RC0 - AFP and Library available for testing



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


> On 3 Jan 2016, at 1:20 PM, Gerwin Klein <kleing at unsw.edu.au> wrote:
>
>
>> On 03.01.2016, at 02:53, Makarius <makarius at sketis.net> wrote:
>>
>> 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.
>
> It should end up in the AFP eventually, but it hasnât yet. It needs cleanup.
>
> Weâll start updating to Isabelle2016-RC* and Iâll post an update when itâs pushed out.
>
> 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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.