Re: [isabelle] AFP Incompleteness Entry



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.