[isabelle] quotient_type command fails

[Salomon Sickert]

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

[Lawrence Paulson]

I don’t think that any names in Isabelle are allowed to contain whitespace.

Larry Paulson

Apparently in Isabelle 2013-2 the quotient_type command doesn't work, if the theory name contains white-space.

[Salomon Sickert]

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

Post by Lawrence Paulson
I don’t think that any names in Isabelle are allowed to contain whitespace.
Larry Paulson

Post by Salomon Sickert
Apparently in Isabelle 2013-2 the quotient_type command doesn't
work, if the theory name contains white-space.

[Lawrence Paulson]

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

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.
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

Post by Lawrence Paulson
I don’t think that any names in Isabelle are allowed to contain whitespace.
Larry Paulson

Apparently in Isabelle 2013-2 the quotient_type command doesn't work, if the theory name contains white-space.

[Makarius]

Post by Lawrence Paulson
Isabelle dates from an era when no names contained white space, so it
wasn’t even thought about.

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

[Lawrence Paulson]

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

Post by Lawrence Paulson
Isabelle dates from an era when no names contained white space, so it wasn’t even thought about.

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]

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
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.

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