A good definition of ∃ is easy to find with a search engine nowadays, whereas exists is imaginary syntax that's impossible to find.

I think it's ok to use = in meta syntax.
I had to look up that <-> is iff. Maybe I'm dumb, because I did take math courses in uni... Anyway, the search result for <-> isn't as good as ∃, for what it's worth, but most of all, we don't need this operator.

Or double equal sign like the preceding law in the diff

I think the implementation could perhaps be optimized for the true case, because then you don't need to find the other root, or allocate path component lists, but you'd have to measure it. Something for a later PR maybe.

So just the suggestion (either one) and then lgtm

I think I'd rather remove the extra newlines to be consistent with the rest of this file, sounds good otherwise!

I'm curious what people think, so unscientific twitter poll.

We could also do this to avoid the $\exists$:

Equivalent to whether some subpath s exists that can be appended to the first path to get the second path:

hasPrefix p q == (append p s == q)

But also, the two =='s do look a bit weird, I think something like <-> would be better, but yeah it's not that well known, I don't mind either way

How about <=> or $\iff$?

<=> is what I would expect.

How about just having this, no additional formula:

hasPrefix p q is only true if q == append p s for some subpath s.

(latest commit uses this now)

I think that's best, overall.

Though personally any of the notation above is fine too. I've finally stopped overriding \iff from <=> to <-> in LaTeX 😂

It was the wrong way around, and the filesystem root thing really doesn't need to be mentioned, since you can't even produce paths that would cause that error in current Nix.

(applied in latest commit)

Maybe also something like

To make it clear that hasPrefix /foo/b /foo/bar == false.

Sounds good, applied!

This should not cause the function to fail, it should instead just return false (Edit: I don't think so anymore, see #237610 (comment))

This is all a bit messed up, because the reason this check is here is because we decided to limit the number of assumptions the path library makes to a minimum, see the design document. Notably we don't assume that there's only one filesystem root, meaning that theoretically paths could have no common ancestor. The reason for this is to ensure compatibility with how NixOS/nix#6530 implements lazy paths, introducing a way to have multiple filesystem roots.

But it's kind of ridiculous, Nixpkgs shouldn't have to ensure forwards compatibility with a potential future Nix version. We can't even test this code here right now without going through hoops!

On the other hand, having this check here ensures that we won't have any buggy behavior in case the above PR gets merged like that, and it doesn't cause any problems if the PR isn't merged either, so it's harmless and just a safety measure.

So because of that I'd say: Let's continue without the assumption of singular filesystem roots and have this check here.

Regarding throwing vs not throwing. I think it should definitely throw for now because:

• We can always remove throws afterwards, it's backwards compatible
• The notion of different filesystem roots is very unexplored, we aren't sure what the semantics should be like yet
• I can imagine however that in most cases, this would indicate an user error, and it would be better to notify the user instead of "failing" silently
• Code that needs to ensure it doesn't throw can still check whether the two paths have the same filesystem root beforehand

So in conclusion, no change is necessary here imo.

And I did test this code path at least locally:

❯ nix run github:edolstra/nix/lazy-trees -- repl -f lib
Welcome to Nix 2.17.0pre20230602_3c4d678. Type :? for help.

Loading installable ''...
Added 411 variables.
nix-repl> p = (builtins.fetchTree { type = "git"; url = ./.; }).outPath

nix-repl> path.hasPrefix p ./.                                         
error: lib.path.hasPrefix: Filesystem roots must be the same for both paths, but paths with different roots were given:
    first argument: "/home/tweagysil/antithesis/nixpkgs/" with root "/home/tweagysil/antithesis/nixpkgs/"
    second argument: "/home/tweagysil/antithesis/nixpkgs" with root "/"

• We can always remove throws afterwards, it's backwards compatible

We'd break code that relies on this function for input validation. Just because it works for valid inputs doesn't mean that changing it won't lead to hard to troubleshoot problems for others. Basically your third point, but with a time / change aspect added.

True, though I'd argue that backwards compatibility conventionally only means "If it worked before it should work in the future", a one-way implication, so something not working now doesn't mean it will continue not working in the future.

But it's kind of ridiculous, Nixpkgs shouldn't have to ensure forwards compatibility with a potential future Nix version. We can't even test this code here right now without going through hoops!

I kind of agree, but like you, I care too much about the future of lib.

The hoops are packaging that branch and using it in lib/release.nix. However, that would be irresponsible because of how broken it is. While I am confident that this particular behavior is good, users might adapt their programming to behaviors that are bad. Paths are already confusing to users, so we should discourage all adaptation to path related behaviors that will not be released.

Users won't run into this error anyways right now though, the PR isn't merged yet, or might not even get merged with this behavior ever.

And if it were to get merged, I still think throwing an error here is better than returning false for the other reasons at least. Whether we want to change this behavior in the future and whether we should consider that backwards incompatible should be left for then, I don't think it makes sense to discuss this much here.

Do you agree that the code is fine as is?