You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I need to program stuff with mingw, so I open vscode on mingw, once 1 window has been opened in mingw, all other windows will inherit this context, so it doesn't matter if they are open on
Context
I have lots of vscodium sessions open, and I would like to have lean open simmulataneously with the others
Steps to Reproduce
go to directory with lean project
run mingw this changes the path, but it should be additive, not substractive
run code .
or
open unrelated project in vscode in mingw.
open vscode normally
open lean project
Expected behavior: [Clear and concise description of what you expect to happen]
LSP starts and works
Actual behavior: [Clear and concise description of what actually happens]
LSP fails and crashes
Versions
[Version of vscode-lean4 (Hover over 'lean4' in the 'Extensions' menu)]
0.0.117
[Output of lean --version in the folder that the issue occured in]
Lean (version 4.2.0-rc4, commit 819b5eaceaa4, Release)
[OS version]
windows 10
Additional Information
I would love to know how to debug LSPs so I can figure out the exact bug, but it's been annoying me for a while. I've never developed a vscode extension
The text was updated successfully, but these errors were encountered:
Description
I need to program stuff with mingw, so I open vscode on mingw, once 1 window has been opened in mingw, all other windows will inherit this context, so it doesn't matter if they are open on
Context
I have lots of vscodium sessions open, and I would like to have lean open simmulataneously with the others
Steps to Reproduce
mingw
this changes the path, but it should be additive, not substractivecode .
or
vscode
normallyExpected behavior: [Clear and concise description of what you expect to happen]
LSP starts and works
Actual behavior: [Clear and concise description of what actually happens]
LSP fails and crashes
Versions
[Version of vscode-lean4 (Hover over 'lean4' in the 'Extensions' menu)]
0.0.117
[Output of
lean --version
in the folder that the issue occured in]Lean (version 4.2.0-rc4, commit 819b5eaceaa4, Release)
[OS version]
windows 10
Additional Information
I would love to know how to debug LSPs so I can figure out the exact bug, but it's been annoying me for a while. I've never developed a vscode extension
The text was updated successfully, but these errors were encountered: