Email Gateway (Aug 19 2022 at 14:43): Email Gateway (Aug 19 2022 at 14:43):From: Salomon Sickert <sickert@in.tum.de>
Hello List,
I guess this is the right place to report bugs. If not, please refer me
to the right place.
Apparently in Isabelle 2013-2 the quotient_type command doesn't work,
if the theory name contains white-space.
In my testcase the theory was called "With Whitespace" and the command
produced the following error:
attribute "Lifting.lifting_restore_internal": bad arguments
Whitespace.foo.lifting
I attached a testcase for the problem to reproduce the issue. One
theory called "WithoutWhitespace.thy", which works fine, and a copy
renamed to "With Whitespace.thy", which fails.
Regards,
Salomon
With Whitespace.thy
WithoutWhitespace.thy
Email Gateway (Aug 19 2022 at 14:43):From: Lawrence Paulson <lp15@cam.ac.uk>
I don’t think that any names in Isabelle are allowed to contain whitespace.
Larry Paulson
Email Gateway (Aug 19 2022 at 14:45):From: Salomon Sickert <sickert@in.tum.de>
Up to now Isabelle never complained about whitespace in theory names,
so I assumed that this is supported.
IMHO Isabelle should either immediately complain about the whitespace
or quotient_type should work as expected. Anything else feels a bit
inconsistent.
Apart from that:
Guessing from the error output, I would say that some function is
splitting the string containing theory names using whitespace as
delimiter. Thus ends up with the theory name "Whitespace" and loses the
"With " part.
Regards,
Salomon Sickert
Email Gateway (Aug 19 2022 at 14:45):From: Lawrence Paulson <lp15@cam.ac.uk>
Isabelle dates from an era when no names contained white space, so it wasn’t even thought about. The development team will have to think about whether whitespace in theory names is worth supporting or not.
Larry Paulson
Email Gateway (Aug 19 2022 at 15:17):From: Makarius <makarius@sketis.net>
The quotient_type command might have some weaknesses in its implementation
to break in such an odd way, but theory names with white-space just don't
make any sense. Think of it as a formal module name and a file-name at
the same time: use plain ASCII identifier syntax without any special
ambitions.
The canonical form without whitespace actually uses an underscore:
Without_Whitespace.thy -- camel case is not used in Isabelle sources (at
least not in up-to-date ones).
Makarius
Email Gateway (Aug 19 2022 at 15:18):From: Makarius <makarius@sketis.net>
I am myself too young for that, but my Compiler Construction professor
used to tell us that really old versions of FORTRAN allowed white space in
identifiers, which was before there was a clear concept of a "token" in
programming languages. It was one of his "never do this at home" examples
-- he had other ones drawn from Knuth's TeX language.
Makarius
Email Gateway (Aug 19 2022 at 15:19):From: Lawrence Paulson <lp15@cam.ac.uk>
Not exactly. FORTRAN did not — perhaps still does not — regard spaces as significant. Thus it is that
DO 30 I = 1. 100
does not start a loop but instead assigns DO30I the value 1.1.
Larry
Last updated: Apr 26 2024 at 16:20 UTC