Zulip Chat Archive
Stream: general
Topic: WSL
Wrenna Robson (Nov 27 2020 at 18:15):
Has any consideration been given to adding instructions for using Lean with a WSL/WSL2 setup? To my mind it's a nicer way of setting things up on Windows (because you can just use the Linux setup chain and you don't need to install Git Bash etc.)
I guess it might go here: https://leanprover-community.github.io/install/windows.html
Wrenna Robson (Nov 27 2020 at 18:17):
(I've been doing it recently and it's really a best-of-all-worlds solution for me!)
Johan Commelin (Nov 27 2020 at 18:25):
If you can write up some foolproof instructions, that would be great! PRs welcome!
(I'm not a Windows user... so I can't judge what works and what doesn't.)
Rob Lewis (Nov 27 2020 at 18:27):
Emphasis on the "foolproof"! The current instructions have been through a few hundred iterations and people still get it wrong all the time. For setups that don't have many users here, it's hard to help when the instructions fail.
Eric Wieser (Nov 27 2020 at 18:42):
Thankfully, lean works just fine for me on windows so I've never had a need to do this.
Wrenna Robson (Nov 27 2020 at 18:45):
I'll see what I can do :)
Wrenna Robson (Nov 27 2020 at 18:45):
It works for me on windows! But I just find Windows plain more annoying to work in in some ways - but also it's what I use on my desktop. WSL's a best of both worlds situation.
Johan Commelin (Nov 27 2020 at 18:46):
I live in a best of one world situtation: :penguin:
Wrenna Robson (Nov 27 2020 at 18:47):
the dream
Wrenna Robson (Nov 27 2020 at 18:47):
WSL2 is basically just magic.
Yakov Pechersky (Nov 27 2020 at 18:55):
I use WSL. But there are some pain points -- the oleans are downloaded into different paths depending on how you set up your mathlib or other repo branch. I end up just using Remote-WSL in VSCode and doing everything there. Mixing Windows and WSL files, and thus, commands that generate them like leanproject, has been a recipe for severe frustration.
Wrenna Robson (Nov 27 2020 at 21:22):
Oh, certainly, I use Remote-WSL
Sebastian Ullrich (Nov 28 2020 at 12:19):
WSL is definitely one solution I thought about before to solve the issue of Windows support for Lean being both hard to implement and still regularly being subpar compared to Unix platforms (because there aren't enough Windows devs around interested in truly polishing the implementation). But the big problem I see with WSL is that the installation is both complex and requires admin privileges, which probably makes it a no-go on e.g. school PCs.
Wrenna Robson (Nov 28 2020 at 16:44):
Yes, although it's getting easier. I suppose in theory some form of virtualization solution might be good.
Matthew Ballard (Oct 15 2021 at 12:08):
I hear a lot of good things about the improvements to WSL on windows 11. Is anyone using Lean on it?
Yakov Pechersky (Oct 15 2021 at 14:34):
I've been using solely WSL for lean for 1.5 years
Matthew Ballard (Oct 15 2021 at 14:48):
Are there simple installation instructions/steps?
Yakov Pechersky (Oct 15 2021 at 14:49):
To install WSL? Or to install lean on it?
Eric Rodriguez (Oct 15 2021 at 14:50):
How'd you set up the rest of development?
Eric Rodriguez (Oct 15 2021 at 14:50):
Like in VSCode do you use remote containers thing? Or do you use nvim or sth
Matthew Ballard (Oct 15 2021 at 14:51):
Yakov Pechersky said:
To install WSL? Or to install lean on it?
All of the above? In W11, I think WSL install is easier now though
Yakov Pechersky (Oct 15 2021 at 14:51):
VSCode has a Remote-WSL mode. One sec, will forward the link
Yakov Pechersky (Oct 15 2021 at 14:53):
Do you use Docker on your machine? If so, there are some more steps to get Docker happy with WSL. Otherwise, try the directions here https://docs.microsoft.com/en-us/windows/wsl/install
Yakov Pechersky (Oct 15 2021 at 14:54):
After those, you have a Linux distro, and can follow the Linux install instructions on mathlib's site. VSCode plugins will work in the Remote-WSL, as long as you click the button that says "Install in Remote-WSL"
Matthew Ballard (Oct 15 2021 at 14:55):
Thanks! No docker. I need to switch over to the other partition to try this out on W11.
Matthew Ballard (Oct 15 2021 at 17:54):
Yes, this was a pleasant experience.
Bryan Gin-ge Chen (Oct 15 2021 at 17:55):
Are WSL instructions worth adding to our install docs? (Does someone want to volunteer to make a PR to our windows install instructions?)
Matthew Ballard (Oct 15 2021 at 18:42):
PR Am I correct in saying there is no regex Zulip linkifier for PRs to this particular repo?
Bryan Gin-ge Chen (Oct 15 2021 at 18:43):
Thanks! Yeah, the linkifier if it worked would be leanprover-community.github.io#211 but it looks like the dots screw it up.
Max (Oct 24 2021 at 15:20):
Btw, it is easy enough to setup lean natively on windows, you don't even need wsl.
Last updated: Dec 20 2023 at 11:08 UTC