More informative 'incompatible header' error?

Stream: lean4

[James E Hanson]

A pain point I keep encountering when working with lake is incompatible header errors of the form

uncaught exception: failed to read file '/path/to/olean/file.olean', incompatible header

It seems like these are usually (always?) an issue with toolchain versions, but I sometimes find it pretty hard to pinpoint where the problem is. Looking at the listed file with xxd at least tells me what its version number is, but when that file lists the version number that I thought the entire project was already on, I don't really know what to look for next.

I've tried using the --verbose flag with lake, but that doesn't do anything here. Is there some way to make this error more informative?

[Kim Morrison]

@James E Hanson, would you mind opening an issue for this one? I agree we could probably provide something actionable here, even if just advice to run lake clean... (Pinging @Mac Malone for visibility.)

[Mac Malone]

Could you provide more details on when/where this has occurred? Usually when this happens there is a bug somewhere. In normal operation, Lake should prevent this from happening.

[James E Hanson]

I realized why this was happening so much. I was playing around with Comparator, which uses a precompiled lean4export binary. I didn't quite understand how the toolchain versions worked at the time, so I was trying to use Comparator on project with different toolchains version than the compiled version of lean4export.