lean4-lake-find-dir

Stream: Emacs

[Yury G. Kudryashov]

Moving the discussion from a closed PR https://github.com/leanprover-community/lean4-mode/pull/100

[Yury G. Kudryashov]

@Mekeor Melire , I've run the following test:

(defun lean4-root-dir-p (dir)
  "Check if directory DIR contains \"lakefile.lean\" or \"lakefile.toml\"."
  (or
   (file-exists-p (expand-file-name "lakefile.lean" dir))
   (file-exists-p (expand-file-name "lakefile.toml" dir))))

(message (locate-dominating-file (elt argv 0) #'lean4-root-dir-p))

$ tree find-dir-test
find-dir-test
├── a
│   └── b
│       ├── c
│       │   └── d
│       └── d
└── lakefile.toml

(all the leaves are files, not directories)

$ strace emacs --script find-dir.el find-dir-test/a/b/c/d 2>&1 | grep find-dir-test

There is no find-dir-test/a/b/d in the output, but there are non-existing directories like find-dir-test/.hg etc

[Yury G. Kudryashov]

@Mekeor Melire I'm reading the source code of locate-dominating-file trying to find out why it's looking at these directories.

[Yury G. Kudryashov]

I tried to run it line by line using (debug-on-entry 'locate-dominating-file), but these *.hg/*.git files don't show up in the log.

[Yury G. Kudryashov]

I've tried to paste the strace log, but it's too long. I'll try again when I come home

[Lua Viana Reis]

just a reminder that locate-dominating-file is already being called (and probably more commonly than in lean4-lake.el) at lean4-create-lsp-workspace on lean4-mode.el

[Yury G. Kudryashov]

We should probably merge these 2 searches.

[Yury G. Kudryashov]

:face_palm: I've figured out why strace indicated access to all those .git/.hg files. I didn't reset argv to nil at the end of the script, so Emacs tried to load find-dir-test/a/b/c/d then, and was looking for .git/.hg/.dir-locals etc.

[Yury G. Kudryashov]

tl;dr locate-dominating-file only runs the predicate on the (grand)parent directories, not on any siblings.

[Mekeor Melire]

Thank you very much for investigating, Yury.