Duplicate entries in `lake print-paths`

Stream: lean4

[Denis Gorbachev]

lake print-paths has a lot of duplicates (see below). Is it normal or does it hurt the performance of the commands that iterate over the paths?

lake print-paths | jq
{
  "srcPath": [
    "./lake-packages/std/./.",
    "./lake-packages/Qq/./.",
    "./lake-packages/aesop/./.",
    "./lake-packages/aesop/./.",
    "./lake-packages/Cli/./.",
    "./lake-packages/proofwidgets/./.",
    "./lake-packages/mathlib/./.",
    "./lake-packages/mathlib/./.",
    "./lake-packages/mathlib/./.",
    "./lake-packages/mathlib/./.",
    "./lake-packages/mathlib/./.",
    "./lake-packages/mathlib/./.",
    "./lake-packages/mathlib/./.",
    "././.",
    "././.",
    "././.",
    "././.",
    "././.",
    "././.",
    "././.",
    "././.",
    "././.",
    "././.",
    "././.",
    "././.",
    "././.",
    "././.",
    "././.",
    "././.",
    "././.",
    "././.",
    "././.",
    "././.",
    "././.",
    "././.",
    "././.",
    "././.",
    "././.",
    "././.",
    "././.",
    "././.",
    "././.",
    "././.",
    "././.",
    "././.",
    "././."
  ],
  "oleanPath": [
    "./lake-packages/std/build/lib",
    "./lake-packages/Qq/build/lib",
    "./lake-packages/aesop/build/lib",
    "./lake-packages/Cli/build/lib",
    "./lake-packages/proofwidgets/build/lib",
    "./lake-packages/mathlib/build/lib",
    "./build/lib"
  ],
  "loadDynlibPaths": []
}

[Kevin Buzzard]

Looks a bit like my PATH :-)

[Mac Malone]

@Denis Gorbachev This is "normal". Lake currently does not deduplicate the source path (this is caused by multiple libraries sharing the same source directory). Since the path is generally used for finds which short-circuit when they find a match, it will generally not need to explore every copy. Still, deduplicating is probably a good idea.

[Julian Berman]

Kevin Buzzard said:

Looks a bit like my PATH :-)

Offtopic, but for PATH that's fixable by using -- assuming you're using zsh -- the deduplicating way of modifying your path rather than simple string-based one -- i.e. instead of doing PATH=/foo/bar/baz/:$PATH do path=(/foo/bar/baz $path) -- the latter being an (automatically defined) typeset -U array which automatically changes the former, but uniquifies first. (Of course it likely doesn't matter unless some program you run is somehow bound on how often it loops over PATH, but sometimes it's nice that it's tidy for interactive reasons, and also it's good to know the typeset -U trick for other environment variables -- you can define your own and then get the same behavior).