mathlib olean files

Stream: general

[Kevin Buzzard]

I just upgraded to Lean 3.4.2 and mathlib master. I've got everything compiling. @Chris Hughes and @Kenny Lau I know it's a pain for you to compile mathlib sometimes. Here is a link: mathlib.tar . I packed up mathlib (including all the .olean files) into a "tarball" (using POSIX tar so file timestamps should be to the nearest nanosecond or whatever). Q1 : can you untar this file back into a mathlib directory? And Q2: if you can, what are the timestamps like? For me, if I look in src/topology then I see basic.lean was created at 16:12 today and basic.olean at 16:49, so Lean knows that I didn't edit basic.leanafter I created basic.olean. I took the tarball and untarred it on another unix computer and the timestamps survived. If by the time these files get to you the timestamps of basic.lean and basic.olean are "the time it is now", then the experiment has failed (do files have timestamps in Windows? I know nothing!) because Lean might decide it's time to recompile basic.lean anyway. But if the times are different then maybe this saves you some time compiling mathlib.

[Patrick Massot]

<|> install Linux

[Kevin Buzzard]

Sure, but I'm sure you know that for some people this simply isn't an option.

[Kevin Buzzard]

I'm not sure how to get linux running on a Microsoft Surface Pro, for example.

[Patrick Massot]

I think it's about time Chris and Kenny leave that category of people

[Kevin Buzzard]

Yeah but you have a job

[Kevin Buzzard]

They are poor students :-/

[Kevin Buzzard]

Apparently winzip can extract tarballs. I just don't know what it does with the timestamps. My understanding is that if all the timestamps come out the same then we have to think again. But even this might not be unsolvable.

[Kevin Buzzard]

Imagine if I just zipped up the .olean files and they could somehow unzip them into a mathlib directory.

[Kevin Buzzard]

Then the fact that they're timestamped "now" is to our advantage.

[Patrick Massot]

How can poor students afford buying Windows?

[Kevin Buzzard]

I think they get their parents' old laptops :-/

[Kevin Buzzard]

They might need Windows for other things. My 16 year old son wants to run software like Unity to develop games and this is Windows only, so we are forced to have a Windows machine at home.

[Kevin Buzzard]

All I'm saying is that "switch OS" is of course a solution but it might not be a solution that works for everyone. If we could figure out a way to save my students some time then this would be advantageous for me.

[Patrick Massot]

Then you could test installing mathlib on a windows machine

[Kevin Buzzard]

yes, but it's easier for them to test it :-)

[Kevin Buzzard]

anyway, I'm still at work! I just finished talking to Ramon, who has actually started on schemes :D

[Kevin Buzzard]

(deleted)