Zulip Chat Archive

Stream: new members

Topic: Could not find "Select Default Shell"

AnduinHS (Aug 31 2021 at 13:53):

My lean on VS Code somehow does not work (which means it used to work).(For example, after I entering #eval 1+1 , the green line does not appear underneath #eval 1+1, and hovering the mouse over it I could not see 2 displayed. And it says "'Lean.DisplayGoal' not found")(maybe because I have deleted the previous opening settings(JSON)). I tried to follow https://leanprover-community.github.io/install/windows.html again to make it work. All other things seemed great. However, When I type Select Default Shell, I could not find it. 1.PNG So I have tried Select Default Profile and adds Git Bash to it. However, it doesn't work.
Should I unist and re-install VS Code?

Johan Commelin (Aug 31 2021 at 13:56):

Do you use VScode for other things?

Johan Commelin (Aug 31 2021 at 13:57):

If not, re-installing it seems harmless, so I would try it.

AnduinHS (Aug 31 2021 at 15:33):


Alex J. Best (Aug 31 2021 at 18:01):

I think VScode has changed the name of the select default shell option to select default profile (microsoft/vscode#118790), I've PRed the fix to the site at leanprover-community/leanprover-community.github.io#199

AnduinHS (Sep 01 2021 at 16:06):

Now I know my problem. My DNS(or sth else) was reset by Chinese "Great FireWall". It says "info: downloading installer
curl: (56) OpenSSL SSL_read: Connection was reset, errno 10054
elan: command failed: curl -sSf https://github.com/leanprover/elan/releases/latest
". I should find some other way or have another in some other time.

Last updated: Dec 20 2023 at 11:08 UTC