`lib.path.hasPrefix`: init #237610

infinisil · 2023-06-13T18:43:36Z

Description of changes

Adds a function to lib.path:

lib.path.hasPrefix :: Path -> Path -> Bool: Whether the first path is a prefix of the second path:
```
lib.path.hasPrefix ./. ./lib
-> true
```

This is split off from #210423, relating to other work in the path library effort.

This work is sponsored by Antithesis ✨

Things done

Wrote docs
Wrote tests

With removePrefix introduced in a future commit this law can then be used to derive removePrefix p (append p s) == subpath.normalise s => (wrap with append) append p (removePrefix p (append p s)) == append p (subpath.normalise s) => (append is not influenced by subpath normalisation) append p (removePrefix p (append p s)) == append p s => (substitute q = append p s) append p (removePrefix p q) == q Not included in the docs because it's not that important, just shows that the first statement is more general than the second one (because this derivation doesn't work the other way)

fricklerhandwerk

Nice!

roberth · 2023-06-15T16:21:31Z

lib/path/default.nix

+
+  - Equivalent to whether some subpath exists that can be appended to the first path to get the second path:
+
+        hasPrefix p q <-> exists s . append p s == q


Suggested change

hasPrefix p q <-> exists s . append p s == q

hasPrefix p q

=

∃s. (append p s == q)

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

Suggested change

hasPrefix p q <-> exists s . append p s == q

hasPrefix p q

==

∃s. (append p s == q)

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 😂

infinisil · 2023-06-15T17:34:14Z

lib/path/default.nix

+  Whether the second path is a prefix of the first path, or equal to it.
+  Throws an error if the paths don't share the same filesystem root.


Suggested change

Whether the second path is a prefix of the first path, or equal to it.

Throws an error if the paths don't share the same filesystem root.

Whether the first path is a prefix of the second path.

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)

jtojnar · 2023-06-15T20:15:58Z

lib/path/default.nix

@@ -149,6 +173,51 @@ in /* No rec! Add dependencies on this file at the top. */ {
          ${subpathInvalidReason subpath}'';
    path + ("/" + subpath);

+  /*
+  Whether the first path is a prefix of the second path.


Maybe also something like

Suggested change

Whether the first path is a prefix of the second path.

Whether the first path is a component-wise prefix of the second path.

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

Sounds good, applied!

infinisil · 2023-06-15T20:47:54Z

lib/path/default.nix

+        assert assertMsg
+        (path1Deconstructed.root == path2Deconstructed.root) ''
+          lib.path.hasPrefix: Filesystem roots must be the same for both paths, but paths with different roots were given:
+              first argument: "${toString path1}" with root "${toString path1Deconstructed.root}"
+              second argument: "${toString path2}" with root "${toString path2Deconstructed.root}"'';


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?

infinisil requested a review from roberth June 13, 2023 18:43

infinisil requested a review from edolstra as a code owner June 13, 2023 18:43

This was referenced Jun 13, 2023

Path library functions #210426

Closed

lib.path.hasPrefix, lib.path.removePrefix: init #210423

Closed

ofborg bot added 10.rebuild-darwin: 0 This PR does not cause any packages to rebuild on Darwin 10.rebuild-linux: 1-10 labels Jun 13, 2023

fricklerhandwerk approved these changes Jun 13, 2023

View reviewed changes

mweinelt added the 12.approvals: 1 This PR was reviewed and approved by one reputable person label Jun 14, 2023

roberth reviewed Jun 15, 2023

View reviewed changes

infinisil force-pushed the lib.path.hasPrefix branch from dd30838 to 78b24ab Compare June 15, 2023 16:30

infinisil commented Jun 15, 2023

View reviewed changes

infinisil force-pushed the lib.path.hasPrefix branch from 78b24ab to 0042d58 Compare June 15, 2023 17:51

yurrriq approved these changes Jun 15, 2023

View reviewed changes

jtojnar reviewed Jun 15, 2023

View reviewed changes

lib.path.hasPrefix: init

592213a

infinisil force-pushed the lib.path.hasPrefix branch from 0042d58 to 592213a Compare June 15, 2023 20:29

infinisil commented Jun 15, 2023

View reviewed changes

infinisil mentioned this pull request Jun 15, 2023

lib.path.removePrefix: init #238013

Merged

2 tasks

figsoda removed the 12.approvals: 1 This PR was reviewed and approved by one reputable person label Jun 18, 2023

roberth approved these changes Jun 21, 2023

View reviewed changes

roberth merged commit 43be38b into NixOS:master Jun 21, 2023

infinisil deleted the lib.path.hasPrefix branch June 21, 2023 15:01

infinisil mentioned this pull request Jul 19, 2023

lib.lists.{hasPrefix,removePrefix}: init #243511

Merged

2 tasks

infinisil mentioned this pull request Nov 7, 2023

Don't expose all functions in the top-level lib, prefer sub-libraries #266103

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

`lib.path.hasPrefix`: init #237610

`lib.path.hasPrefix`: init #237610

infinisil commented Jun 13, 2023 •

edited

Loading

fricklerhandwerk left a comment

roberth Jun 15, 2023

roberth Jun 15, 2023

infinisil Jun 15, 2023

roberth Jun 15, 2023

infinisil Jun 15, 2023 •

edited

Loading

fricklerhandwerk Jun 15, 2023

infinisil Jun 15, 2023 •

edited

Loading

yurrriq Jun 15, 2023

infinisil Jun 15, 2023 •

edited

Loading

jtojnar Jun 15, 2023

infinisil Jun 15, 2023

infinisil Jun 15, 2023 •

edited

Loading

infinisil Jun 15, 2023

infinisil Jun 15, 2023

roberth Jun 15, 2023

infinisil Jun 15, 2023

roberth Jun 15, 2023

infinisil Jun 15, 2023


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

		hasPrefix p q <-> exists s . append p s == q

		Whether the second path is a prefix of the first path, or equal to it.
		Throws an error if the paths don't share the same filesystem root.

	Whether the second path is a prefix of the first path, or equal to it.
	Throws an error if the paths don't share the same filesystem root.
	Whether the first path is a prefix of the second path.

	Whether the first path is a prefix of the second path.
	Whether the first path is a component-wise prefix of the second path.

lib.path.hasPrefix: init #237610

lib.path.hasPrefix: init #237610

Conversation

infinisil commented Jun 13, 2023 • edited Loading

Description of changes

Things done

fricklerhandwerk left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

infinisil Jun 15, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

infinisil Jun 15, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

infinisil Jun 15, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

infinisil Jun 15, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

`lib.path.hasPrefix`: init #237610

`lib.path.hasPrefix`: init #237610

infinisil commented Jun 13, 2023 •

edited

Loading

infinisil Jun 15, 2023 •

edited

Loading

infinisil Jun 15, 2023 •

edited

Loading

infinisil Jun 15, 2023 •

edited

Loading

infinisil Jun 15, 2023 •

edited

Loading