## Stream: general

### Topic: Visual Studio Code: "spawn ENOTDIR" error

#### Bryan Gin-ge Chen (Mar 06 2021 at 17:06):

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

#### François Sunatori (Mar 06 2021 at 20:02):

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 (Mar 06 2021 at 20:22):

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 (Mar 06 2021 at 20:37):

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 (Mar 06 2021 at 20:48):

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 (Mar 06 2021 at 21:00):

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 (Mar 06 2021 at 21:03):

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 (Mar 06 2021 at 21:07):

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

#### François Sunatori (Mar 06 2021 at 21:22):

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 (Mar 06 2021 at 21:22):

hooray for moving backwards :) -- glad it helped

Last updated: May 12 2021 at 23:13 UTC