lake: seems to accumulate ././'s

[juhp]

Prerequisites

• Check that your issue is not already filed
• Reduce the issue to a minimal, self-contained, reproducible test case.
• Test your test case against the latest nightly release

Description

lake seems to generate extra "././" relative directory prefixes.
It is confusing to read and parse (eg also for Emacs).

Context

I read this new note in the code.
https://github.com/leanprover/lean4/blob/master/src/lake/Lake/Load/Materialize.lean also seems to deal with relPkgDir.
I appreciate that the current implementation works and might be considered safe or foolproof,
and perhaps was introduced also for simple portability? But there ought to be some
straightforward operator to join these paths without introducing redundant ./'s?
I feel it would be great to get rid of all the ./'s altogther if possible.

Steps to Reproduce

$ lean new test
$ cd test
$ vi Main.lean # break compile
$ lake build

Expected behavior:
No "././" or "././././":

$ lake build
✖ [4/8] Building Main
trace: .> LEAN_PATH=./.lake/build/lib LD_LIBRARY_PATH= /usr/lib64/lean4/bin/lean ./Main.lean -R . -o ./.lake/build/lib/Main.olean -i ./.lake/build/lib/Main.ilean -c ./.lake/build/ir/Main.c --json
error: ./Main.lean:5:0: expected '}'
error: Lean exited with code 1
Some required builds logged failures:
- Main
error: build failed

Actual behavior:

lake generates relative directory prefixes like "././" and "././././"

$ lake build
✖ [4/8] Building Main
trace: .> LEAN_PATH=././.lake/build/lib LD_LIBRARY_PATH= /usr/lib64/lean4/bin/lean ././././Main.lean -R ./././. -o ././.lake/build/lib/Main.olean -i ././.lake/build/lib/Main.ilean -c ././.lake/build/ir/Main.c --json
error: ././././Main.lean:5:0: expected '}'
error: Lean exited with code 1
Some required builds logged failures:
- Main
error: build failed

Versions

4.14-rc2
Fedora Linux

Additional Information

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.