Zulip Chat Archive

Stream: general

Topic: mathlib olean files


Kevin Buzzard (Jan 22 2019 at 18:18):

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 (Jan 22 2019 at 18:19):

<|> install Linux

Kevin Buzzard (Jan 22 2019 at 18:19):

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

Kevin Buzzard (Jan 22 2019 at 18:20):

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

Patrick Massot (Jan 22 2019 at 18:20):

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

Kevin Buzzard (Jan 22 2019 at 18:21):

Yeah but you have a job

Kevin Buzzard (Jan 22 2019 at 18:21):

They are poor students :-/

Kevin Buzzard (Jan 22 2019 at 18:22):

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 (Jan 22 2019 at 18:22):

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

Kevin Buzzard (Jan 22 2019 at 18:22):

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

Patrick Massot (Jan 22 2019 at 18:23):

How can poor students afford buying Windows?

Kevin Buzzard (Jan 22 2019 at 18:24):

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

Kevin Buzzard (Jan 22 2019 at 18:25):

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 (Jan 22 2019 at 18:25):

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 (Jan 22 2019 at 18:26):

Then you could test installing mathlib on a windows machine

Kevin Buzzard (Jan 22 2019 at 18:26):

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

Kevin Buzzard (Jan 22 2019 at 18:27):

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

Kevin Buzzard (Jan 22 2019 at 20:57):

(deleted)


Last updated: Dec 20 2023 at 11:08 UTC