Problems with VSCode extension on WSL

Stream: lean4

[Darylgolden]

Hi, I'm having some trouble getting Lean to work correctly on VSCode with WSL.
Firstly it sometimes takes very long to startup; here's an example with the mathematics_in_lean repository:
image.png
Here the server startup has been going on for around 5 minutes already.
Upon clicking "click for details", the output doesn't seem very informative, here is the full output:

/mnt/c/Users/daryl/Downloads/mathematics_in_lean> curl --version
curl 8.5.0 (x86_64-pc-linux-gnu) libcurl/8.5.0 OpenSSL/3.0.13 zlib/1.3 brotli/1.1.0 zstd/1.5.5 libidn2/2.3.7 libpsl/0.21.2 (+libidn2/2.3.7) libssh/0.10.6/openssl/zlib nghttp2/1.59.0 librtmp/2.3 OpenLDAP/2.6.7
Release-Date: 2023-12-06, security patched: 8.5.0-2ubuntu10.6
Protocols: dict file ftp ftps gopher gophers http https imap imaps ldap ldaps mqtt pop3 pop3s rtmp rtsp scp sftp smb smbs smtp smtps telnet tftp
Features: alt-svc AsynchDNS brotli GSS-API HSTS HTTP2 HTTPS-proxy IDN IPv6 Kerberos Largefile libz NTLM PSL SPNEGO SSL threadsafe TLS-SRP UnixSockets zstd

/mnt/c/Users/daryl/Downloads/mathematics_in_lean> git --version
git version 2.43.0

/mnt/c/Users/daryl/Downloads/mathematics_in_lean> lean --version
Lean (version 4.20.0, x86_64-unknown-linux-gnu, commit b02228b03f65, Release)
/mnt/c/Users/daryl/Downloads/mathematics_in_lean> elan --version
elan 4.1.2 (58e8d545e 2025-05-26)

/mnt/c/Users/daryl/Downloads/mathematics_in_lean> lean --version
Lean (version 4.20.0, x86_64-unknown-linux-gnu, commit b02228b03f65, Release)
/mnt/c/Users/daryl/Downloads/mathematics_in_lean> lake --version
Lake version 5.0.0-b02228b (Lean version 4.20.0)
/mnt/c/Users/daryl/Downloads/mathematics_in_lean> lake serve -- /mnt/c/Users/daryl/Downloads/mathematics_in_lean

[Darylgolden]

image.png
After it loads the file again takes very long to load, sometimes up to 10 minutes. Again I'm not sure how I can get more detailed debug information here.

[Sebastian Ullrich]

I do not know why you are using WSL but filesystem performance when accessing the Windows mount is a well-known issue, you'll want to use a separate copy of the repo: https://stackoverflow.com/a/68974497

[Darylgolden]

I'm using WSL because there's an extension I'm using that doesn't work properly on Windows. It feels pretty strange that the filesystem performance can cause such a slow down, but I'll try that, thanks!