Windows Support

[yangky11]

I'm not sure how important it is to support Windows (how many Lean users actually use Windows?)

[alreadydone]

Is it difficult to support? I just got a Windows laptop with 4060 (8GB VRAM) GPU last night, and have successfully run 4bit-quantized Mistral 7B via https://github.com/oobabooga/text-generation-webui#one-click-installers and also via https://github.com/LostRuins/koboldcpp#windows-usage, so I can certainly help testing.

[yangky11]

Currently, the main non-Windows-compatible part is when we want a system function that's not supported by Lean (e.g., to count the number of CPUs, or check if the system is ARM64 or X64), we use some Unix-specific workaround (e.g., uname -m). It should definitely be possible to implement a separate version for Windows.

Thanks for offering to test it. We'll work on it and post updates here.

[yangky11]

BTW, Windows with WSL has already been tested to work.

[teorth]

I managed to get Copilot working on Windows (WSL) after about two hours of effort, in large part because I missed the very important acronym "WSL" in the list of requirements. My workflow ended up being as follows:

• Create a new Lean project
• Diagnose, then find a workaround for, an unrelated bug in lake update for Windows (see https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60lake.20update.60.20broken.20on.20Windows.20.28.3F.29 )
• Work out how to add a "package configuration option" to lakefile.lean
• Install Git LFS
• Attempt to install LeanCopilot
• Manually fix two lines of code in the LeanCopilot lakefile.lean to make it run
• Realize that LeanCopilot does not actually support Windows, but rather Windows WSL
• Install Windows WSL
• Install Lean for Ubuntu
• Install VSCode for Ubuntu
• Work out how to iteratively install dependencies in Ubuntu to complete VSCode installation
• Install Lean plugin for VSCode
• Create a new Lean project in Ubuntu
• Delete (or move to cloud) multiple files due to low disk space
• Attempt to install LeanCopilot
• Install Git LFS for Ubuntu
• Finally get LeanCopilot to install
• Uninstall Lean plugin (as it was for Lean 3); install Lean 4 plugin instead

I think it would help users who are not already experienced in installing open source software to (a) clarify exactly how to add a package configuration option to lakefile.lean (viz., by placing it inside the "package {...}" fragment of that lean file), and (b) emphasizing that the software does not directly run in Windows itself (it took me about an hour of trying to "debug" the lean file (which was not reporting a "run_io" feature) until finally hitting the "panic! "Windows is not supported"" error message).

[yangky11]

Hi @teorth,

Thank you for your valuable suggestions. I have incorporated them into the current README.

LeanCopilot doesn't support native Windows because Lean didn't have cross-platform implementations for some features we need, so we resorted to workarounds that are Unix-specific. However, maybe that's no longer the case with the most recent version of Lean. If so, it may make sense to support Windows directly. @Peiyang-Song Can you take a look when you get a chance?