Elan + Lean4 Extension

Stream: general

[Sidharth Hariharan]

Hi! I am having a small technical problem and was hoping someone here would be able to help me fix it.

I just updated my elan version and for some reason my Lean4 VS Code extension seems to have stopped working. I'm on Lean 4.15.0 and Elan 3.1.1 and use a MacBook Air M2 with OS Sequoia 15.2. Things like lake exe cache get and lake build seem to be working fine, but I can no longer see the orange bars in my file. The infoview just says "No info found" and has a little thing circling next to the file name. Given that lake seems to be working fine, I am assuming something about my elan update somehow broke my extension. I do not seem to be getting errors in my editor, either: for instance,

example (A B : Prop) : A → A := by
  exact h1

does not give me any errors in my editor even though this code is incorrect. lake build, however, catches it out, just as one would expect it to.

Does anyone know how I can fix it? Many thanks in advance!

[Mauricio Collares]

What's your Lean 4 VS Code extension version?

[Sidharth Hariharan]

0.0.186, last updated today

[Sidharth Hariharan]

Interestingly, I only seem to be having this problem when I open up one specific repository. The repository works for other people, and worked perfectly for me before I updated elan.

[Kevin Buzzard]

Try deleting .lake and then doing lake exe cache get! but I'm not optimistic that this will fix it.

[Bhavik Mehta]

After having tried a bit to fix it on Sidharth's laptop - since lake build works fine, I'm not sure how much that'll help! Lean is working fine from command line in the repo, just not Lean in the extension

[Kevin Buzzard]

Uninstall and reinstall the extension? Disable Lean 3 extension?

[Sidharth Hariharan]

Doesn't seem to be working... the Lean3 one is disabled and i've tried uninstalling and reinstalling as well as restarting the extension.

[Sebastian Ullrich]

What does https://github.com/leanprover/vscode-lean4/blob/master/vscode-lean4/manual/manual.md#collecting-setup-information show in that project?

[Sidharth Hariharan]

Here's what it says:

Operating system: Darwin (release: 24.2.0)
CPU architecture: arm64
CPU model: 8 x Apple M2
Available RAM: 17.18 GB

VS Code version: Reasonably up-to-date (version: 1.96.2)
Lean 4 extension version: 0.0.186
Curl installed: true
Git installed: true
Elan: Reasonably up-to-date (version: 3.1.1)
Lean: Reasonably up-to-date (version: 4.15.0)
Project: Valid Lean project (path: path/to/my/repo)

---

Elan toolchains:

installed toolchains
--------------------

stable
leanprover-community/lean:3.44.1
leanprover-community/lean:3.48.0
leanprover-community/lean:3.49.1
leanprover-community/lean:3.50.1
leanprover-community/lean:3.50.3
leanprover-community/lean:3.51.1
leanprover/lean4:nightly (default)
leanprover/lean4:nightly-2023-02-04
leanprover/lean4:nightly-2023-05-31
leanprover/lean4:nightly-2024-04-24
leanprover/lean4:stable
leanprover/lean4:v4.10.0-rc2
leanprover/lean4:v4.11.0-rc2
leanprover/lean4:v4.13.0-rc3
leanprover/lean4:v4.14.0-rc2
leanprover/lean4:v4.15.0
leanprover/lean4:v4.15.0-rc1

leanprover/lean4:v4.4.0-rc1
leanprover/lean4:v4.6.0-rc1
leanprover/lean4:v4.8.0-rc2

active toolchain
----------------

leanprover/lean4:v4.15.0 (overridden by 'path/to/my/repo/lean-toolchain')

Lean (version 4.15.0, x86_64-apple-darwin22.6.0, commit 11651562caae, Release)

[Mauricio Collares]

It's not the cause of your problem, but you're using a x86_64 elan, which is not ideal unless you still plan on using Lean 3

[Mauricio Collares]

You can uninstall your current elan (probably via homebrew) and then follow the instructions at https://github.com/leanprover/elan to get a native version

[Bhavik Mehta]

That's exactly what caused this! We uninstalled elan from brew and asked the extension to install it again

[Mauricio Collares]

Try removing ~/.elan and asking the extension to install it one more time? I'm worried that the new (aarch64) elan together with the old x86_64 toolchains might be a problem

[Mauricio Collares]

If you want to gather more data, you can also see if elan toolchain uninstall leanprover/lean4:v4.15.0 (and letting elan reinstall it) is enough to fix this particular project/toolchain

[Bhavik Mehta]

Mauricio Collares said:

If you want to gather more data, you can also see if elan toolchain uninstall leanprover/lean4:v4.15.0 (and letting elan reinstall it) is enough to fix this particular project/toolchain

I believe we did this too, but it's probably worth trying again

[Sidharth Hariharan]

Mauricio Collares said:

Try removing ~/.elan and asking the extension to install it one more time? I'm worried that the new (aarch64) elan together with the old x86_64 toolchains might be a problem

I did this, and it removed all traces of elan and Lean. I then reinstalled them via the extension. Unfortunately, I'm still having a problem with this particular repository... other repositories seem to be completely fine, even after this uninstalling and reinstalling. For reference, I'm pasting my setup information again:

Operating system: Darwin (release: 24.2.0)
CPU architecture: arm64
CPU model: 8 x Apple M2
Available RAM: 17.18 GB

VS Code version: Reasonably up-to-date (version: 1.96.2)
Lean 4 extension version: 0.0.186
Curl installed: true
Git installed: true
Elan: Reasonably up-to-date (version: 3.1.1)
Lean: Reasonably up-to-date (version: 4.15.0)
Project: Valid Lean project (path: path/to/my/repo)

---

Elan toolchains:

installed toolchains
--------------------

leanprover/lean4:stable (default)
leanprover/lean4:v4.14.0-rc2
leanprover/lean4:v4.15.0
leanprover/lean4:v4.15.0-rc1

active toolchain
----------------


leanprover/lean4:v4.15.0 (overridden by 'path/to/my/repo/lean-toolchain')

Lean (version 4.15.0, arm64-apple-darwin23.6.0, commit 11651562caae, Release)

In particular, the architecture mentioned in the Lean version is now the right one.

[Kim Morrison]

And you've tried deleting and recloning the relevant repository after all that reinstalling?

[Mauricio Collares]

If deleting and recloning doesn't work, is there anything weird about the path/to/my/repo part, like spaces, non-ASCII characters, or something network-related (e.g. NFS mount or inside a Dropbox folder)?

[Sidharth Hariharan]

I've recloned the repo into a folder with a less weird path (which is where all my other projects are) and now I finally have those coveted orange bars. Infoview seems to be working fine. Thank you for your help!

[Marc Huisinga]

Which aspect of the path that the project used to be in was "weird"?

[Sidharth Hariharan]

I don't think cloud storage is the problem: all my repos are on OneDrive, and this is the first time I've faced this sort of problem (at least since moving to Lean 4). I don't think a space in the path is a problem, because all my non-junk files on OneDrive are inside a folder whose name has a space in them. My first thought was that it was because my parent directory—the one into which I had cloned my repo—had a space in it, because for all my other repos, the immediate parent directory didn't have any spaces in them. However, when I created a dummy directory called Trial inside this directory and cloned my project in there, it still didn't work. My next thought is that the problem stems from the fact that the parent directory had brackets in the name. The reason for this is that the repo is for a course I'm taking, and I always add the course number to the course name in brackets for ease of reference. This is consistent with the fact that when I created a directory with the same name inside my standard Lean project directory and cloned the repo inside that folder, the same issue came up again. I might play around with it a little more at some point, but based on this preliminary experimentation, I suspect that the brackets are the reason it wasn't working.

[Mauricio Collares]

I can reproduce with:

$ mkdir "[Test]"
$ cd "[Test]"
$ git clone https://github.com/b-mehta/formalising-mathematics-notes
$ cd formalising-mathematics-notes/
$ lake exe cache get

When I open Section01logic/Sheet1.lean in VS Code, the Infoview permanently shows a "Restart file" button and "No info found" regardless of where the cursor is. {Test} also fails, (Test) works. All three work in Emacs.

[Kim Morrison]

Thanks for tracking this down! @Sidharth Hariharan or @Mauricio Collares, would one of you mind opening a bug report for that? (I know that some people will tear their hair out at the thought of using brackets in directory names, but ... it happens!)

[Marc Huisinga]

No need to create an issue, I think I already know what the problem is.

[Marc Huisinga]

vscode-lean4#566

[Bhavik Mehta]

Woah, thanks for this! And thanks Mauricio for thinking about the path - I'd never have considered that to be relevant!

[Mauricio Collares]

Marc Huisinga said:

vscode-lean4#566

Thanks! I tested 0.0.189 and it works for [Test], but unfortunately not yet for {Test}. VSCodium versions:

Version: 1.96.2
Release: 24355
Commit: 29b115fb6fb418b80e93102cb177e06803e7b907
Date: 2024-12-21T00:45:47.611Z
Electron: 32.2.7
ElectronBuildId: undefined
Chromium: 128.0.6613.186
Node.js: 20.18.1
V8: 12.8.374.38-electron.0
OS: Linux x64 6.1.0-23-amd64

[Mauricio Collares]

I guess it's also good to try a directory named {a,b}

[Marc Huisinga]

Great, looks like the escape function from the npm glob package doesn't actually escape globs correctly. vscode-lean4#569

[Mauricio Collares]

The previous fix seems like the idiomatic JS way to do it, but it is somewhat amusing. To recap, to escape globs in JS, one installs the glob npm package, which defers this functionality to the minimatch npm package, which has a one-line function escape which just does regexp substitution with the wrong regexp.

[Mauricio Collares]

Thanks for inlining and fixing the regexp!

[Marc Huisinga]

FWIW, it looks like this issue still isn't entirely fixed as @Mauricio Collares figured out, since paths like {Test don't work (though {Test} does). The glob escaping seems to work fine AFAICT, so my next guess would be that there's another issue in VS Code's language client library or perhaps even in VS Code itself. I've created vscode-lean4#570 to track this.

Perhaps it's best to just wait until the next language client release that removes the need for glob escaping entirely and see if we can figure this out fully then.