Visual Studio Code: "spawn ENOTDIR" error

Stream: general

[Bryan Gin-ge Chen]

I don't think I've seen reports of this before. What does elan show say from the command line?

[François Sunatori]

Hi @Bryan Gin-ge Chen this is the output I get for elan show

installed toolchains

---

stable (default)
leanprover-community-lean-3.17.1
leanprover-community-lean-3.18.4
leanprover-community-lean-3.23.0
leanprover-community-lean-3.26.0
leanprover-community-lean-3.27.0

active toolchain

---

stable (default)
Lean (version 3.4.2, commit cbd2b6686ddb, Release)

[Bryan Gin-ge Chen]

OK, that could be reasonable if you ran elan show in a random directory. When you're running VS Code, are you opening a directory containing a Lean project? 99% of the time you want your Lean code to be part of a Lean project. What do you see when you run elan show in the project you're trying to work in?

[François Sunatori]

When in Mathlib I run elan show and get

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

stable (default)
leanprover-community-lean-3.17.1
leanprover-community-lean-3.18.4
leanprover-community-lean-3.23.0
leanprover-community-lean-3.26.0
leanprover-community-lean-3.27.0

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

leanprover-community-lean-3.27.0 (overridden by '/Users/fss/Dropbox/Documents/lean/mathlib/leanpkg.toml')
Lean (version 3.27.0, commit de35266fe596, Release)

[Bryan Gin-ge Chen]

If you open VS Code in that directory and go to "Help > Toggle Developer Tools" do you see any suspicious errors in the console?

[François Sunatori]

This is what I see when I place the cursor in a file
Screen-Shot-2021-03-06-at-16.00.28.png

[Julian Berman]

In case it helps, Google/GH search finds e.g. https://github.com/microsoft/vscode/issues/118164 as a recent (open) VSCode issue (which seems to mention SSH / containers, but one of the comments there at least seems to mention another possible scenario it's showing up in on Big Sur), so if all else fails maybe you try downgrading as shown there and see if it goes away

[Bryan Gin-ge Chen]

Right, if the problem only appeared after you upgraded VS Code then the upgrade seems like a likely culprit.

[François Sunatori]

I'm not sure if I had upgraded (maybe some auto update), but downgrading to 1.53.2 solved it. Thanks for your help @Julian Berman and @Bryan Gin-ge Chen !

[Julian Berman]

hooray for moving backwards :) -- glad it helped