leanprover
RFC: the Lean language server could not connect
I opened the vscode software, but the Lean language server could not connect successfully. Because the area is restricted. I use a proxy to access the Internet and configure the proxy address on the vscode client. But it still appears that the Lean language server cannot be successfully connected. What should I do?
The language server is a local application, it does not need to connect to the internet.
What makes you think that the language server is not working? The InfoView seems to work just fine (it displays the expected type at the text cursor position), and that requires the language server.
Is the problem here that you are expecting lake run to run the Lean executable that you built? Assuming that your lakefile.lean is set up correctly to build executables, you can execute your program by navigating to .lake/build/bin and running the executable that lake build produced in that folder.
