Email Gateway (Aug 22 2022 at 14:06): Email Gateway (Aug 22 2022 at 14:06):From: Corey Richardson <corey@octayn.net>
Greetings AFP maintainers,
Using the 2016-09-09 release of the AFP, I have tried exploring the
Incompleteness entry with Isabelle2016. The sessions of that directory
build fine with "isabelle build", but when I try to open Goedel_I.thy in
jEdit I get numerous errors from Nominal2. Is there a special way to
invoke jEdit that allows interactive exploration of these theories? I
especially find the control-click navigation useful.
Best,
Corey
signature.asc
Email Gateway (Aug 22 2022 at 14:06):From: Corey Richardson <corey@octayn.net>
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
signature.asc
Email Gateway (Aug 22 2022 at 14:06):From: Lars Hupel <hupel@in.tum.de>
Hi Corey,
it is already documented in some way: the ROOT file specifies the parent
session. In case of "Incompleteness":
session Incompleteness (AFP) = HOL +
But it is true that it could be clarified in general.
Cheers
Lars
Email Gateway (Aug 22 2022 at 14:06):From: Gerwin.Klein@data61.csiro.au
Let me investigate that. You shouldn’t be getting any errors from Nominal2, esp not if it builds fine in batch mode.
Cheers,
Gerwin
Email Gateway (Aug 22 2022 at 14:06):From: Gerwin.Klein@data61.csiro.au
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?
Cheers,
Gerwin
Email Gateway (Aug 22 2022 at 14:06):From: Gerwin.Klein@data61.csiro.au
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
Email Gateway (Aug 22 2022 at 14:07):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
The Quotient_Examples version is clearly the one that should be renamed. Judging from the logs, it was developed by Cezary Kaliszyk, then semi-obsoleted by Ondra Kuncar who developed the new FSet in Library. See e.g. Isabelle/9a21e5c6e5d9. Perhaps we should simply rename the old, example "FSet" to "Old_FSet"? This would be consistent with this warning:
(****************
WARNING: There is a formalization of 'a fset as a subtype of sets in
HOL/Library/FSet.thy using Lifting/Transfer. The user should use
that file rather than this file unless there are some very specific
reasons.
*****************)
Jasmin
Email Gateway (Aug 22 2022 at 14:07):From: Ondřej Kunčar <kuncar@in.tum.de>
If nobody objects, I will rename Quotient_Examples/FSet to
Quotient_Examples/Quotient_FSet.
Ondrej
Email Gateway (Aug 22 2022 at 14:07):From: Gerwin.Klein@data61.csiro.au
Would work for me!
Cheers,
Gerwin
Email Gateway (Aug 22 2022 at 14:07):From: Ondřej Kunčar <kuncar@in.tum.de>
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
Email Gateway (Aug 22 2022 at 14:07):From: Gerwin.Klein@data61.csiro.au
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
Email Gateway (Aug 22 2022 at 14:07):From: Ondřej Kunčar <kuncar@in.tum.de>
was renamed in 003622e08379: resolve the name clash of HOL/Library/FSet
and HOL/Quotient_Examples/FSet
Ondrej
Email Gateway (Aug 22 2022 at 14:07):From: Gerwin.Klein@data61.csiro.au
Perfect.
Gerwin
Last updated: Apr 19 2024 at 20:15 UTC