Discussion:
[isabelle] AFP Incompleteness Entry
(too old to reply)
Corey Richardson
2016-09-18 00:05:29 UTC
Permalink
Raw Message
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
Corey Richardson
2016-09-18 03:05:49 UTC
Permalink
Raw Message
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
Lars Hupel
2016-09-18 08:11:32 UTC
Permalink
Raw Message
Hi Corey,
Post by Corey Richardson
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).
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
G***@data61.csiro.au
2016-09-18 11:16:56 UTC
Permalink
Raw Message
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
Post by Corey Richardson
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
Jasmin Blanchette
2016-09-18 11:38:47 UTC
Permalink
Raw Message
Post by G***@data61.csiro.au
(* 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?
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
Ondřej Kunčar
2016-09-18 12:46:24 UTC
Permalink
Raw Message
If nobody objects, I will rename Quotient_Examples/FSet to
Quotient_Examples/Quotient_FSet.

Ondrej
Post by Jasmin Blanchette
Post by G***@data61.csiro.au
(* 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?
(********************************************************************
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
G***@data61.csiro.au
2016-09-18 13:06:24 UTC
Permalink
Raw Message
Would work for me!

Cheers,
Gerwin
If nobody objects, I will rename Quotient_Examples/FSet to Quotient_Examples/Quotient_FSet.
Ondrej
Post by Jasmin Blanchette
Post by G***@data61.csiro.au
(* 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?
(********************************************************************
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
Ondřej Kunčar
2016-09-19 17:15:21 UTC
Permalink
Raw Message
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
Post by G***@data61.csiro.au
(* 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
Post by Corey Richardson
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
G***@data61.csiro.au
2016-09-19 22:06:20 UTC
Permalink
Raw Message
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
Post by Ondřej Kunčar
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
Post by G***@data61.csiro.au
(* 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
Post by Corey Richardson
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
Ondřej Kunčar
2016-09-20 00:01:32 UTC
Permalink
Raw Message
was renamed in 003622e08379: resolve the name clash of HOL/Library/FSet
and HOL/Quotient_Examples/FSet

Ondrej
Post by G***@data61.csiro.au
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
Post by Ondřej Kunčar
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
Post by G***@data61.csiro.au
(* 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
Post by Corey Richardson
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
G***@data61.csiro.au
2016-09-20 00:26:37 UTC
Permalink
Raw Message
Perfect.
Gerwin
was renamed in 003622e08379: resolve the name clash of HOL/Library/FSet and HOL/Quotient_Examples/FSet
Ondrej
Post by G***@data61.csiro.au
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
Post by Ondřej Kunčar
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
Post by G***@data61.csiro.au
(* 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
Post by Corey Richardson
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
G***@data61.csiro.au
2016-09-18 11:15:42 UTC
Permalink
Raw Message
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
Let me investigate that. You shouldn’t be getting any errors from Nominal2, esp not if it builds fine in batch mode.
Cheers,
Gerwin
Post by Corey Richardson
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
G***@data61.csiro.au
2016-09-18 11:18:57 UTC
Permalink
Raw Message
Let me investigate that. You shouldn’t be getting any errors from Nominal2, esp not if it builds fine in batch mode.

Cheers,
Gerwin
Post by Corey Richardson
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
Loading...