Re: [isabelle] AFP Incompleteness Entry



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.