fix: FileSystem.normalize

[neunenak]

This PR implements the TODO comment here, to handle multiple path separators and the . special character when normalizing file paths.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c92425f98de92a3afc4dfc7b4c0ad754fb19e6f4 --onto b01ca8ee237a1b3c299384e73ad79d424e216a84. (2025-02-07 04:20:32)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c92425f98de92a3afc4dfc7b4c0ad754fb19e6f4 --onto 88664e4a995883877a5d85211a5cfab0a672b5ed. (2025-02-18 09:52:53)

[Kha]

Thanks for the PR, was this implementation taken from some other stdlib? This definitely isn't something we should just reinvent.

[neunenak]

Thanks for the PR, was this implementation taken from some other stdlib? This definitely isn't something we should just reinvent.

Nope, this is just some functionality that I personally needed (and that I saw the TODO comment for), I wrote it by hand based on what seemed reasonable.

[Kha]

Ok, then I don't think we can upstream it as is

[neunenak]

Ok, then I don't think we can upstream it as is

What would be necessary in order to upstream it?

[hargoniX]

The implementation should be based on one from another reputable stdlib such that we do not repeat mistakes that other people have made and already have support for weird edge cases early on. Additionally we should probably have tests to demonstrate that we do indeed manage to handle such edge cases.

[neunenak]

I think the Rust stdlib PathBuf normalization mostly happens in this method: https://doc.rust-lang.org/std/path/struct.PathBuf.html#method.components which might be a good guide for this lean implementation

[Kha]

I've converted this to a draft until that point