Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC