Re: [isabelle] AFP Incompleteness Entry



Good point, the development version is fine.

As long as the name clash exists in Isabelle itself, the issue will potentially reappear in other developments, though, so we should do something more permanent about it.

Cheers,
Gerwin

> On 20.09.2016, at 03:10, OndÅej KunÄar <kuncar at in.tum.de> wrote:
> 
> Actually, this limitation of Nominal2 in AFP was already solved in
> AFP/c515e20878fe: to be able to use the more standard Library/FSet.thy, rather than Quotient_Examples/FSet.thy (patch by Joachim Breitner)
> 
> Ondrej
> 
> On 09/18/2016 06:35 AM, Gerwin.Klein at data61.csiro.au wrote:
>> Turns out there is already a comment in Nominal2/ROOT:
>> 
>>    (* cannot depend on HOL-Library image because of name clash with Library/FSet: *)
>>    "~~/src/HOL/Quotient_Examples/FSetâ
>> 
>> Thatâs certainly more than a little inconvenient.
>> 
>> One of the two theories HOL/Library/FSet and HOL/Quotient_Examples/FSet should be renamed. This is not really an issue with the AFP, but with the Isabelle distribution itself.
>> 
>> Who are the guardians of these two?
>> 
>> Cheers,
>> Gerwin
>> 
>>> On 18.09.2016, at 12:58, Corey Richardson <corey at octayn.net> wrote:
>>> 
>>> On 2016-09-17 22:29, Gerwin.Klein at data61.csiro.au wrote:
>>>> Hi Corey,
>>>> 
>>>> I canât reproduce the errors â if I download afp-2016-09-09, untar, and load up the theory Goedel_I in jedit/Isabelle2016 it processes fine, including the theories from Nominal2.
>>>> 
>>>> Is it possible that it is loading a wrong Nominal2 package from somewhere else, i.e. from an image?
>>>> 
>>> 
>>> It's certainly possible, and it seems that was indeed the issue. Using
>>> the HOL heap instead of HOL-Library yields success for me. Perhaps this
>>> caveat should be mentioned on the AFP site? It seems like the root of
>>> the issue here is some difference with multiset (at least, the first
>>> error I got in Nominal2_Base was the instance of multiset :: (pt) pt).
>>> 
>>> Thanks for the help, regardless!
>>> 
>>> Best,
>>> Corey
>>> 
>>> 
>> 
> 
> 



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