Email Gateway (Aug 22 2022 at 16:14): Email Gateway (Aug 22 2022 at 16:14):From: Lars Hupel <hupel@in.tum.de>
[I took the liberty of moving this to isabelle-users]
Dear Christian,
Isabelles pdflatex document build fails when there is a space or any of
ä, ö, ü, ß and % in a theories name. Possibly more characters are
affected.
I would strongly recommend using plain ASCII characters for theory
names. Many things might break in unexpected things (apart from document
preparation) when non-ASCII characters are used.
To make Isabelle and its document build feature more permissive with
filenames, what is the best way to solve these issues?
I don't think this is expected to work, hence I see very little prospect
to solve this in the future.
Cheers
Lars
Email Gateway (Aug 22 2022 at 16:14):From: Makarius <makarius@sketis.net>
On 09/10/17 21:58, Lars Hupel wrote:
[I took the liberty of moving this to isabelle-users]
Great. Now we can discuss this properly.
Isabelles pdflatex document build fails when there is a space or any of
ä, ö, ü, ß and % in a theories name. Possibly more characters are
affected.I would strongly recommend using plain ASCII characters for theory
names. Many things might break in unexpected things (apart from document
preparation) when non-ASCII characters are used.
Theory names live in different formal domains, and certain restrictions
on the name syntax can be derived from that.
* Outer syntax: syntax category "name" (cf. isar-ref manual), which
means the quoted form can be almost anything, only excluding corner
cases of string representation (e.g. null characters, control
characters, odd Unicode sequences).
* Inner syntax (via theory name space qualifiers): syntax category
"id" or "short_ident" (cf. isar-ref manual). Otherwise it is in general
not possible to write qualified constant names like
My_Theory.my_constant. It is very unfriendly to produce a theory where
users cannot refer to qualified names within terms later.
* Formal theory header, both in Isabelle/ML and Isabelle/Scala: there
are differences in string representation (UTF-8 vs. UTF-16) and
sometimes the difference cannot be fully hidden. Note that it is
generally a bad idea to use raw Unicode for names in Isabelle, only
proper Isabelle symbols like \<alpha> or \<forall>.
* File-system name space on Linux, Mac OS X, Windows, Cygwin. This
imposes various real-world restrictions. Isabelle symbols are excluded
because of the use of the backslash required for Windows. Unicode often
works, but not universally on all platforms in all situations. Spaces
work most of the time, but are very bad style on Unix platforms. (There
is a funny problem in the Cygwin version bundled with Isabelle2016-1 and
Isabelle2017: if Isabelle is installed into a directory name like "test
a" or "testä" it works, but if it is "test ä" it doesn't. Maybe we
should start a thread on the Cygwin mailing list about that Unicode oddity).
Intersecting all these side-conditions, the remainder is indeed a plain
ASCII identifier consisting of: A-Z a-z 0-9 _ (starting with a letter).
Moreover, there is a hard and fast convention to use upper-case words in
singular that are separated by underscores (some particles might not
count as words and remain lower-case). Plural means that several
concepts of the same kind are covered.
Examples:
theory Nat -- a theory of natural numbers
theory List -- a theory of lists
theory Coinductive_List -- a theory of coinductive lists
theory Orders -- a theory with several kinds of orders (plural)
theory Misc_List_Lemmas -- a theory with various list lemmas (plural)
theory Fundamental_Theorem_of_Algebra -- particle in lower-case
A common mistake is to use plural too often, e.g. a theory "Lists" of
lists would provide a constant "Lists.map", but this should be
"List.map" instead.
Note that the situation is similar to type names: the type of lists is
called "list" in singular (and in lower-case).
To make Isabelle and its document build feature more permissive with
filenames, what is the best way to solve these issues?I don't think this is expected to work, hence I see very little prospect
to solve this in the future.
Right. At some point, the system should check that explicitly and reject
strange theory names outright.
The Prover IDE could also provide more hints about further fine-points.
Makarius
Email Gateway (Aug 22 2022 at 16:15):From: Christian Weinz <christian@madez.de>
El lun, 09-10-2017 a las 21:58 +0200, Lars Hupel escribió:
[I took the liberty of moving this to isabelle-users]
Thanks!
Dear Christian,
Isabelles pdflatex document build fails when there is a space or
any of
ä, ö, ü, ß and % in a theories name. Possibly more characters are
affected.I would strongly recommend using plain ASCII characters for theory
names. Many things might break in unexpected things (apart from
document
preparation) when non-ASCII characters are used.
Things do break, but I do not see how that is a reason not to fix them.
To make Isabelle and its document build feature more permissive
with
filenames, what is the best way to solve these issues?I don't think this is expected to work, hence I see very little
prospect
to solve this in the future.
I expect programs to properly handle filenames. I also don't think this
requires a big monolithic change.
Is there any negative effect of making Isabelle more robust in handling
of names?
Last updated: Nov 21 2024 at 12:39 UTC