Cross-version olean imports

Stream: lean4

[Mac]

@Xubai Wang discovered that Lake (revision 71defa0) built with leanprover/lean4:nightly-2021-07-09 segfaults when the elan Lean version in the current working directory is set to leanprover/lean4:nightly-2021-07-23. He reported this issue to me on the Lake GitHub (see #3). I reproduced this (it hangs for me) and discovered it also occurs with later versions (such as the 07-28 nightly).

I suspect this is because the Lean version Lake is built with is different from the Lean version of the .oleans Lake finds in its search path while interpreting the config file. If I am correct about this, would it be feasible for Lean to save some kind of version information in an .olean about the Lean version it was built with and verify that it matches the running Lean version when imported? Though, honestly, anything would be better than the current behavior of a hang/segfault. :wink: