Re: [isabelle] AFP Incompleteness Entry



Perfect.
Gerwin



> On 20 Sep 2016, at 09:57, OndÅej KunÄar <kuncar at in.tum.de> wrote:
> 
> was renamed in 003622e08379: resolve the name clash of HOL/Library/FSet and HOL/Quotient_Examples/FSet
> 
> Ondrej
> 
> On 09/19/2016 11:59 PM, Gerwin.Klein at data61.csiro.au wrote:
>> 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.