Zulip Chat Archive

Stream: general

Topic: Cheap installation idea for Windows

Kevin Buzzard (Jul 02 2018 at 10:33):

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 (Jul 02 2018 at 10:34):

I think you should try it and find out

Mario Carneiro (Jul 02 2018 at 10:34):

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

Patrick Massot (Jul 02 2018 at 10:34):

We really need such a thing to be possible

Kevin Buzzard (Jul 02 2018 at 10:34):

I might well do this today.

Last updated: Dec 20 2023 at 11:08 UTC