Zulip Chat Archive

Stream: new members

Topic: oleans


view this post on Zulip Julian Berman (Mar 24 2021 at 18:23):

What should I read to understand how Lean decides whether an olean (presumably one fetched out of band) is acceptable for the .lean file it sits near? Is there a "magic number" or equivalent that takes into account the Lean interpreter version? Presumably there's a checksum on the file contents? The X to this Y is I'm recently [last 2 weeks?] noticing much more compilation happening when I use leanproject to fetch mathlib cached oleans (where I've made no changes).

view this post on Zulip Bryan Gin-ge Chen (Mar 24 2021 at 18:28):

I don't think this is documented anywhere outside of the code. lean#140 by @Wojciech Nawrocki would be where I'd start investigating.

view this post on Zulip Julian Berman (Mar 24 2021 at 18:29):

Thanks! The thing I particularly want to check is whether platform architecture is somehow part of it -- in particular I notice this on my M1, and not on my intel mac (though it's possible I've somehow broken the setup in an unrelated way). Will start by reading there, appreciated.

view this post on Zulip Bryan Gin-ge Chen (Mar 24 2021 at 18:31):

As far as I know platform architecture isn't supposed to matter in Lean 3, so it's interesting if that somehow changed on M1.

view this post on Zulip Julian Berman (Mar 24 2021 at 18:32):

A haaaa I found it.

view this post on Zulip Julian Berman (Mar 24 2021 at 18:32):

Platform is not it, but platform caused the it. (Sorry, I should have found this by just opening the olean in vim)

view this post on Zulip Julian Berman (Mar 24 2021 at 18:32):

I had to start compiling lean myself because the version on GH somehow recently stopped working for reasons I didn't diagnose

view this post on Zulip Julian Berman (Mar 24 2021 at 18:33):

And .oleans contain not just the version but the full version it seems

view this post on Zulip Julian Berman (Mar 24 2021 at 18:33):

Specifically I see in the file: 3.28.0, commit 5a3bb32c05bc

view this post on Zulip Julian Berman (Mar 24 2021 at 18:33):

and I compiled some commit 1 or 2 commits past that probably

view this post on Zulip Bryan Gin-ge Chen (Mar 24 2021 at 18:34):

Yep, this is something we've talked about removing in the past, but it hasn't been high on the list.

view this post on Zulip Julian Berman (Mar 24 2021 at 18:34):

Got it, ok, lesson learned, I'll go compile the release commit


Last updated: May 13 2021 at 00:41 UTC