Cheap installation idea for Windows

Stream: general

[Kevin Buzzard]

If I download Lean 3.4.1 and a recent mathlib on a Windows 7 machine, write a careful leanpkg.path, compile everything (i.e. make all the .olean files), bundle it all up and make it accessible to a bunch of undergraduates who are also using Windows 7 machines, is it likely that they would be able to download and extract this bundle of files and then just have a working Lean and mathlib? In other words, are .olean files compiled on one machine likely to work on another machine running the same OS?

[Mario Carneiro]

I think you should try it and find out

[Mario Carneiro]

I'm not aware of too much experimentation in this area

[Patrick Massot]

We really need such a thing to be possible

[Kevin Buzzard]

I might well do this today.