relative filepath normalization

Stream: lean4

[James Gallicchio]

is there a quick way to resolve relative paths to absolute file paths in a way that also gets rid of . and .. in the paths? I'm trying to get the actual parent of a file, e.g. the parent of something/./file should be something, not something/.

[Arthur Paulino]

Doesn't FilePath.normalize resolve that?

[Eric Wieser]

Do you want to resolve symlinks or not? Sometimes foo/bar/../baz can resolve to definitely_not_foo/baz.

[James Gallicchio]

hm, weird

[James Gallicchio]

any symlink behavior would be fine

[James Gallicchio]

Arthur Paulino said:

Doesn't FilePath.normalize resolve that?

no, it only normalizes parent//child to parent/child :/

[Mario Carneiro]

normally you would use something called realpath for this

[Mario Carneiro]

and oh hey look -> docs4#IO.FS.realPath

[James Gallicchio]

aha! that looks like exactly what I want, thanks mario

[Mario Carneiro]

that will do what Eric says though, if foo/bar is a symlink to definitely_not_foo/qux then foo/bar/../baz resolves to definitely_not_foo/baz

[Mario Carneiro]

filesystems are fun, you never know where you might end up

[James Gallicchio]

I think that's the behavior I'd want anyways, so that is fine with me

[James Gallicchio]

(I'm traversing the files in the same directory as a given file, so symlink'd parents are ~irrelevant)

[Mario Carneiro]

why would you need to use .. for that?

[James Gallicchio]

I'm not using .. to get the parent -- rather, I might have the relative file ././. in which case it is not straightforward to get the parent directory to traverse :P

[James Gallicchio]

I suspect it is good practice to just always call realPath at top-level so all filepaths provided on the command line are resolved early.

[Reid Barton]

Normally . is not a file.

[James Gallicchio]

err, sorry, ./././anActualFile :joy:

[James Gallicchio]

somewhat relatedly -- is there a particular reason for what stuff ends up in IO.FS versus System.FilePath? both have IO functions that take a single filepath argument. I suspect it is arbitrary and just follows the file structure of where things are declared?

[Reid Barton]

But if you have ./././anActualFile then you can strip off the last component and use ././. as the directory to read, no?

[Reid Barton]

I don't see why this actually requires anything like realpath

[James Gallicchio]

That is very true, and I don't remember why it was an issue. I should probably not be coding in the middle of the night like this.

[James Gallicchio]

I guess the weirdness with parents only comes up if p is a directory, since then p could be ./. and its path-parent . is not its filesystem parent ..

[Mario Carneiro]

Finding the sibling of a directory is necessarily "get the parent and then get the other child" though, so appending ../otherChild looks like the most correct thing. After all, the root is a directory too, what is the sibling of /?

[James Gallicchio]

Totally -- it is cleaner and probably more correct to just do (file / "..").walkDir (fun p => ...) instead of actually getting the parent. Thanks everyone!

[James Gallicchio]

wait, that does not make sense

[James Gallicchio]

because file/.. does not exist

[James Gallicchio]

ah, but there is the withFile function or whatever

[James Gallicchio]

we are back on track everyone

[James Gallicchio]

file.withFileName ".." is quite an odd way to spell file.parent

[James Gallicchio]

and it does sort of beg the question whether file.parent should return .instead of none in the case a file doesn't have multiple components. but they are both useful functions, so it is whatever

[Reid Barton]

Don't you want file.withFileName "."?

[James Gallicchio]

yup... saving me from painful debugging later, thank you