oleans

Stream: new members

[Julian Berman]

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]

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]

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]

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]

A haaaa I found it.

[Julian Berman]

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

[Julian Berman]

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

[Julian Berman]

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

[Julian Berman]

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

[Julian Berman]

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

[Bryan Gin-ge Chen]

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

[Julian Berman]

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