Email Gateway (Aug 22 2022 at 18:49): Email Gateway (Aug 22 2022 at 18:49):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi again,
an issue concerning paths in Isabelle/ML, as observed in Isabelle2018:
Path.basic accepts ".." and ".":
ML_val ‹Path.basic "."›
ML_val ‹Path.basic ".." = Path.parent› ~> false
As far as I understand the data model, ‹Path.basic "."› should be
rejected similar to ‹Path.basic ""›, and ‹Path.parent› would be the
correct way to refert to the parent directory.
Cheers,
Florian
signature.asc
Email Gateway (Aug 22 2022 at 18:50):From: Makarius <makarius@sketis.net>
That is indeed a bit odd: I will revisite this and tighten the
programming interface.
Whenever I see Path.basic, I ask myself if it would be better to use
general Path.explode instead, just for simplicity and uniformity. Did
you have an application where the implicit "basicness check" of
Path.basic was required?
Moreover, users have occasionally run into problems by using odd names
for formal items that later become file-system paths, notably theory and
session names. In Isabelle2018 I have introduced the concept of a
"system_name" (with predicates/parsers in Isabelle/ML and
Isabelle/Scala). Thus tools can make their user-facing syntax a bit more
robust.
Maybe I should also tighten this to exclude the special name "aux",
"con", "nul" for Windows file systems, see also
https://docs.microsoft.com/en-us/windows/desktop/fileio/naming-a-file
Makarius
Email Gateway (Aug 22 2022 at 18:50):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
The strictness of Path.basic is some kind of sanity check: when
composing a path of various sources, you can assert that no accidental
".." or "/" will smash your implicit assumptions about the resulting tree.
Florian
signature.asc
Email Gateway (Aug 22 2022 at 18:54):From: Makarius <makarius@sketis.net>
I have done that for the next release -- presumably Isabelle2019 (June
2019). The relevant change is Isabelle/415dc92050a6.
Moreover I have tightened Path.T and system_name according to
https://docs.microsoft.com/en-us/windows/desktop/fileio/naming-a-file
(see Isabelle/57ff523d9008 and Isabelle/adb52af5ba55).
Makarius
Last updated: Apr 18 2024 at 20:16 UTC