As an alternative to the MSYS2 setup you can also use the Windows Subsystem for Linux to build Lean there, but edit and debug using Visual Studio Code in Windows.
For the most part setup in WSL is the same as Ubuntu. This document provides additional information on how to setup Windows Visual Studio Code remote debugging into your WSL environment using the lean extension running in WSL.
It is recommended that you setup Ubuntu in WSL 2. Then follow the Dev setup using elan.
Install Visual Studio Code on Windows. Install the VS Code
Remote Development extension from Microsoft. This extension
includes the Remote - WSL extension. Install the lean4 extension but
into the WSL using: Install in WSL: Ubuntu
Type Ctrl+Shift+P and select Remote-WSL: Open Folder in WSL... to
open a folder containing your hello world lean package.
When everything is working you should see something like this with a functioning infoview, syntax coloring and tooltips:
lean4: Could not find Lean version by running 'lean --version'.
Check that the lean program is available in your PATH in your WSL
environment.
Logs are showing up with a windows file path
Check that you have not set a windows path in your
lean4.serverLogging.path Visual Studio Code setting. it is best if
this setting is set as follows:
"lean4.serverLogging.path": "logs"This will result in a logs folder being created inside your lean package folder in the WSL file system.