Absolute path in lake require

Stream: lean4

[Patrick Massot]

What is the intended syntax in require foo from path when path wants to start with the root directory. I see that from "/"/"home"/... works but surely this isn’t the intended syntax?

[Mario Carneiro]

Does "/home/..." not work?

[Mario Carneiro]

The point of using the / operator on FilePath is to make the separators OS independent (although I'm not sure how necessary this actually is in modern times since all supported OSs understand / as a directory separator), but absolute paths are by nature OS dependent so there isn't much need for it

[Patrick Massot]

Oh, it works actually. I was misled by the example in the lake README.