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?

[Richard Copley]

@Yury G. Kudryashov, this was #48. The issue persists, and I've just added an up-to-date reproducer to the PR. Can you review it, please? No rush, obviously.

[Yury G. Kudryashov]

Thanks! Merged

[Yury G. Kudryashov]

If you have other PRs to lean4-mode you want to get merged fast, then please ping me here (with @ mention) on Zulip.

[Richard Copley]

Thanks!

[Yury G. Kudryashov]

@Richard Copley It looks like you know about Emacs more than I do. Recently, I tried Emacs (v30.0.50)+LSP-mod(20240501.110)+lean4-mode(master) on a new machine, and I'm getting the following error whenever I open a .lean file:

LSP :: The following servers support current file but do not have automatic installation: lean4-lsp
You may find the installation instructions at<...>

[Yury G. Kudryashov]

Do you know why this can appear?

[Yury G. Kudryashov]

I manually run (require 'lean4-mode) before opening the file to make sure that it's already loaded.

[Richard Copley]

I've seen it, but not recently. If I'm remembering right, I don't think there was a bug. Some little thing, like making sure elan is on the path (the environment variable in the emacs process's environment, and probably also the exec-path elisp variable). Does Meta-Shift-! lake --version RET show something sensible? (It needs to be after 3.1.0. Current version is 5.0.0.)

There is a strange piece of code in that remembers the path to the server in a variable lean4-rootdir when first starting the server. To clear the cache (setq lean4-rootdir nil) (or kill Emacs).

[Richard Copley]

That code was touched in #51 so if there's a bug now, that's where to look first. Let me know

[Yury G. Kudryashov]

Indeed, elan was not in the PATH of emacs (because it was started by systemd). Thanks!

[Yury G. Kudryashov]

BTW, did you ever try running Emacs+Lean on a remote repository (e.g., via tramp)?

[Yury G. Kudryashov]

I'm running it in a terminal via mosh for now.

[Richard Copley]

Yury G. Kudryashov said:

BTW, did you ever try running Emacs+Lean on a remote repository (e.g., via tramp)?

I always assumed it wasn't worth trying, but actually it probably should be possible. It doesn't seem to work though. (That's with Emacs on Windows and a project in Linux (on WSL), via tramp and plink/ssh.) I usually work locally but if not, I use a terminal too.

[Richard Copley]

@Yury G. Kudryashov, lean4-mode PR 64 handles the switch to TOML config files, by searching for "lean-toolchain" instead of "lakefile.lean" when locating the project root directory, which is what the VS Code extension does I think. One could argue it's a fix for PR 48. Can you review please?

[Yury G. Kudryashov]

Thanks! Merged.