Refactor lake find dir #100
Conversation
to use built-in locate-dominating-file
It is not used anywhere else but `lean4-lake-find-dir`.
|
Any update here from maintainers? I'm also getting bitten by this infinite loop if we're using a |
|
First of all, thanks for your efforts and the PR. While I do see that it fixes a problem, I'd prefer to continue my work on work-in-progress PR #96 which aims to reach Milestone Three which includes issue #90, and in particular aims to solve this problem in greater depth. Of course, I'm just a contributor, and it's the maintainer @urkud who decides. |
| (when dir | ||
| (or (when (file-exists-p (expand-file-name "lakefile.lean" dir)) dir) | ||
| (lean4-lake-find-dir-in (file-name-directory (directory-file-name dir)))))) | ||
| (defun lean4-root-dir-p (dir) |
lean4-lake.el
Outdated
|
|
||
| (defun lean4-lake-find-dir () | ||
| "Find a parent directory of the current file with file \"lakefile.lean\"." | ||
| "Find a parent directory of the current file with a \"lakefile.lean\" |
There was a problem hiding this comment.
The first line of a docstring should be a full sentence ending with a full stop.
| (and (buffer-file-name) | ||
| (lean4-lake-find-dir-in (directory-file-name (buffer-file-name))))) | ||
| (locate-dominating-file (buffer-file-name) #'lean4-root-dir-p))) |
There was a problem hiding this comment.
I wonder how long locate-dominating-file takes when you open a Lean source file inside a large Nix or Guix store.
There was a problem hiding this comment.
I don't see why this should take a long time in any case. You check for existence of 2 files in each of the (grand)parent directories. It's just 2 stats per a (grand)parent.
|
Hi, I'm going to apply a quick fix taking code from both branches tonight. |
|
I'm sorry for the delay. I'm going to wait for CI, then merge it. |
|
On June 1, 2025 5:18:19 AM GMT+02:00, "Yury G. Kudryashov" ***@***.***> wrote:
@urkud commented on this pull request.
> (and (buffer-file-name)
- (lean4-lake-find-dir-in (directory-file-name (buffer-file-name)))))
+ (locate-dominating-file (buffer-file-name) #'lean4-root-dir-p)))
I don't see why this should take a long time in any case. You check for existence of 2 files in each of the (grand)parent directories. It's just 2 `stat`s per a (grand)parent.
--
Reply to this email directly or view it on GitHub:
#100 (comment)
You are receiving this because you commented.
Message ID: ***@***.***>
@urkud: If you had read the docstring for locate-dominating-file, you would have seen that it has support for a NAME given as function/predicate which is tested on every sibling files on possibly every level.
It makes me sad to see that you don't trust in my review.
|
|
Probably, I've misinterpreted the docstring. I'll try running it with strace tonight. I'm sorry about the tone of my comment. |
Fixes
See also Issue #90