Emacs lean4-mode in package directories

Stream: general

[Richard Copley]

Emacs lean4-mode and lake build cooperate well while editing the files of the top-level project, but visiting a file in a referenced package causes that file and all its dependencies to be rebuilt (and then rebuilt again, when returning to the top-level project). It's a pain! Anyone know why this happens, and how to work around or fix it?

[David Renshaw]

Yeah, I'm noticing this behavior too. It seems to have been a recent regression.

[Yury G. Kudryashov]

If this is a recent regression, then you can try to git bisect it and find the offending commit.

[Richard Copley]

Great idea. But lsp-mode, lean4-mode and Lean 4 itself all change rapidly enough that finding compatible combinations is not a simple matter. I tried quite hard to get a bisection to work (I won't bore you with the details), and in my judgement it's not worth trying harder. It would be easier to get to the bottom of this the old-fashioned way, by understanding what goes wrong. At a guess, it's the lean4-mode developers who are best placed to do that, assuming they're interested.

[David Renshaw]

I believe the regression was in mathlib/lake/lean4, not in lean4-mode

[Richard Copley]

Do you know if there is a similar issue in VS Code?

[David Renshaw]

The behavior I'm seeing:

1. I have a project that depends on mathlib4.
2. I run git clean -xffd to clear out any local cache.
3. I run lake exe cache get to download oleans
4. I run lake build
5. I open a file in the project in emacs. Nothing needs to get rebuilt.
6. The file has a reference to Real.tan. I jump to definition on that.
7. Then I see LSP building a bunch of files in Std, Qq and Aesop, (but not in Mathlib). This takes maybe 20 seconds and then it finishes.

[David Renshaw]

The building that happens in step 7 is what was surprising me, but on further reflection, I'm not so sure it's a regression.

[David Renshaw]

@Buster sounds like maybe you were seeing a behavior that's more pathological than this

[David Renshaw]

I have not updated my lean4-mode or other emacs packages in a while, so it's possible that your issue comes from newer versions of those.

[Richard Copley]

I see the same up to step 6, then visit a file in mathlib (by following a reference, or by using find-file), and its dependencies (in mathlib) get recompiled. Anything from a few files to a few thousand files. I'm not sure I remember a time when this didn't happen. I do keep my packages up to date.

[Sebastian Ullrich]

Does M-x lsp-describe-session indicate that lsp-mode opened a new workspace for the dependency?

[Richard Copley]

Yes, it does.

[Sebastian Ullrich]

That's the issue then. It's not really something lean4-mode has any influence on.

[Richard Copley]

Thanks. Perhaps another angle of approach, then. It's a minor inconvenience to have two workspaces, each with its own lake process, but it wouldn't be so bad if lake did not rebuild the unmodified sources. It uses the same toolchain and reproduces the same oleans with the same filenames. Do you know if there's a good reason for lake to behave that way? If not, maybe it can be fixed.

[Sebastian Ullrich]

The dependency is a valid Lake package in itself, it is not Lake's fault that the editor decided to use two independent workspace roots

[Sebastian Ullrich]

Note that there is no guarantee that the two toolchains are identical, so even with a user-wide Lake cache this could lead to rebuilds

[Richard Copley]

Here's a fix for "lean4-mode.el":

diff --git a/lean4-mode.el b/lean4-mode.el
index 30d3d15..ac71446 100644
--- a/lean4-mode.el
+++ b/lean4-mode.el
@@ -190,6 +190,9 @@ This will allow us to use Emacs when a repo contains multiple lean packages."
   (when-let ((file-name (buffer-file-name))
              (root (vc-find-root (buffer-file-name)
                                  "lakefile.lean")))
+    (while (let ((parent (f-parent root)))
+             (when (string= (f-filename parent) "lake-packages")
+               (setq root (f-parent parent)))))
     (lsp-workspace-folders-add root)))

 ;; Automode List
--

After finding the nearest ancestor directory containing a lakefile, if that directory's parent is named "lake-packages", step up two more directories (and check again).

Your list of workspace folders in ~/.emacs.d/.lsp-session-v1 likely already contains package subdirectories. Restart Emacs and delete that file.

[Yury G. Kudryashov]

Could you please open a PR?