New laptop

Stream: FoMM / Lean Together 2020

[Neil Strickland]

The bad news is that I had a minor mishap yesterday which resulted in my laptop getting completely borked. I am hoping to buy a new one at Target when it opens at 8am. The good news is that that creates an opportunity to observe/debug/improve the process of installing Lean on a Windows machine. Let me know if you're interested in that. I certainly want to get it done today.

[Neil Strickland]

I have installed Lean on my new laptop following the instructions at https://github.com/leanprover-community/mathlib/blob/master/docs/install/windows.md as far as possible. However, some amendments to those instructions will be needed. I have detailed notes and a bunch of screenshots. I will attempt to go through https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md as well, then I will put together a PR for the documentation. However, it might be more efficient for interested people to talk about it first while we are in Pittsburgh.