VSCode extension doesn't start

Stream: new members

[Agost Biro]

Hi,

I've started learning Lean by working through the exercises in the Mathematics in Lean book and I'm having a bit of trouble with VSCode: the Lean 4 extension fails to start with a "cannot find git" error. It used to work before I restarted VSCode recently and I tried configuring the git path manually in VSCode without success. (Git is installed on the system to be clear.) Has anyone run into this before?

[Marc Huisinga]

A hack to make this work is to add the installation path of Git to the Lean 4: Env Path Extensions setting. But ideally, it would be good to figure out why VS Code can't find Git.

1. How did you install VS Code and Git?
2. How are you launching VS Code (e.g. as administrator or as a regular user, from a terminal, from a shortcut?)
3. Is Git in your PATH? Can you call it from the command line?
4. Does the "Source Control" feature of VS Code still work fine in a Git repository when this error shows up?

[Agost Biro]

Marc Huisinga said:

A hack to make this work is to add the installation path of Git to the Lean 4: Env Path Extensions setting. But ideally, it would be good to figure out why VS Code can't find Git.

1. How did you install VS Code and Git?
2. How are you launching VS Code (e.g. as administrator or as a regular user, from a terminal, from a shortcut?)
3. Is Git in your PATH? Can you call it from the command line?
4. Does the "Source Control" feature of VS Code still work fine in a Git repository when this error shows up?

Hi, thanks for the detailed reply! I just sat down with Lean again and it started working. I suspect the issue was caused by an Xcode update where I had to accept the license before being able to use Xcode Command Line Tools (that bundle Git) again. I didn't notice this immediately, as I'm using a custom installation of Git in my normal workflow.

[Marc Huisinga]

Thanks, that's very helpful information in case someone else has this issue on MacOS in the future!