Bring back .olean version check

[Kha]

We should add back the Lean 3 behavior of writing the Lean binary's commit hash into each .olean file and checking against it on load, optionally omitting the check during development.

However, Lean 4 introduces a new complication here: if we compile only up to stage 1, we use a stdlib compiled by stage 0 (whose hash we set to 00... to avoid rebuilds). So the check would fail. We would either need a new flag for overriding the commit hash while building, or always build up to stage 2. If we default the check to off for development, we could do so only for (nightly/stable) release builds, in which case the overhead of building stage 2 shouldn't matter.