[x] 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
Prerequisites
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
Expected behavior: No "././" or "././././":
Actual behavior:
lake generates relative directory prefixes like "././" and "././././"
Versions
4.14-rc2 Fedora Linux
Additional Information
Impact
Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.