## Stream: new members

### Topic: oleans

#### 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).

#### 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.

#### 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.

#### 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.

#### Julian Berman (Mar 24 2021 at 18:32):

A haaaa I found it.

#### 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)

#### 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

#### Julian Berman (Mar 24 2021 at 18:33):

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

#### Julian Berman (Mar 24 2021 at 18:33):

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

#### Julian Berman (Mar 24 2021 at 18:33):

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

#### 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.

#### 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