Zulip Chat Archive

Stream: general

Topic: Visual Studio Code: "spawn ENOTDIR" error


view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 !

view this post on Zulip Julian Berman (Mar 06 2021 at 21:22):

hooray for moving backwards :) -- glad it helped


Last updated: May 12 2021 at 23:13 UTC